have : ¬2 ∣ ext i X := by
  simp [show ext i X = 2 * ext (√i) X + 1 from by simpa [ppi.sq_sqrt_eq ne2] using hXi,
    ←mod_eq_zero_iff_dvd, one_lt_two]
case neg.inr.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
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = 2 * x
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this : 2 ∣ ext i X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'
case neg.inr.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
left✝¹ : X ≤ y ^ 4
Y : M
left✝ : Y ≤ y ^ 4
hseq₀ : Seq₀ X Y
hseqₛ : Seqₛ y X Y
i : M
hi : i ≤ y ^ 2
ne2 : i ≠ 2
ppi : PPow2 i
hXx : ext i X = 2 * x
hYy : ext i Y = y
ne4 : ¬i = 4
hXi : ext ((√i) ^ 2) X = 2 * ext (√i) X + 1
right✝ : ext ((√i) ^ 2) Y = 2 * ext (√i) Y ^ 2
this✝ : 2 ∣ ext i X
this : ¬2 ∣ ext i X
⊢ ∃ y', y = y' ^ 2 ∧ Exponential x y'