-- Mathlib/Algebra/LinearRecurrence.lean
theorem eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : Fin E.order → α} (h : E.IsSolution u)
    (heq : ∀ n : Fin E.order, u n = init n) : ∀ n, u n = E.mkSol init n

Proof state:
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution 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
⊢ E.coeffs k * E.mkSol init (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
simp

Result:
no goals

Proof state:
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution 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
⊢ E.coeffs k * u (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
rw [eq_mk_of_is_sol_of_eq_init h heq (n - E.order + k)]

Result:
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution 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
⊢ E.coeffs k * E.mkSol init (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Proof state:
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k : Fin E.order,
      let_fun x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
dsimp only

Result:
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n = ∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + ↑k)

Proof state:
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.coeffs k * u (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
have : n - E.order + k < n := by omega

Result:
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution 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
⊢ E.coeffs k * u (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Proof state:
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n = ∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
rw [← tsub_add_cancel_of_le (le_of_not_lt h'), h (n - E.order)]

Result:
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i : Fin E.order, E.coeffs i * u (n - E.order + ↑i) =
    ∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Proof state:
case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ ∑ i : Fin E.order, E.coeffs i * u (n - E.order + ↑i) =
    ∑ k : Fin E.order, E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Tactic:
congr with k

Result:
case neg.e_f.h
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ E.coeffs k * u (n - E.order + ↑k) = E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + ↑k)

Proof state:
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : n < E.order
⊢ u n = init ⟨n, h'⟩

Tactic:
exact mod_cast heq ⟨n, h'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
⊢ ∀ (n : ℕ), u n = E.mkSol init n

Tactic:
intro n

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n = E.mkSol init n

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
⊢ n - E.order + ↑k < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n = E.mkSol init n

Tactic:
rw [mkSol]

Result:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k : Fin E.order,
        let_fun x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + ↑k)

Proof state:
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
⊢ u n =
    if h : n < E.order then init ⟨n, h⟩
    else
      ∑ k : Fin E.order,
        let_fun x := ⋯;
        E.coeffs k * E.mkSol init (n - E.order + ↑k)

Tactic:
split_ifs with h'

Result:
case pos
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : n < E.order
⊢ u n = init ⟨n, h'⟩

case neg
α : Type u_1
inst✝ : CommSemiring α
E : LinearRecurrence α
u : ℕ → α
init : Fin E.order → α
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u ↑n = init n
n : ℕ
h' : ¬n < E.order
⊢ u n =
    ∑ k : Fin E.order,
      let_fun x := ⋯;
      E.coeffs k * E.mkSol init (n - E.order + ↑k)