Theorem: LO.FirstOrder.Arith.Model.le_iff_lt_succ (Logic/FirstOrder/Arith/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 ⊧ₘ* 𝐏𝐀⁻
x y : M
⊢ x ≤ y → x < y + 1
Tactic:
intro h
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h : x ≤ y
⊢ x < y + 1

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h : x ≤ y
⊢ x < y + 1
Tactic:
exact lt_of_le_of_lt h (lt_add_one y)
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 ⊧ₘ* 𝐏𝐀⁻
x y : M
h : x < y + 1
⊢ x ≤ y
Tactic:
rcases lt_iff_exists_add.mp h with ⟨z, hz, h⟩
State after:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z : M
hz : z > 0
h : y + 1 = x + z
⊢ x ≤ y

State before:
case intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z : M
hz : z > 0
h : y + 1 = x + z
⊢ x ≤ y
Tactic:
rcases eq_succ_of_pos hz with ⟨z', rfl⟩
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
⊢ x ≤ y

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
⊢ x ≤ y
Tactic:
have : y = x + z' := by simpa[←add_assoc] using h
State after:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
this : y = x + z'
⊢ x ≤ y

State before:
case intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
this : y = x + z'
⊢ x ≤ y
Tactic:
simp[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 ⊧ₘ* 𝐏𝐀⁻
x y : M
h✝ : x < y + 1
z' : M
hz : z' + 1 > 0
h : y + 1 = x + (z' + 1)
⊢ y = x + z'
Tactic:
simpa[←add_assoc] using h
State after:
no goals