rcases show Seqₛ.Even X Y (√i) ∨ Seqₛ.Odd X Y (√i) from
  hₛ (√i) (sqrt_le_of_le_sq $ hi) (ppi.sqrt_ne_two ne2 ne4) (ppi.sqrt ne2) with (heven | hodd)
case neg
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₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
⊢ 1 ≤ ext i X
case neg.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₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
heven : Seqₛ.Even X Y (√i)
⊢ 1 ≤ ext i X

case neg.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₀ X Y
hₛ : Seqₛ y X Y
i : M
IH✝ : ∀ y_1 < i, y_1 ≠ 2 → y_1 ≤ y ^ 2 → PPow2 y_1 → 1 ≤ ext y_1 X
ne2 : i ≠ 2
hi : i ≤ y ^ 2
ppi : PPow2 i
ne4 : ¬i = 4
IH : 1 ≤ ext (√i) X
hodd : Seqₛ.Odd X Y (√i)
⊢ 1 ≤ ext i X