case zero
q : ℕ+
⊢ ↑(s zero) = ω ^ 2 ^ zero + ωb ^ 2 ^ zero

case succ
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s (succ i)) = ω ^ 2 ^ succ i + ωb ^ 2 ^ succ i
q : ℕ+
i : ℕ
⊢ ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
induction' i with i ih
case zero
q : ℕ+
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1
case zero
q : ℕ+
⊢ ↑(s zero) = ω ^ 2 ^ zero + ωb ^ 2 ^ zero
dsimp [s, ω, ωb]
no goals
case zero
q : ℕ+
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1
ext <;> norm_num
no goals
case succ
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s (succ i)) = ω ^ 2 ^ succ i + ωb ^ 2 ^ succ i
calc
  (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
  _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
  _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
  _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
  _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
    rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel]
  _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ']
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i ^ 2 - 2) = ↑(s i) ^ 2 - 2
push_cast
no goals
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
rfl
no goals
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2
rw [ih]
no goals
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2
ring
no goals
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2
rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel]
no goals
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)
rw [← pow_mul, ← pow_mul, _root_.pow_succ']