no goals
α : Type ?u.310360
β : Type ?u.310363
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
h : b = c / a
⊢ a * b = c
rw [h, ENNReal.mul_div_cancel' ha ha']
no goals
α : Type ?u.310360
β : Type ?u.310363
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
ha' : a ≠ ⊤
h : a * b = c
⊢ b = c / a
rw [← h, mul_div_assoc, ENNReal.mul_div_cancel' ha ha']