calc
  2 * (2 * y ^ 2) = (2 * y)^2 := by simp [sq, mul_assoc, mul_left_comm y 2]
  _               ≤ i^2       := sq_le_sq.mpr (by simpa [hYy] using this)
  _               < 2 * i^2   := lt_mul_of_one_lt_left ppi.sq.pos one_lt_two
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 + 1 < i ^ 2
this : 2 * ext i Y ≤ i
⊢ 2 * (2 * y ^ 2) < 2 * i ^ 2
no goals