[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n
[PROOFSTEP]
rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h), tsub_lt_iff_left]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ ↑k + n < E.order + n
[PROOFSTEP]
exact add_lt_add_right k.is_lt n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ E.order ≤ ↑k + n
[PROOFSTEP]
convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h)
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
x✝ : ℕ
n : ℕ := x✝
h : ¬n < E.order
k : Fin E.order
⊢ E.order = 0 + E.order
[PROOFSTEP]
simp only [zero_add]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ IsSolution E (mkSol E init)
[PROOFSTEP]
intro n
[GOAL]
α : 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)
[PROOFSTEP]
rw [mkSol]
[GOAL]
α : 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)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
⊢ ∀ (n : Fin E.order), mkSol E init ↑n = init n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ mkSol E init ↑n = init n
[PROOFSTEP]
rw [mkSol]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
init : Fin E.order → α
n : Fin E.order
⊢ (if h : ↑n < E.order then init { val := ↑n, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : ↑n - E.order + ↑k < ↑n);
        coeffs E k * mkSol E init (↑n - E.order + ↑k)) =
    init n
[PROOFSTEP]
simp only [n.is_lt, dif_pos, Fin.mk_val, Fin.eta]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
⊢ ∀ (n : ℕ), u n = mkSol E init n
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n = mkSol E init n
[PROOFSTEP]
rw [mkSol]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init { val := n, isLt := h }
    else
      ∑ k : Fin E.order,
        let_fun x := (_ : n - E.order + ↑k < n);
        coeffs E k * mkSol E init (n - E.order + ↑k)
