α : Type ?u.297877
β : Type ?u.297880
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a * b = 1
⊢ b ≠ ⊤
α : Type ?u.297877
β : Type ?u.297880
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a * b = 1
⊢ a = b⁻¹
rw [← mul_one a, ← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h), ← mul_assoc, h,
  one_mul]
α : Type ?u.297877
β : Type ?u.297880
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a * ⊤ = 1
⊢ False
α : Type ?u.297877
β : Type ?u.297880
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a * b = 1
⊢ b ≠ ⊤
rintro rfl
no goals
α : Type ?u.297877
β : Type ?u.297880
a c d : ℝ≥0∞
r p q : ℝ≥0
h : a * ⊤ = 1
⊢ False
simp [left_ne_zero_of_mul_eq_one h] at h