Theorem: LO.FirstOrder.Arith.Model.sub_mul (Arithmetization/Basic/PeanoMinus.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ (a - b) * c = a * c - b * c
Tactic:
have : a = (a - b) + b := (tsub_eq_iff_eq_add_of_le h).mp rfl
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = a * c - b * c

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = a * c - b * c
Tactic:
calc
  (a - b) * c = (a - b) * c + b * c - b * c := by simp
  _           = (a - b + b) * c - b * c     := by simp [add_mul]
  _           = a * c - b * c               := by simp [sub_add_self_of_le h]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = (a - b) * c + b * c - b * c
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c + b * c - b * c = (a - b + b) * c - b * c
Tactic:
simp [add_mul]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b + b) * c - b * c = a * c - b * c
Tactic:
simp [sub_add_self_of_le h]
State after:
no goals