Theorem: LO.FirstOrder.Arith.Model.Exponential.zero_uniq (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 ⊧ₘ* 𝐈𝚫₀
y : M
h : Exponential 0 y
⊢ y = 1
Tactic:
rcases h with (⟨_, rfl⟩ | ⟨X, _, Y, _, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, _⟩⟩)
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 ⊧ₘ* 𝐈𝚫₀
left✝ : 0 = 0
⊢ 1 = 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 ⊧ₘ* 𝐈𝚫₀
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
hX : ext u X = 0
right✝ : ext u Y = y
⊢ y = 1

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 ⊧ₘ* 𝐈𝚫₀
left✝ : 0 = 0
⊢ 1 = 1
Tactic:
rfl
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 ⊧ₘ* 𝐈𝚫₀
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
hX : ext u X = 0
right✝ : ext u Y = y
⊢ y = 1
Tactic:
have : 1 ≤ ext u X  := one_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
State after:
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 ⊧ₘ* 𝐈𝚫₀
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
hX : ext u X = 0
right✝ : ext u Y = y
this : 1 ≤ ext u X
⊢ y = 1

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 ⊧ₘ* 𝐈𝚫₀
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
hX : ext u X = 0
right✝ : ext u Y = y
this : 1 ≤ ext u X
⊢ y = 1
Tactic:
simp [hX] at this
State after:
no goals