Theorem: LO.FirstOrder.Arith.Model.Exponential.succ_lt_s (Arithmetization/ISigmaZero/Exponential/Exp.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
h : Exponential (x + 1) y
⊢ 2 ≤ y
Tactic:
rcases h with (⟨h, rfl⟩ | ⟨X, _, Y, _, H₀, Hₛ, ⟨u, hu, ne2, ppu, _, hY⟩⟩)
State after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
h : x + 1 = 0
⊢ 2 ≤ 1

case inr.intro.intro.intro.intro.intro.intro.intro.intro.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 X : M
left✝² : X ≤ y ^ 4
Y : M
left✝¹ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
left✝ : ext u X = x + 1
hY : ext u Y = y
⊢ 2 ≤ y

State before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
x : M
h : x + 1 = 0
⊢ 2 ≤ 1
Tactic:
simp at h
State after:
no goals

State before:
case inr.intro.intro.intro.intro.intro.intro.intro.intro.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 X : M
left✝² : X ≤ y ^ 4
Y : M
left✝¹ : Y ≤ y ^ 4
H₀ : Seq₀ X Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
left✝ : ext u X = x + 1
hY : ext u Y = y
⊢ 2 ≤ y
Tactic:
simpa [hY] using two_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
State after:
no goals