awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
h' : ¬n < E.order
neg :
  ∀ (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 : ℕ))
⊢ Eq.{u_1 + 1} (α := R) (∑ 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
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
n : ℕ
h' : ¬n < E.order
k : Fin E.order
neg :
  E.coeffs k * E.mkSol init (n - E.order + (↑k : ℕ)) =
    E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ))
⊢ 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)]

Premises used: HSub.hSub, Fin.val, HAdd.hAdd, LinearRecurrence.order
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
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 * E.mkSol init (n - E.order + (↑k : ℕ)) =
    E.coeffs k * E.mkSol init (n - E.order + E.order - E.order + (↑k : ℕ))

Tactic:
simp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
init : Fin E.order → R
h : E.IsSolution u
heq : ∀ (n : Fin E.order), u (↑n : ℕ) = init n
⊢ u = E.mkSol init

Tactic:
funext (E.eq_mk_of_is_sol_of_eq_init h heq)

Premises used: funext, LinearRecurrence.eq_mk_of_is_sol_of_eq_init
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : Membership.mem (γ := Set (ℕ → R)) {u : ℕ → R | E.IsSolution u} u
hv : Membership.mem (γ := Set (ℕ → R)) {u : ℕ → R | E.IsSolution u} v
n : ℕ
⊢ (u + v) (n + E.order) = ∑ i : Fin E.order, E.coeffs i * (u + v) (n + (↑i : ℕ))

Tactic:
simp [mul_add, sum_add_distrib, hu n, hv n]

Premises used: Finset.sum_add_distrib, mul_add
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (0 (n + E.order)) (∑ i : Fin E.order, E.coeffs i * 0 (n + (↑i : ℕ)))

Tactic:
simp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
a : R
u : ℕ → R
hu : Membership.mem (γ := Set (ℕ → R)) {u : ℕ → R | E.IsSolution u} u
n : ℕ
simp :
  Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, a * (E.coeffs i * u (n + (↑i : ℕ))))
    (∑ x : Fin E.order, E.coeffs x * (a * u (n + (↑x : ℕ))))
⊢ (a • u) (n + E.order) = ∑ i : Fin E.order, E.coeffs i * (a • u) (n + (↑i : ℕ))

Tactic:
simp [hu n, mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
a : R
u : ℕ → R
hu : Membership.mem (γ := Set (ℕ → R)) {u : ℕ → R | E.IsSolution u} u
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, a * (E.coeffs i * u (n + (↑i : ℕ))))
    (∑ x : Fin E.order, E.coeffs x * (a * u (n + (↑x : ℕ))))

Tactic:
ac_rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ℕ → R
⊢ E.IsSolution u ↔ u ∈ E.solSpace

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, LinearRecurrence.IsSolution
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
h :
  ∀ (x : Fin E.order),
    (↑(u + v) : ℕ → R) (↑x : ℕ) =
      HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R) (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ))
        (fun (x : Fin E.order) ↦ (↑v : ℕ → R) (↑x : ℕ)) x
⊢ (fun (x : Fin E.order) ↦ (↑(u + v) : ℕ → R) (↑x : ℕ)) =
    HAdd.hAdd (α := Fin E.order → R) (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) fun (x : Fin E.order) ↦
      (↑v : ℕ → R) (↑x : ℕ)

Tactic:
ext
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ↥E.solSpace
x : Fin E.order
⊢ (↑(u + v) : ℕ → R) (↑x : ℕ) =
    HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R) (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ))
      (fun (x : Fin E.order) ↦ (↑v : ℕ → R) (↑x : ℕ)) x

Tactic:
simp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
h :
  ∀ (x : Fin E.order),
    (↑(a • u) : ℕ → R) (↑x : ℕ) =
      HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) a : R)
        (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) x
⊢ (fun (x : Fin E.order) ↦ (↑(a • u) : ℕ → R) (↑x : ℕ)) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) a : R) fun (x : Fin E.order) ↦
      (↑u : ℕ → R) (↑x : ℕ)

