-- Mathlib/Data/Real/GoldenRatio.lean
theorem Real.coe_fib_eq' :
    (fun n => Nat.fib n : ℕ → ℝ) = fun n => (φ ^ n - ψ ^ n) / √5

Proof state:
case «1»

⊢ √5 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_4.h
this : fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = (√5)⁻¹ * φ ^ x✝ - (√5)⁻¹ * ψ ^ x✝

Tactic:
ring

Result:
no goals

Proof state:
case hv.a

⊢ (fun n => (√5)⁻¹ * ψ ^ n) ∈ fibRec.solSpace

Tactic:
exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_goldConj_isSol_fibRec

Result:
no goals

Proof state:
case hv

⊢ fibRec.IsSolution fun n => (φ ^ n - ψ ^ n) / √5

Tactic:
suffices LinearRecurrence.IsSolution fibRec
    ((fun n ↦ (√5)⁻¹ * φ ^ n) - (fun n ↦ (√5)⁻¹ * ψ ^ n)) by
  convert this
  rw [Pi.sub_apply]
  ring

Result:
case hv

⊢ fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)

Proof state:
⊢ Set.EqOn (fun n => ↑(Nat.fib n)) (fun n => (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)

Tactic:
intro i hi

Result:
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / √5) i

Proof state:
this : fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)
⊢ fibRec.IsSolution fun n => (φ ^ n - ψ ^ n) / √5

Tactic:
convert this

Result:
case h.e'_4.h
this : fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n) x✝

Proof state:
case «1»

⊢ 1 = √5 * (√5)⁻¹

Tactic:
rw [mul_inv_cancel₀]

Result:
case «1»

⊢ √5 ≠ 0

Proof state:
case «0»

⊢ (fun n => ↑(Nat.fib n)) 0 = (fun n => (φ ^ n - ψ ^ n) / √5) 0

Tactic:
simp

Result:
no goals

Proof state:
case hv.a

⊢ (fun n => (√5)⁻¹ * φ ^ n) ∈ fibRec.solSpace

Tactic:
exact Submodule.smul_mem fibRec.solSpace (√5)⁻¹ geom_gold_isSol_fibRec

Result:
no goals

Proof state:
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / √5) i

Tactic:
norm_cast at hi

Result:
i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / √5) i

Proof state:
case «1»

⊢ (fun n => ↑(Nat.fib n)) 1 = (fun n => (φ ^ n - ψ ^ n) / √5) 1

Tactic:
simp only [goldenRatio, goldenConj]

Result:
case «1»

⊢ ↑(Nat.fib 1) = (((1 + √5) / 2) ^ 1 - ((1 - √5) / 2) ^ 1) / √5

Proof state:
case «1»

⊢ ↑(Nat.fib 1) = (((1 + √5) / 2) ^ 1 - ((1 - √5) / 2) ^ 1) / √5

Tactic:
ring_nf

Result:
case «1»

⊢ 1 = √5 * (√5)⁻¹

Proof state:
case hv

⊢ fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)

Tactic:
apply (@fibRec ℝ _).solSpace.sub_mem

Result:
case hv.a

⊢ (fun n => (√5)⁻¹ * φ ^ n) ∈ fibRec.solSpace

case hv.a

⊢ (fun n => (√5)⁻¹ * ψ ^ n) ∈ fibRec.solSpace

Proof state:
case h.e'_4.h
this : fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n) x✝

Tactic:
rw [Pi.sub_apply]

Result:
case h.e'_4.h
this : fibRec.IsSolution ((fun n => (√5)⁻¹ * φ ^ n) - fun n => (√5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / √5 = (√5)⁻¹ * φ ^ x✝ - (√5)⁻¹ * ψ ^ x✝

Proof state:
i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / √5) i

Tactic:
fin_cases hi

Result:
case «0»

⊢ (fun n => ↑(Nat.fib n)) 0 = (fun n => (φ ^ n - ψ ^ n) / √5) 0

case «1»

⊢ (fun n => ↑(Nat.fib n)) 1 = (fun n => (φ ^ n - ψ ^ n) / √5) 1

Proof state:
⊢ (fun n => ↑(Nat.fib n)) = fun n => (φ ^ n - ψ ^ n) / √5

Tactic:
rw [fibRec.sol_eq_of_eq_init]

Result:
⊢ Set.EqOn (fun n => ↑(Nat.fib n)) (fun n => (φ ^ n - ψ ^ n) / √5) ↑(Finset.range fibRec.order)

case hu

⊢ fibRec.IsSolution fun n => ↑(Nat.fib n)

case hv

⊢ fibRec.IsSolution fun n => (φ ^ n - ψ ^ n) / √5

Proof state:
case hu

⊢ fibRec.IsSolution fun n => ↑(Nat.fib n)

Tactic:
exact fib_isSol_fibRec

Result:
no goals