-- Mathlib/Algebra/LinearRecurrence.lean
theorem geom_sol_iff_root_charPoly (q : α) :
    (E.IsSolution fun n ↦ q ^ n) ↔ E.charPoly.IsRoot q

Proof state:
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (E.coeffs x✝¹ * q ^ ↑x✝¹) = E.coeffs x✝¹ * (q ^ n * q ^ ↑x✝¹)

Tactic:
ring

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0
n : ℕ
⊢ ∑ i : Fin E.order, q ^ n * (E.coeffs i * q ^ ↑i) = ∑ x : Fin E.order, E.coeffs x * (q ^ n * q ^ ↑x)

Tactic:
exact sum_congr rfl fun _ _ ↦ by ring

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) → q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : E.IsSolution fun n => q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0

Proof state:
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) ↔ E.charPoly.IsRoot q

Tactic:
rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]

Result:
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) ↔
    eval₂ (RingHom.id α) q ((monomial E.order) 1 - ∑ i : Fin E.order, (monomial ↑i) (E.coeffs i)) = 0

Proof state:
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0
n : ℕ
⊢ (fun n => q ^ n) (n + E.order) = ∑ i : Fin E.order, E.coeffs i * (fun n => q ^ n) (n + ↑i)

Tactic:
simp only [pow_add, sub_eq_zero.mp h, mul_sum]

Result:
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0
n : ℕ
⊢ ∑ i : Fin E.order, q ^ n * (E.coeffs i * q ^ ↑i) = ∑ x : Fin E.order, E.coeffs x * (q ^ n * q ^ ↑x)

Proof state:
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : E.IsSolution fun n => q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0

Tactic:
simpa [sub_eq_zero] using h 0

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) → q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0

case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n => q ^ n

Proof state:
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0 → E.IsSolution fun n => q ^ n

Tactic:
intro h n

Result:
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0
n : ℕ
⊢ (fun n => q ^ n) (n + E.order) = ∑ i : Fin E.order, E.coeffs i * (fun n => q ^ n) (n + ↑i)

Proof state:
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) ↔
    eval₂ (RingHom.id α) q ((monomial E.order) 1 - ∑ i : Fin E.order, (monomial ↑i) (E.coeffs i)) = 0

Tactic:
simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial,
  Polynomial.eval₂_sub]

Result:
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (E.IsSolution fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0