Tactic:
ext
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
a : R
u : ↥E.solSpace
x : Fin E.order
⊢ (↑(a • u) : ℕ → R) (↑x : ℕ) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) a : R)
      (fun (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) x

Tactic:
simp
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
a :
  ∀ (n : ℕ),
    (↑((fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) ⋯)
              ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u)) :
          ℕ → R)
        n =
      (↑u : ℕ → R) n
⊢ (fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) ⋯)
      ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u) =
    u

Tactic:
ext n
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
a :
  (↑u : ℕ → R) n =
    (↑((fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) ⋯)
            ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u)) :
        ℕ → R)
      n
⊢ (↑((fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) ⋯)
            ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u)) :
        ℕ → R)
      n =
    (↑u : ℕ → R) n

Tactic:
symm
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
a : ∀ (n : Fin E.order), (↑u : ℕ → R) (↑n : ℕ) = (fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u n
⊢ (↑u : ℕ → R) n =
    (↑((fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) ⋯)
            ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u)) :
        ℕ → R)
      n

Tactic:
apply E.eq_mk_of_is_sol_of_eq_init u.2

Premises used: LinearRecurrence.eq_mk_of_is_sol_of_eq_init, Subtype.property
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : ℕ
k : Fin E.order
⊢ (↑u : ℕ → R) (↑k : ℕ) = (fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u k

Tactic:
rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
⊢ Function.Injective E.mkSol

Tactic:
Subtype.val_injective.comp E.toInit.symm.injective

Premises used: LinearEquiv.symm, Subtype.val_injective, WellFounded.Nat.fix, WellFounded.Nat.fix.go, Function.Injective.comp, LinearRecurrence.toInit, LinearEquiv.injective
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
⊢ Eq (α := Fin E.order →₀ R) ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) u : Fin E.order →₀ R)
    (Finsupp.ofSupportFinite ((↑u : ℕ → R) ∘ Fin.val) ⋯ : Fin E.order →₀ R)

Tactic:
rfl

Premises used: Finsupp.ofSupportFinite, rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
n : Fin E.order
⊢ (((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) u : Fin E.order →₀ R) : (a : Fin E.order) → R) n =
    (↑u : ℕ → R) (↑n : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : E.IsSolution u
hv : E.IsSolution v
⊢ u ∈ E.solSpace

Tactic:
replace hu : u ∈ E.solSpace := (is_sol_iff_mem_solSpace _ _).mp hu
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hv : E.IsSolution v
hu : u ∈ E.solSpace
⊢ v ∈ E.solSpace

Tactic:
replace hv : v ∈ E.solSpace := (is_sol_iff_mem_solSpace _ _).mp hv
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
rw :
  Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R) ↔
    Set.EqOn u v (↑(range E.order) : Set ℕ)
⊢ u = v ↔ Set.EqOn u v (↑(range E.order) : Set ℕ)

Tactic:
rw [← Subtype.mk.injEq u hu v hv, ← E.basis.repr.injective.eq_iff]

Premises used: Function.Injective.eq_iff, Module.Basis.repr, Subtype.mk.injEq, LinearRecurrence.basis, LinearEquiv.injective
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
mp :
  Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R) →
    Set.EqOn u v (↑(range E.order) : Set ℕ)
mpr :
  Set.EqOn u v (↑(range E.order) : Set ℕ) →
    Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R)
⊢ Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R) ↔
    Set.EqOn u v (↑(range E.order) : Set ℕ)

Tactic:
constructor
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R) →
    Set.EqOn u v (↑(range E.order) : Set ℕ)

Tactic:
fun h n hn ↦ congr($h ⟨n, Finset.mem_range.mp hn⟩)

Premises used: congrArg, Fin.mk, id, Finset.mem_range, Set.EqOn, Iff.mp, DFunLike.coe
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R) →
    Set.EqOn u v (↑(range E.order) : Set ℕ)

Tactic:
exact fun h n hn ↦ congr($h ⟨n, Finset.mem_range.mp hn⟩)
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Set.EqOn u v (↑(range E.order) : Set ℕ) →
    Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R)

