Theorem: coe_fib_eq (LeanCourse/Lectures/Lecture7.lean)

State before:
n✝ n : ℕ
⊢ ↑(fib n) = (ϕ ^ n - ψ ^ n) / (ϕ - ψ)
Tactic:
induction n using Nat.two_step_induction
State after:
case zero
n : ℕ
⊢ ↑(fib 0) = (ϕ ^ 0 - ψ ^ 0) / (ϕ - ψ)

case one
n : ℕ
⊢ ↑(fib 1) = (ϕ ^ 1 - ψ ^ 1) / (ϕ - ψ)

case step
n k✝ : ℕ
IH0✝ : ↑(fib k✝) = (ϕ ^ k✝ - ψ ^ k✝) / (ϕ - ψ)
IH1✝ : ↑(fib (k✝ + 1)) = (ϕ ^ (k✝ + 1) - ψ ^ (k✝ + 1)) / (ϕ - ψ)
⊢ ↑(fib (k✝ + 2)) = (ϕ ^ (k✝ + 2) - ψ ^ (k✝ + 2)) / (ϕ - ψ)

State before:
n : ℕ
⊢ ↑(fib 0) = (ϕ ^ 0 - ψ ^ 0) / (ϕ - ψ)
Tactic:
case zero => simp
State after:
no goals

State before:
n : ℕ
⊢ ↑(fib 1) = (ϕ ^ 1 - ψ ^ 1) / (ϕ - ψ)
Tactic:
case one => simp
State after:
no goals

State before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ↑(fib (k + 2)) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Tactic:
case step k ih1 ih2 =>
  simp [fib, ih1, ih2]
  field_simp
  simp [pow_add]
  ring
State after:
no goals

State before:
n : ℕ
⊢ ↑(fib 0) = (ϕ ^ 0 - ψ ^ 0) / (ϕ - ψ)
Tactic:
simp
State after:
no goals

State before:
n : ℕ
⊢ ↑(fib 1) = (ϕ ^ 1 - ψ ^ 1) / (ϕ - ψ)
Tactic:
simp
State after:
no goals

State before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ↑(fib (k + 2)) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Tactic:
simp [fib, ih1, ih2]
State after:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ) + (ϕ ^ k - ψ ^ k) / (ϕ - ψ) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)

State before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ) + (ϕ ^ k - ψ ^ k) / (ϕ - ψ) = (ϕ ^ (k + 2) - ψ ^ (k + 2)) / (ϕ - ψ)
Tactic:
field_simp
State after:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ (k + 1) - ψ ^ (k + 1) + (ϕ ^ k - ψ ^ k) = ϕ ^ (k + 2) - ψ ^ (k + 2)

State before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ (k + 1) - ψ ^ (k + 1) + (ϕ ^ k - ψ ^ k) = ϕ ^ (k + 2) - ψ ^ (k + 2)
Tactic:
simp [pow_add]
State after:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ k * ϕ - ψ ^ k * ψ + (ϕ ^ k - ψ ^ k) = ϕ ^ k * (ϕ + 1) - ψ ^ k * (ψ + 1)

State before:
n k : ℕ
ih1 : ↑(fib k) = (ϕ ^ k - ψ ^ k) / (ϕ - ψ)
ih2 : ↑(fib (k + 1)) = (ϕ ^ (k + 1) - ψ ^ (k + 1)) / (ϕ - ψ)
⊢ ϕ ^ k * ϕ - ψ ^ k * ψ + (ϕ ^ k - ψ ^ k) = ϕ ^ k * (ϕ + 1) - ψ ^ k * (ψ + 1)
Tactic:
ring
State after:
no goals