case inl
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

case inr
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
⊢ (a - b) * c = a * c - b * c
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
⊢ (a - b) * c = a * c - b * c
cases' le_or_lt a b with hab hab
case inr.inl
α : Type ?u.188373
β : Type ?u.188376
a c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < 0 → 0 < a → c ≠ ⊤
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

case inr.inr
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c
case inr
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
⊢ (a - b) * c = a * c - b * c
rcases eq_or_lt_of_le (zero_le b) with (rfl | hb)
no goals
case inr.inr
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c
exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul
no goals
case inl
α : Type ?u.188373
β : Type ?u.188376
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < b → b < a → c ≠ ⊤
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c
simp [hab, mul_right_mono hab]
no goals
case inr.inl
α : Type ?u.188373
β : Type ?u.188376
a c d : ℝ≥0∞
r p q : ℝ≥0
h : 0 < 0 → 0 < a → c ≠ ⊤
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c
simp