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

case hu

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

case hv

⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
⊢ (fun n => ↑(Nat.fib n)) = fun n => (φ ^ n - ψ ^ n) / sqrt 5
rw [fibRec.sol_eq_of_eq_init]
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
⊢ Set.EqOn (fun n => ↑(Nat.fib n)) (fun n => (φ ^ n - ψ ^ n) / sqrt 5) ↑(Finset.range fibRec.order)
intro i hi
i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
norm_cast at hi
case head

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

case tail.head

⊢ (fun n => ↑(Nat.fib n)) 1 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 1
i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
fin_cases hi
no goals
case head

⊢ (fun n => ↑(Nat.fib n)) 0 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 0
simp
case tail.head

⊢ ↑(Nat.fib 1) = (((1 + sqrt 5) / 2) ^ 1 - ((1 - sqrt 5) / 2) ^ 1) / sqrt 5
case tail.head

⊢ (fun n => ↑(Nat.fib n)) 1 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 1
simp only [goldenRatio, goldenConj]
case tail.head

⊢ 1 = sqrt 5 * (sqrt 5)⁻¹
case tail.head

⊢ ↑(Nat.fib 1) = (((1 + sqrt 5) / 2) ^ 1 - ((1 - sqrt 5) / 2) ^ 1) / sqrt 5
ring_nf
case tail.head

⊢ sqrt 5 ≠ 0
case tail.head

⊢ 1 = sqrt 5 * (sqrt 5)⁻¹
rw [mul_inv_cancel]
no goals
case tail.head

⊢ sqrt 5 ≠ 0
norm_num
no goals
case hu

⊢ LinearRecurrence.IsSolution fibRec fun n => ↑(Nat.fib n)
exact fib_isSol_fibRec
case hv

⊢ LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
case hv

⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
suffices LinearRecurrence.IsSolution fibRec
    ((fun n ↦ (sqrt 5)⁻¹ * φ ^ n) - (fun n ↦ (sqrt 5)⁻¹ * ψ ^ n)) by
  convert this
  rw [Pi.sub_apply]
  ring
case hv.a

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

case hv.a

⊢ (fun n => (sqrt 5)⁻¹ * ψ ^ n) ∈ LinearRecurrence.solSpace fibRec
case hv

⊢ LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
apply (@fibRec ℝ _).solSpace.sub_mem
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n) x✝
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
convert this
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = (sqrt 5)⁻¹ * φ ^ x✝ - (sqrt 5)⁻¹ * ψ ^ x✝
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n) x✝
rw [Pi.sub_apply]
no goals
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = (sqrt 5)⁻¹ * φ ^ x✝ - (sqrt 5)⁻¹ * ψ ^ x✝
ring
no goals
case hv.a

⊢ (fun n => (sqrt 5)⁻¹ * φ ^ n) ∈ LinearRecurrence.solSpace fibRec
exact Submodule.smul_mem fibRec.solSpace (Real.sqrt 5)⁻¹ geom_gold_isSol_fibRec
no goals
case hv.a

⊢ (fun n => (sqrt 5)⁻¹ * ψ ^ n) ∈ LinearRecurrence.solSpace fibRec
exact Submodule.smul_mem fibRec.solSpace (Real.sqrt 5)⁻¹ geom_goldConj_isSol_fibRec