Tactic:
fun h ↦ Finsupp.ext fun n ↦ h <| Finset.mem_range.mpr n.prop

Premises used: Iff.mpr, Finsupp.ext, Fin.prop, Finset.mem_range
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ Set.EqOn u v (↑(range E.order) : Set ℕ) →
    Eq (α := Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) u hu) :
        Fin E.order →₀ R)
      ((E.basis.repr : (a : ↥E.solSpace) → Fin E.order →₀ R) (Subtype.mk (p := Membership.mem E.solSpace) v hv) :
        Fin E.order →₀ R)

Tactic:
exact fun h ↦ Finsupp.ext fun n ↦ h <| Finset.mem_range.mpr n.prop

Premises used: Finsupp.ext
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
h :
  ∀ (i : Fin E.order),
    (if h : (↑i : ℕ) + 1 < E.order then (x + y) ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * (x + y) i) =
      HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then x (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order)
          else ∑ i : Fin E.order, E.coeffs i * x i)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order)
          else ∑ i : Fin E.order, E.coeffs i * y i)
        i
⊢ (fun (i : Fin E.order) ↦
      if h : (↑i : ℕ) + 1 < E.order then (x + y) ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * (x + y) i) =
    HAdd.hAdd (α := Fin E.order → R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then x (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * x i)
      fun (i : Fin E.order) ↦
      if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * y i

Tactic:
ext i
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
pos :
  ∀ (h : (↑i : ℕ) + 1 < E.order),
    (x + y) (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) =
      HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then x ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * x i)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then y ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * y i)
        i
neg :
  ∀ (h : ¬(↑i : ℕ) + 1 < E.order),
    ∑ i : Fin E.order, E.coeffs i * (x + y) i =
      HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then x (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order)
          else ∑ i : Fin E.order, E.coeffs i * x i)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order)
          else ∑ i : Fin E.order, E.coeffs i * y i)
        i
⊢ (if h : (↑i : ℕ) + 1 < E.order then (x + y) ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * (x + y) i) =
    HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then x (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * x i)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * y i)
      i

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : (↑i : ℕ) + 1 < E.order
⊢ (x + y) (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) =
    HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then x ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * x i)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then y ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * y i)
      i

Tactic:
simp [h, mul_add, sum_add_distrib]

Premises used: Finset.sum_add_distrib, mul_add
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
i : Fin E.order
h : ¬(↑i : ℕ) + 1 < E.order
⊢ ∑ i : Fin E.order, E.coeffs i * (x + y) i =
    HAdd.hAdd (α := Fin E.order → R) (β := Fin E.order → R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then x (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * x i)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * y i)
      i

Tactic:
simp [h, mul_add, sum_add_distrib]

Premises used: Finset.sum_add_distrib, mul_add
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
h :
  ∀ (i : Fin E.order),
    (if h : (↑i : ℕ) + 1 < E.order then (x • y) ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * (x • y) i) =
      HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order)
          else ∑ i : Fin E.order, E.coeffs i * y i)
        i
⊢ (fun (i : Fin E.order) ↦
      if h : (↑i : ℕ) + 1 < E.order then (x • y) ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * (x • y) i) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R) fun (i : Fin E.order) ↦
      if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * y i

Tactic:
ext i
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
i : Fin E.order
pos :
  ∀ (h : (↑i : ℕ) + 1 < E.order),
    (x • y) (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) =
      HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then y ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * y i)
        i
neg :
  ∀ (h : ¬(↑i : ℕ) + 1 < E.order),
    ∑ i : Fin E.order, E.coeffs i * (x • y) i =
      HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R)
        (fun (i : Fin E.order) ↦
          if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order)
          else ∑ i : Fin E.order, E.coeffs i * y i)
        i
⊢ (if h : (↑i : ℕ) + 1 < E.order then (x • y) ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * (x • y) i) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * y i)
      i

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
i : Fin E.order
h : (↑i : ℕ) + 1 < E.order
⊢ (x • y) (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then y ⟨(↑i : ℕ) + 1, h⟩ else ∑ i : Fin E.order, E.coeffs i * y i)
      i

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, h, ↓reduceDIte, mul_sum]

