Theorem: LO.FirstOrder.Arith.Model.Exponential.Seqₛ.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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
⊢ Seqₛ y X Y →
    ∀ u ≤ y,
      u ≠ 2 →
        PPow2 u →
          ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
            (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
intro H u hu ne2 ppu
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
rcases H u hu ne2 ppu with (H | H)
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) 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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
exact Or.inl ⟨⟨ext u X, by simp [H.1]⟩, ⟨ext u Y, by simp [H.2]⟩⟩
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ext u X ≤ X ∧ ext u X = ext u X ∧ 2 * ext u X = ext (u ^ 2) X
Tactic:
simp [H.1]
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Even X Y u
⊢ ext u Y ≤ Y ∧ ext u Y = ext u Y ∧ ext u Y ^ 2 = ext (u ^ 2) Y
Tactic:
simp [H.2]
State after:
no goals

State before:
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
    (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
      ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
Tactic:
exact Or.inr ⟨⟨ext u X, by simp [H.1]⟩, ⟨ext u Y, by simp [H.2]⟩⟩
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ext u X ≤ X ∧ ext u X = ext u X ∧ 2 * ext u X + 1 = ext (u ^ 2) X
Tactic:
simp [H.1]
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H✝ : Seqₛ y X Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
H : Odd X Y u
⊢ ext u Y ≤ Y ∧ ext u Y = ext u Y ∧ 2 * ext u Y ^ 2 = ext (u ^ 2) Y
Tactic:
simp [H.2]
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
⊢ (∀ u ≤ y,
      u ≠ 2 →
        PPow2 u →
          ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
            (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
              ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y) →
    Seqₛ y X Y
Tactic:
intro H u hu ne2 ppu
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ Even X Y u ∨ Odd X Y u

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
⊢ Even X Y u ∨ Odd X Y u
Tactic:
rcases H u hu ne2 ppu with (⟨⟨_, _, rfl, hx⟩, ⟨_, _, rfl, hy⟩⟩ | ⟨⟨_, _, rfl, hx⟩, ⟨_, _, rfl, hy⟩⟩)
State after:
case inl.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 Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u

case inr.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 Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u

State before:
case inl.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 Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u
Tactic:
exact Or.inl ⟨by simp [hx, hy], by simp [hx, hy]⟩
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) X = 2 * ext u X
Tactic:
simp [hx, hy]
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) Y = ext u Y ^ 2
Tactic:
simp [hx, hy]
State after:
no goals

State before:
case inr.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 Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ Even X Y u ∨ Odd X Y u
Tactic:
exact Or.inr ⟨by simp [hx, hy], by simp [hx, hy]⟩
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) X = 2 * ext u X + 1
Tactic:
simp [hx, hy]
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 ⊧ₘ* 𝐈𝚫₀
y X Y : M
H :
  ∀ u ≤ y,
    u ≠ 2 →
      PPow2 u →
        ((∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ ext_u_Y ^ 2 = ext (u ^ 2) Y) ∨
          (∃ ext_u_X ≤ X, ext_u_X = ext u X ∧ 2 * ext_u_X + 1 = ext (u ^ 2) X) ∧
            ∃ ext_u_Y ≤ Y, ext_u_Y = ext u Y ∧ 2 * ext_u_Y ^ 2 = ext (u ^ 2) Y
u : M
hu : u ≤ y
ne2 : u ≠ 2
ppu : PPow2 u
left✝¹ : ext u X ≤ X
hx : 2 * ext u X + 1 = ext (u ^ 2) X
left✝ : ext u Y ≤ Y
hy : 2 * ext u Y ^ 2 = ext (u ^ 2) Y
⊢ ext (u ^ 2) Y = 2 * ext u Y ^ 2
Tactic:
simp [hx, hy]
State after:
no goals