Theorem: LO.FirstOrder.Arith.Model.sub_sub (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
⊢ a - b - c = a - (b + c)
Tactic:
by_cases ha : b + c ≤ a
State after:
case pos
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
ha : b + c ≤ a
⊢ a - b - c = a - (b + c)

case neg
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
ha : ¬b + c ≤ a
⊢ a - b - c = a - (b + c)

State before:
case pos
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
ha : b + c ≤ a
⊢ a - b - c = a - (b + c)
Tactic:
exact sub_remove_left <| sub_remove_left <| by
  simp [add_assoc, show c + b = b + c from add_comm _ _, sub_add_self_of_le, ha]
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
ha : b + c ≤ a
⊢ a = a - (b + c) + c + b
Tactic:
simp [add_assoc, show c + b = b + c from add_comm _ _, sub_add_self_of_le, ha]
State after:
no goals

State before:
case neg
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
ha : ¬b + c ≤ a
⊢ a - b - c = a - (b + c)
Tactic:
simp [sub_spec_of_lt (show a < b + c from not_le.mp ha)]
State after:
case neg
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
ha : ¬b + c ≤ a
⊢ a - b - c = 0

State before:
case neg
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
ha : ¬b + c ≤ a
⊢ a - b - c = 0
Tactic:
by_cases hc : c ≤ a - b
State after:
case pos
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
⊢ a - b - c = 0

case neg
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
ha : ¬b + c ≤ a
hc : ¬c ≤ a - b
⊢ a - b - c = 0

State before:
case pos
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
⊢ a - b - c = 0
Tactic:
by_cases hb : b ≤ a
State after:
case pos
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
⊢ a - b - c = 0

case neg
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : ¬b ≤ a
⊢ a - b - c = 0

State before:
case pos
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
⊢ a - b - c = 0
Tactic:
have : a < a := calc
  a < b + c       := not_le.mp ha
  _ ≤ b + (a - b) := by simp[hc]
  _ = a           := add_tsub_self_of_le hb
State after:
case pos
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
this : a < a
⊢ a - b - c = 0

State before:
case pos
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
this : a < a
⊢ a - b - c = 0
Tactic:
simp at this
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
⊢ b + c ≤ b + (a - b)
Tactic:
simp[hc]
State after:
no goals

State before:
case neg
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
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : ¬b ≤ a
⊢ a - b - c = 0
Tactic:
simp [show a - b = 0 from sub_spec_of_lt (not_le.mp hb)]
State after:
no goals

State before:
case neg
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
ha : ¬b + c ≤ a
hc : ¬c ≤ a - b
⊢ a - b - c = 0
Tactic:
exact sub_spec_of_lt (not_le.mp hc)
State after:
no goals