rcases H u hu ne2 ppu with (⟨⟨_, _, rfl, hx⟩, ⟨_, _, rfl, hy⟩⟩ | ⟨⟨_, _, rfl, hx⟩, ⟨_, _, rfl, hy⟩⟩)
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
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