rw [ext_append_last, ext_append_last, ext_append_of_lt , ext_append_of_lt] <;>
  simp [ppi, ppi.sq, hxsqi, hysqi, hiisq, hXx, hYy]
case neg.h
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 = x
hYy : ext i Y = y
hxsqi : 2 * x < i ^ 2
hiisq : i < i ^ 2
X' : M := append (i ^ 2) X (2 * x)
Y' : M := append (i ^ 2) Y (y ^ 2)
bX' : X' ≤ (y ^ 2) ^ 4
bY' : Y' ≤ (y ^ 2) ^ 4
hseq₀' : Seq₀ X' Y'
hj : i ≤ y ^ 2
jne2 : ¬i = 2
ppj : PPow2 i
hysqi : y < i
hjy : y < i
⊢ ext (i ^ 2) X' = 2 * ext i X' ∧ ext (i ^ 2) Y' = ext i Y' ^ 2
no goals