case zero

⊢ fib (2 * zero) = fib zero * (2 * fib (zero + 1) - fib zero)

case succ
n✝ : ℕ
⊢ fib (2 * succ n✝) = fib (succ n✝) * (2 * fib (succ n✝ + 1) - fib (succ n✝))
n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)
cases n
no goals
case zero

⊢ fib (2 * zero) = fib zero * (2 * fib (zero + 1) - fib zero)
simp
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
case succ
n✝ : ℕ
⊢ fib (2 * succ n✝) = fib (succ n✝) * (2 * fib (succ n✝ + 1) - fib (succ n✝))
rw [Nat.succ_eq_add_one, two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
simp only [← add_assoc, add_tsub_cancel_right]
no goals
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)
ring