α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ mkSol E init (n + E.order) = ∑ i : Fin E.order, coeffs E i * mkSol E init (n + ↑i)
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ IsSolution E (mkSol E init)
intro n
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ (if h : n + E.order < E.order then init { val := n + E.order, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : n + E.order - E.order + ↑k < n + E.order);
        coeffs E k * mkSol E init (n + E.order - E.order + ↑k)) =
    ∑ i : Fin E.order, coeffs E i * mkSol E init (n + ↑i)
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ mkSol E init (n + E.order) = ∑ i : Fin E.order, coeffs E i * mkSol E init (n + ↑i)
rw [mkSol]
no goals
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : ℕ
⊢ (if h : n + E.order < E.order then init { val := n + E.order, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : n + E.order - E.order + ↑k < n + E.order);
        coeffs E k * mkSol E init (n + E.order - E.order + ↑k)) =
    ∑ i : Fin E.order, coeffs E i * mkSol E init (n + ↑i)
simp