rw [ext_append_of_lt, ext_append_of_lt, ext_append_of_lt, ext_append_of_lt] <;> try simp [ppi.sq, ppj.sq, lt_of_le_of_lt hj hz, *]
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) (Exponential.append (i ^ 2) X x) = 2 * ext j (Exponential.append (i ^ 2) X x) ∧
    ext (j ^ 2) (Exponential.append (i ^ 2) Y y) = ext j (Exponential.append (i ^ 2) Y y) ^ 2
case inl.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
z x y X Y i : M
h : Seqₛ z X Y
ppi : PPow2 i
hz : z < i
j : M
hj : j ≤ z
ne2 : j ≠ 2
ppj : PPow2 j
this✝ : j < i ^ 2
this : j ^ 2 < i ^ 2
H : Even X Y j
⊢ ext (j ^ 2) X = 2 * ext j X ∧ ext (j ^ 2) Y = ext j Y ^ 2