α : Type ?u.262242
β : Type ?u.262245
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
α : Type ?u.262242
β : Type ?u.262245
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c
simp_rw [div_eq_mul_inv]
no goals
α : Type ?u.262242
β : Type ?u.262245
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
exact ENNReal.sub_mul (by simpa using h)
no goals
α : Type ?u.262242
β : Type ?u.262245
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ⊤
simpa using h