no goals
case inl
α : Type u
β : Type ?u.23190
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hbc : b ≤ c
⊢ a * (b - c) = a * b - a * c
rw [tsub_eq_zero_iff_le.2 hbc, mul_zero, tsub_eq_zero_iff_le.2 (mul_le_mul_left' hbc a)]
case inr
α : Type u
β : Type ?u.23190
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b
case inr
α : Type u
β : Type ?u.23190
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) = a * b - a * c
apply h.eq_tsub_of_add_eq
no goals
case inr
α : Type u
β : Type ?u.23190
inst✝³ : CanonicallyOrderedCommSemiring α
a b c : α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : IsTotal α fun x x_1 => x ≤ x_1
h : AddLECancellable (a * c)
hcb : c ≤ b
⊢ a * (b - c) + a * c = a * b
rw [← mul_add, tsub_add_cancel_of_le hcb]