case intro
α : Type ?u.226273
β : Type ?u.226276
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ↑a ≠ 0
⊢ ↑a * (↑a)⁻¹ = 1
α : Type ?u.226273
β : Type ?u.226276
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : a ≠ 0
ht : a ≠ ⊤
⊢ a * a⁻¹ = 1
lift a to ℝ≥0 using ht
case intro
α : Type ?u.226273
β : Type ?u.226276
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1
case intro
α : Type ?u.226273
β : Type ?u.226276
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ↑a ≠ 0
⊢ ↑a * (↑a)⁻¹ = 1
norm_cast at h0
case intro
α : Type ?u.226273
β : Type ?u.226276
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1
case intro
α : Type ?u.226273
β : Type ?u.226276
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ¬a = 0
⊢ ↑a * (↑a)⁻¹ = 1
norm_cast
no goals
case intro
α : Type ?u.226273
β : Type ?u.226276
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ¬a = 0
⊢ a * a⁻¹ = 1
exact mul_inv_cancel h0