α : Type ?u.41184
inst✝¹ : CommSemiring α
β : Type u_1
inst✝ : CommRing β
⊢ (↑(monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      Finset.sum Finset.univ fun i => ↑(monomial ↑i) (LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i)) =
    X ^ 2 - (X + 1)
α : Type ?u.41184
inst✝¹ : CommSemiring α
β : Type u_1
inst✝ : CommRing β
⊢ LinearRecurrence.charPoly fibRec = X ^ 2 - (X + 1)
rw [fibRec, LinearRecurrence.charPoly]
no goals
α : Type ?u.41184
inst✝¹ : CommSemiring α
β : Type u_1
inst✝ : CommRing β
⊢ (↑(monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      Finset.sum Finset.univ fun i => ↑(monomial ↑i) (LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i)) =
    X ^ 2 - (X + 1)
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]