Premises used: Finset.mul_sum, RingHom.id_apply, reduceDIte, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
i : Fin E.order
h : ¬(↑i : ℕ) + 1 < E.order
neg :
  Eq.{u_1 + 1} (α := R) (∑ x_1 : Fin E.order, E.coeffs x_1 * (x * y x_1)) (∑ i : Fin E.order, x * (E.coeffs i * y i))
⊢ ∑ i : Fin E.order, E.coeffs i * (x • y) i =
    HSMul.hSMul (α := R) (β := Fin E.order → R) ((RingHom.id R : (a : R) → R) x : R)
      (fun (i : Fin E.order) ↦
        if h : (↑i : ℕ) + 1 < E.order then y (⟨(↑i : ℕ) + 1, h⟩ : Fin E.order) else ∑ i : Fin E.order, E.coeffs i * y i)
      i

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, h, ↓reduceDIte, mul_sum]

Premises used: Finset.mul_sum, RingHom.id_apply, reduceDIte, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x_1 : R
y : Fin E.order → R
i : Fin E.order
h : ¬(↑i : ℕ) + 1 < E.order
x : Fin E.order
h_1 : Membership.mem (γ := Finset (Fin E.order)) univ x
⊢ E.coeffs x * (x_1 * y x) = x_1 * (E.coeffs x * y x)

Tactic:
ac_rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
i : Fin E.order
h : ¬(↑i : ℕ) + 1 < E.order
⊢ Eq.{u_1 + 1} (α := R) (∑ x_1 : Fin E.order, E.coeffs x_1 * (x * y x_1)) (∑ i : Fin E.order, x * (E.coeffs i * y i))

Tactic:
exact sum_congr rfl fun x _ ↦ by ac_rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
inst_1 : StrongRankCondition R
E : LinearRecurrence R
⊢ Module.rank R ↥E.solSpace = (↑E.order : Cardinal.{u_1})

Tactic:
simp [rank_eq_card_basis E.basis]

Premises used: rank_eq_card_basis, LinearRecurrence.basis
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
rw : degree.{u_1} (R := R) ((monomial E.order : (a : R) → R[X]) 1) = (↑E.order : WithBot ℕ)
rw₁ :
  degree.{u_1} (R := R) (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i)) <
    degree.{u_1} (R := R) ((monomial E.order : (a : R) → R[X]) 1)
⊢ E.charPoly.degree = (↑E.order : WithBot ℕ)

Tactic:
rw [charPoly, degree_sub_eq_left_of_degree_lt]

Premises used: Polynomial.degree_sub_eq_left_of_degree_lt, LinearRecurrence.charPoly
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
rw rw₁ : Eq (α := WithBot ℕ) (↑E.order : WithBot ℕ) (↑E.order : WithBot ℕ)
⊢ degree.{u_1} (R := R) ((monomial E.order : (a : R) → R[X]) 1) = (↑E.order : WithBot ℕ)

Tactic:
rw [degree_monomial E.order one_ne_zero]

Premises used: one_ne_zero, LinearRecurrence.order, Polynomial.degree_monomial
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
rw :
  degree.{u_1} (R := R) (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i)) < (↑E.order : WithBot ℕ)
⊢ degree.{u_1} (R := R) (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i)) <
    degree.{u_1} (R := R) ((monomial E.order : (a : R) → R[X]) 1)

Tactic:
rw [degree_monomial E.order one_ne_zero]

Premises used: one_ne_zero, LinearRecurrence.order, Polynomial.degree_monomial
-- Module: Mathlib.Algebra.LinearRecurrence
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
simp_rw :
  degree.{u_1} (R := R)
      (∑ x : Fin E.order,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (E.coeffs x) : R[X]) (HPow.hPow (α := R[X]) X (↑x : ℕ))) <
    (↑E.order : WithBot ℕ)
⊢ degree.{u_1} (R := R) (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i)) < (↑E.order : WithBot ℕ)

Tactic:
simp_rw [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial