Theorem: LO.FirstOrder.Arith.Model.Exponential.graph_iff (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
⊢ Exponential x y →
    x = 0 ∧ y = 1 ∨
      ∃ X ≤ y ^ 4,
        ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Tactic:
rintro (H | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, hY⟩⟩)
State after:
case inl
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 = 0 ∧ y = 1
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y

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
bX : X ≤ y ^ 4
Y : M
bY : 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 = x
hY : ext u Y = y
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y

State before:
case inl
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 = 0 ∧ y = 1
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Tactic:
exact Or.inl 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
bX : X ≤ y ^ 4
Y : M
bY : 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 = x
hY : ext u Y = y
⊢ x = 0 ∧ y = 1 ∨
    ∃ X ≤ y ^ 4,
      ∃ Y ≤ y ^ 4, (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y
Tactic:
exact Or.inr ⟨X, bX, Y, bY, ⟨H₀.1.symm, H₀.2.symm⟩, Hₛ, ⟨u, hu, ne2, ppu, hX.symm, hY.symm⟩⟩
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
⊢ (x = 0 ∧ y = 1 ∨
      ∃ X ≤ y ^ 4,
        ∃ Y ≤ y ^ 4,
          (1 = ext 4 X ∧ 2 = ext 4 Y) ∧ Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ PPow2 u ∧ x = ext u X ∧ y = ext u Y) →
    Exponential x y
Tactic:
rintro (H | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, hX, hY⟩⟩)
State after:
case inl
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 = 0 ∧ y = 1
⊢ Exponential x y

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
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : 1 = ext 4 X ∧ 2 = ext 4 Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : x = ext u X
hY : y = ext u Y
⊢ Exponential x y

State before:
case inl
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 = 0 ∧ y = 1
⊢ Exponential x y
Tactic:
exact Or.inl 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
bX : X ≤ y ^ 4
Y : M
bY : Y ≤ y ^ 4
H₀ : 1 = ext 4 X ∧ 2 = ext 4 Y
Hₛ : Seqₛ y X Y
u : M
hu : u ≤ y ^ 2
ne2 : u ≠ 2
ppu : PPow2 u
hX : x = ext u X
hY : y = ext u Y
⊢ Exponential x y
Tactic:
exact Or.inr ⟨X, bX, Y, bY, ⟨H₀.1.symm, H₀.2.symm⟩, Hₛ, ⟨u, hu, ne2, ppu, hX.symm, hY.symm⟩⟩
State after:
no goals