[PROOFSTEP]
split_ifs with h'
[GOAL]
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : n < E.order
⊢ u n = init { val := n, isLt := h' }
[PROOFSTEP]
exact_mod_cast heq ⟨n, h'⟩
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k : Fin E.order,
      let_fun x := (_ : n - E.order + ↑k < n);
      coeffs E k * mkSol E init (n - E.order + ↑k)
[PROOFSTEP]
simp only
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n = ∑ x : Fin E.order, coeffs E x * mkSol E init (n - E.order + ↑x)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i : Fin E.order, coeffs E i * u (n - E.order + ↑i) =
    ∑ x : Fin E.order, coeffs E x * mkSol E init (n - E.order + E.order - E.order + ↑x)
[PROOFSTEP]
congr with k
[GOAL]
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ coeffs E k * u (n - E.order + ↑k) = coeffs E k * mkSol E init (n - E.order + E.order - E.order + ↑k)
[PROOFSTEP]
have : n - E.order + k < n :=
  by
  rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h'), tsub_lt_iff_left]
  · exact add_lt_add_right k.is_lt n
  · convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h')
    simp only [zero_add]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n
[PROOFSTEP]
rw [add_comm, ← add_tsub_assoc_of_le (not_lt.mp h'), tsub_lt_iff_left]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ ↑k + n < E.order + n
[PROOFSTEP]
exact add_lt_add_right k.is_lt n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.order ≤ ↑k + n
[PROOFSTEP]
convert add_le_add (zero_le (k : ℕ)) (not_lt.mp h')
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.order = 0 + E.order
[PROOFSTEP]
simp only [zero_add]
[GOAL]
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
this : n - E.order + ↑k < n
⊢ coeffs E k * u (n - E.order + ↑k) = coeffs E k * mkSol E init (n - E.order + E.order - E.order + ↑k)
[PROOFSTEP]
rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]
[GOAL]
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : IsSolution E u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
this : n - E.order + ↑k < n
⊢ coeffs E k * mkSol E (fun n => init n) (n - E.order + ↑k) =
    coeffs E k * mkSol E init (n - E.order + E.order - E.order + ↑k)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : u ∈ {u | IsSolution E u}
hv : v ∈ {u | IsSolution E u}
n : ℕ
⊢ (u + v) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)
[PROOFSTEP]
simp [mul_add, sum_add_distrib, hu n, hv n]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
n : ℕ
⊢ OfNat.ofNat 0 (n + E.order) = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
⊢ (a • u) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (a • u) (n + ↑i)
[PROOFSTEP]
simp [hu n, mul_sum]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
⊢ ∑ x : Fin E.order, a * (coeffs E x * u (n + ↑x)) = ∑ x : Fin E.order, coeffs E x * (a * u (n + ↑x))
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
⊢ (fun x => a * (coeffs E x * u (n + ↑x))) = fun x => coeffs E x * (a * u (n + ↑x))
[PROOFSTEP]
ext
[GOAL]
case e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : ℕ → α
hu :
  u ∈
    {
          toAddSubsemigroup :=
            { carrier := {u | IsSolution E u},
              add_mem' :=
                (_ :
                  ∀ {u v : ℕ → α},
                    u ∈ {u | IsSolution E u} →
                      v ∈ {u | IsSolution E u} →
                        ∀ (n : ℕ),
                          u (n + E.order) + v (n + E.order) = ∑ i : Fin E.order, coeffs E i * (u + v) (n + ↑i)) },
          zero_mem' :=
            (_ : ∀ (n : ℕ), 0 = ∑ i : Fin E.order, coeffs E i * OfNat.ofNat 0 (n + ↑i)) }.toAddSubsemigroup.carrier
n : ℕ
x✝ : Fin E.order
⊢ a * (coeffs E x✝ * u (n + ↑x✝)) = coeffs E x✝ * (a * u (n + ↑x✝))
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : { x // x ∈ solSpace E }
⊢ (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : { x // x ∈ solSpace E }
x✝ : Fin E.order
⊢ (fun u x => ↑u ↑x) (u + v) x✝ = ((fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : { x // x ∈ solSpace E }
⊢ AddHom.toFun
      { toFun := fun u x => ↑u ↑x,
        map_add' :=
          (_ :
            ∀ (u v : { x // x ∈ solSpace E }),
              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
      (a • u) =
    ↑(RingHom.id α) a •
      AddHom.toFun
        { toFun := fun u x => ↑u ↑x,
          map_add' :=
            (_ :
              ∀ (u v : { x // x ∈ solSpace E }),
                (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
        u
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
a : α
u : { x // x ∈ solSpace E }
x✝ : Fin E.order
⊢ AddHom.toFun
      { toFun := fun u x => ↑u ↑x,
        map_add' :=
          (_ :
            ∀ (u v : { x // x ∈ solSpace E }),
              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
      (a • u) x✝ =
    (↑(RingHom.id α) a •
        AddHom.toFun
          { toFun := fun u x => ↑u ↑x,
            map_add' :=
              (_ :
                ∀ (u v : { x // x ∈ solSpace E }),
                  (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
          u)
      x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
⊢ (fun u => { val := mkSol E u, property := (_ : IsSolution E (mkSol E u)) })
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun u x => ↑u ↑x,
                map_add' :=
                  (_ :
                    ∀ (u v : { x // x ∈ solSpace E }),
                      (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
            map_smul' :=
              (_ :
                ∀ (a : α) (u : { x // x ∈ solSpace E }),
                  AddHom.toFun
                      { toFun := fun u x => ↑u ↑x,
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ solSpace E }),
                              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                      (a • u) =
                    ↑(RingHom.id α) a •
                      AddHom.toFun
                        { toFun := fun u x => ↑u ↑x,
                          map_add' :=
                            (_ :
                              ∀ (u v : { x // x ∈ solSpace E }),
                                (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                        u) }.toAddHom
        u) =
    u
[PROOFSTEP]
ext n
[GOAL]
case a.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
⊢ ↑((fun u => { val := mkSol E u, property := (_ : IsSolution E (mkSol E u)) })
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun u x => ↑u ↑x,
                    map_add' :=
                      (_ :
                        ∀ (u v : { x // x ∈ solSpace E }),
                          (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
                map_smul' :=
                  (_ :
                    ∀ (a : α) (u : { x // x ∈ solSpace E }),
                      AddHom.toFun
                          { toFun := fun u x => ↑u ↑x,
                            map_add' :=
                              (_ :
                                ∀ (u v : { x // x ∈ solSpace E }),
                                  (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                          (a • u) =
                        ↑(RingHom.id α) a •
                          AddHom.toFun
                            { toFun := fun u x => ↑u ↑x,
                              map_add' :=
                                (_ :
                                  ∀ (u v : { x // x ∈ solSpace E }),
                                    (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                            u) }.toAddHom
            u))
      n =
    ↑u n
[PROOFSTEP]
symm
[GOAL]
case a.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
⊢ ↑u n =
    ↑((fun u => { val := mkSol E u, property := (_ : IsSolution E (mkSol E u)) })
          (AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun u x => ↑u ↑x,
                    map_add' :=
                      (_ :
                        ∀ (u v : { x // x ∈ solSpace E }),
                          (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
                map_smul' :=
                  (_ :
                    ∀ (a : α) (u : { x // x ∈ solSpace E }),
                      AddHom.toFun
                          { toFun := fun u x => ↑u ↑x,
                            map_add' :=
                              (_ :
                                ∀ (u v : { x // x ∈ solSpace E }),
                                  (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                          (a • u) =
                        ↑(RingHom.id α) a •
                          AddHom.toFun
                            { toFun := fun u x => ↑u ↑x,
                              map_add' :=
                                (_ :
                                  ∀ (u v : { x // x ∈ solSpace E }),
                                    (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                            u) }.toAddHom
            u))
      n
[PROOFSTEP]
apply E.eq_mk_of_is_sol_of_eq_init u.2
[GOAL]
case a.h.heq
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
⊢ ∀ (n : Fin E.order),
    ↑u ↑n =
      AddHom.toFun
        {
            toAddHom :=
              { toFun := fun u x => ↑u ↑x,
                map_add' :=
                  (_ :
                    ∀ (u v : { x // x ∈ solSpace E }),
                      (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
            map_smul' :=
              (_ :
                ∀ (a : α) (u : { x // x ∈ solSpace E }),
                  AddHom.toFun
                      { toFun := fun u x => ↑u ↑x,
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ solSpace E }),
                              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                      (a • u) =
                    ↑(RingHom.id α) a •
                      AddHom.toFun
                        { toFun := fun u x => ↑u ↑x,
                          map_add' :=
                            (_ :
                              ∀ (u v : { x // x ∈ solSpace E }),
                                (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                        u) }.toAddHom
        u n
[PROOFSTEP]
intro k
[GOAL]
case a.h.heq
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : { x // x ∈ solSpace E }
n : ℕ
k : Fin E.order
⊢ ↑u ↑k =
    AddHom.toFun
      {
          toAddHom :=
            { toFun := fun u x => ↑u ↑x,
              map_add' :=
                (_ :
                  ∀ (u v : { x // x ∈ solSpace E }),
                    (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) },
          map_smul' :=
            (_ :
              ∀ (a : α) (u : { x // x ∈ solSpace E }),
                AddHom.toFun
                    { toFun := fun u x => ↑u ↑x,
                      map_add' :=
                        (_ :
                          ∀ (u v : { x // x ∈ solSpace E }),
                            (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                    (a • u) =
                  ↑(RingHom.id α) a •
                    AddHom.toFun
                      { toFun := fun u x => ↑u ↑x,
                        map_add' :=
                          (_ :
                            ∀ (u v : { x // x ∈ solSpace E }),
                              (fun u x => ↑u ↑x) (u + v) = (fun u x => ↑u ↑x) u + (fun u x => ↑u ↑x) v) }
                      u) }.toAddHom
      u k
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
⊢ u = v ↔ Set.EqOn u v ↑(range E.order)
[PROOFSTEP]
refine' Iff.intro (fun h x _ ↦ h ▸ rfl) _
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
⊢ Set.EqOn u v ↑(range E.order) → u = v
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
⊢ u = v
[PROOFSTEP]
set u' : ↥E.solSpace := ⟨u, hu⟩
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
⊢ u = v
[PROOFSTEP]
set v' : ↥E.solSpace := ⟨v, hv⟩
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ u = v
[PROOFSTEP]
change u'.val = v'.val
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ ↑u' = ↑v'
[PROOFSTEP]
suffices h' : u' = v'
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
h' : u' = v'
⊢ ↑u' = ↑v'
case h'
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ u' = v'
[PROOFSTEP]
exact h' ▸ rfl
[GOAL]
case h'
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ u' = v'
[PROOFSTEP]
rw [← E.toInit.toEquiv.apply_eq_iff_eq, LinearEquiv.coe_toEquiv]
[GOAL]
case h'
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
⊢ ↑(toInit E) u' = ↑(toInit E) v'
[PROOFSTEP]
ext x
[GOAL]
case h'.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u v : ℕ → α
hu : IsSolution E u
hv : IsSolution E v
h : Set.EqOn u v ↑(range E.order)
u' : { x // x ∈ solSpace E } := { val := u, property := hu }
v' : { x // x ∈ solSpace E } := { val := v, property := hv }
x : Fin E.order
⊢ ↑(toInit E) u' x = ↑(toInit E) v' x
[PROOFSTEP]
exact_mod_cast h (mem_range.mpr x.2)
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
⊢ (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
      (x + y) =
    (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
        x +
      (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
        y
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
⊢ (fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
      (x + y) i =
    ((fun X i => if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
          x +
        (fun X i =>
            if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i)
          y)
      i
[PROOFSTEP]
simp only
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
⊢ (if h : ↑i + 1 < E.order then (x + y) { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * (x + y) i) =
    ((fun i => if h : ↑i + 1 < E.order then x { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * x i) +
        fun i => if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x + y) { val := ↑i + 1, isLt := h } =
    ((fun i => if h : ↑i + 1 < E.order then x { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * x i) +
        fun i => if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_add, sum_add_distrib]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ i : Fin E.order, coeffs E i * (x + y) i =
    ((fun i => if h : ↑i + 1 < E.order then x { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * x i) +
        fun i => if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_add, sum_add_distrib]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
⊢ AddHom.toFun
      {
        toFun := fun X i =>
          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
        map_add' :=
          (_ :
            ∀ (x y : Fin E.order → α),
              (fun X i =>
                    if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                    else ∑ i : Fin E.order, coeffs E i * X i)
                  (x + y) =
                (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    x +
                  (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    y) }
      (x • y) =
    ↑(RingHom.id α) x •
      AddHom.toFun
        {
          toFun := fun X i =>
            if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
          map_add' :=
            (_ :
              ∀ (x y : Fin E.order → α),
                (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    (x + y) =
                  (fun X i =>
                        if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                        else ∑ i : Fin E.order, coeffs E i * X i)
                      x +
                    (fun X i =>
                        if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                        else ∑ i : Fin E.order, coeffs E i * X i)
                      y) }
        y
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
⊢ AddHom.toFun
      {
        toFun := fun X i =>
          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
        map_add' :=
          (_ :
            ∀ (x y : Fin E.order → α),
              (fun X i =>
                    if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                    else ∑ i : Fin E.order, coeffs E i * X i)
                  (x + y) =
                (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    x +
                  (fun X i =>
                      if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                      else ∑ i : Fin E.order, coeffs E i * X i)
                    y) }
      (x • y) i =
    (↑(RingHom.id α) x •
        AddHom.toFun
          {
            toFun := fun X i =>
              if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * X i,
            map_add' :=
              (_ :
                ∀ (x y : Fin E.order → α),
                  (fun X i =>
                        if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                        else ∑ i : Fin E.order, coeffs E i * X i)
                      (x + y) =
                    (fun X i =>
                          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                          else ∑ i : Fin E.order, coeffs E i * X i)
                        x +
                      (fun X i =>
                          if h : ↑i + 1 < E.order then X { val := ↑i + 1, isLt := h }
                          else ∑ i : Fin E.order, coeffs E i * X i)
                        y) }
          y)
      i
[PROOFSTEP]
simp only
[GOAL]
case h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
⊢ (if h : ↑i + 1 < E.order then (x • y) { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * (x • y) i) =
    (↑(RingHom.id α) x • fun i =>
        if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
h : ↑i + 1 < E.order
⊢ (x • y) { val := ↑i + 1, isLt := h } =
    (↑(RingHom.id α) x • fun i =>
        if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_sum]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ i : Fin E.order, coeffs E i * (x • y) i =
    (↑(RingHom.id α) x • fun i =>
        if h : ↑i + 1 < E.order then y { val := ↑i + 1, isLt := h } else ∑ i : Fin E.order, coeffs E i * y i)
      i
[PROOFSTEP]
simp [h, mul_sum]
[GOAL]
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x : α
y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
⊢ ∑ x_1 : Fin E.order, coeffs E x_1 * (x * y x_1) = ∑ x_1 : Fin E.order, x * (coeffs E x_1 * y x_1)
[PROOFSTEP]
exact sum_congr rfl fun x _ ↦ by ac_rfl
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
x✝¹ : α
y : Fin E.order → α
i : Fin E.order
h : ¬↑i + 1 < E.order
x : Fin E.order
x✝ : x ∈ univ
⊢ coeffs E x * (x✝¹ * y x) = x✝¹ * (coeffs E x * y x)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ IsRoot (charPoly E) q
[PROOFSTEP]
rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔
    eval₂ (RingHom.id α) q (↑(monomial E.order) 1 - ∑ i : Fin E.order, ↑(monomial ↑i) (coeffs E i)) = 0
[PROOFSTEP]
simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial, Polynomial.eval₂_sub]
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) → q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : IsSolution E fun n => q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
[PROOFSTEP]
simpa [sub_eq_zero] using h 0
[GOAL]
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0 → IsSolution E fun n => q ^ n
[PROOFSTEP]
intro h n
[GOAL]
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ (fun n => q ^ n) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (fun n => q ^ n) (n + ↑i)
[PROOFSTEP]
simp only [pow_add, sub_eq_zero.mp h, mul_sum]
[GOAL]
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ ∑ x : Fin E.order, q ^ n * (coeffs E x * q ^ ↑x) = ∑ x : Fin E.order, coeffs E x * (q ^ n * q ^ ↑x)
[PROOFSTEP]
exact sum_congr rfl fun _ _ ↦ by ring
[GOAL]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (coeffs E x✝¹ * q ^ ↑x✝¹) = coeffs E x✝¹ * (q ^ n * q ^ ↑x✝¹)
[PROOFSTEP]
ring
