awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
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
have a : (↑u : ℕ → R) n =
  (↑((fun (u : Fin E.order → R) ↦ Subtype.mk (p := fun (x : ℕ → R) ↦ x ∈ E.solSpace) (E.mkSol u) sorry)
          ((fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u)) :
      ℕ → R)
    n
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u : ↥E.solSpace
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
have a : ∀ (n : Fin E.order), (↑u : ℕ → R) (↑n : ℕ) = (fun (u : ↥E.solSpace) (x : Fin E.order) ↦ (↑u : ℕ → R) (↑x : ℕ)) u n
Tactic: apply E.eq_mk_of_is_sol_of_eq_init u.2
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : E.IsSolution u
hv : E.IsSolution v
⊢ u = v ↔ Set.EqOn u v (↑(range E.order) : Set ℕ)
have hu₁ : u ∈ E.solSpace
Tactic: replace hu : u ∈ E.solSpace := (is_sol_iff_mem_solSpace _ _).mp hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hv : E.IsSolution v
hu : u ∈ E.solSpace
⊢ u = v ↔ Set.EqOn u v (↑(range E.order) : Set ℕ)
have hv₁ : v ∈ E.solSpace
Tactic: replace hv : v ∈ E.solSpace := (is_sol_iff_mem_solSpace _ _).mp hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
u v : ℕ → R
hu : u ∈ E.solSpace
hv : v ∈ E.solSpace
⊢ u = v ↔ Set.EqOn u v (↑(range E.order) : Set ℕ)
have 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 ℕ)
Tactic: rw [← Subtype.mk.injEq u hu v hv, ← E.basis.repr.injective.eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
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 ℕ)
have 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 ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
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 ℕ)
⊢ 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 ℕ)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
⊢ (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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x y : Fin E.order → R
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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
⊢ (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
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommSemiring R
E : LinearRecurrence R
x : R
y : Fin E.order → R
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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
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
⊢ ∑ 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
have 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))
Tactic: simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, h, ↓reduceDIte, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
⊢ E.charPoly.degree = (↑E.order : WithBot ℕ)
have rw : degree.{u_1} (R := R) ((monomial E.order : (a : R) → R[X]) 1) = (↑E.order : WithBot ℕ)
Tactic: rw [charPoly, degree_sub_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
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 ℕ)
⊢ E.charPoly.degree = (↑E.order : WithBot ℕ)
have 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)
Tactic: rw [charPoly, degree_sub_eq_left_of_degree_lt]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
⊢ degree.{u_1} (R := R) ((monomial E.order : (a : R) → R[X]) 1) = (↑E.order : WithBot ℕ)
have rw : Eq (α := WithBot ℕ) (↑E.order : WithBot ℕ) (↑E.order : WithBot ℕ)
Tactic: rw [degree_monomial E.order one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
⊢ 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)
have rw : degree.{u_1} (R := R) (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i)) < (↑E.order : WithBot ℕ)
Tactic: rw [degree_monomial E.order one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
inst_1 : Nontrivial R
⊢ degree.{u_1} (R := R) (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i)) < (↑E.order : WithBot ℕ)
have 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 ℕ)
Tactic: simp_rw [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
⊢ E.charPoly.Monic
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
⊢ E.charPoly.Monic
have rw : Eq.{u_1 + 1} (α := R) (∑ b : Fin E.order, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (E.coeffs b)) E.order) 0
Tactic: rw [Monic, leadingCoeff, natDegree_eq_of_degree_eq_some <| charPoly_degree_eq_order _, charPoly,
    coeff_sub, coeff_monomial_same, finsetSum_coeff, sub_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) (∑ b : Fin E.order, coeff ((monomial (↑b : ℕ) : (a : R) → R[X]) (E.coeffs b)) E.order) 0
have refine : ∀ (x : Fin E.order),
  Membership.mem (γ := Finset (Fin E.order)) univ x →
    degree.{u_1} (R := R) ((monomial (↑x : ℕ) : (a : R) → R[X]) (E.coeffs x)) < (↑E.order : WithBot ℕ)
Tactic: refine sum_eq_zero fun _ _ ↦ coeff_eq_zero_of_degree_lt ?_
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
h : Nontrivial R
x : Fin E.order
h_1 : Membership.mem (γ := Finset (Fin E.order)) univ x
⊢ degree.{u_1} (R := R) ((monomial (↑x : ℕ) : (a : R) → R[X]) (E.coeffs x)) < (↑E.order : WithBot ℕ)
have grw : LT.lt (α := WithBot ℕ) (↑(↑x : ℕ) : WithBot ℕ) (↑E.order : WithBot ℕ)
Tactic: grw [degree_monomial_le]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔
    eval₂ (RingHom.id R) q
        (HSub.hSub (α := R[X]) ((monomial E.order : (a : R) → R[X]) 1)
          (∑ i : Fin E.order, (monomial (↑i : ℕ) : (a : R) → R[X]) (E.coeffs i))) =
      0
have simp : (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
Tactic: simp only [Polynomial.eval₂_finsetSum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial,
    Polynomial.eval₂_sub]
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
⊢ (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
have mp : (E.IsSolution fun (n : ℕ) ↦ q ^ n) → q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
mp : (E.IsSolution fun (n : ℕ) ↦ q ^ n) → q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
⊢ (E.IsSolution fun (n : ℕ) ↦ q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
have mpr : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0 → E.IsSolution fun (n : ℕ) ↦ q ^ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.LinearRecurrence (goal)
Goal:
R : Type u_1
inst : CommRing R
E : LinearRecurrence R
q : R
h : q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ (↑x : ℕ) = 0
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((fun (n : ℕ) ↦ q ^ n) (n + E.order))
    (∑ i : Fin E.order, E.coeffs i * (fun (n : ℕ) ↦ q ^ n) (n + (↑i : ℕ)))
have mpr : Eq.{u_1 + 1} (α := R) (∑ i : Fin E.order, q ^ n * (E.coeffs i * q ^ (↑i : ℕ)))
  (∑ x : Fin E.order, E.coeffs x * (q ^ n * q ^ (↑x : ℕ)))
Tactic: simp only [pow_add, sub_eq_zero.mp h, mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
u : Rˣ
x : M
⊢ -u • x = -(u • x)
have rw : (↑(-u) : R) • x = -(u • x)
Tactic: rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
u : Rˣ
x : M
rw : (↑(-u) : R) • x = -(u • x)
⊢ -u • x = -(u • x)
have rw₁ : -(↑u : R) • x = -(u • x)
Tactic: rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
u : Rˣ
x : M
rw : (↑(-u) : R) • x = -(u • x)
rw₁ : -(↑u : R) • x = -(u • x)
⊢ -u • x = -(u • x)
have rw₂ : -((↑u : R) • x) = -(u • x)
Tactic: rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
u : Rˣ
x : M
rw : (↑(-u) : R) • x = -(u • x)
rw₁ : -(↑u : R) • x = -(u • x)
rw₂ : -((↑u : R) • x) = -(u • x)
⊢ -u • x = -(u • x)
have rw₃ : -((↑u : R) • x) = -((↑u : R) • x)
Tactic: rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have pos : ∀ (hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: by_cases hR : (n : R) = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
pos :
  ∀ (hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg : ∀ (hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: by_cases hR : (n : R) = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have pos : ∀ (hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: by_cases hS : (n : S) = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : Eq.{u_6 + 1} (α := R) (↑n : R) 0
pos :
  ∀ (hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0),
    (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
      HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have neg : ∀ (hS : ¬Eq.{u_7 + 1} (α := S) (↑n : S) 0),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: by_cases hS : (n : S) = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Basic (goal)
Goal:
M : Type u_3
M₂ : Type u_4
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
F : Type u_5
inst_2 : FunLike F M M₂
inst_3 : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst_4 : DivisionSemiring R
inst_5 : DivisionSemiring S
inst_6 : Module R M
inst_7 : Module S M₂
n : ℕ
x : M
hR : ¬Eq.{u_6 + 1} (α := R) (↑n : R) 0
⊢ (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
have pos : ∀ (hS : Eq.{u_7 + 1} (α := S) (↑n : S) 0),
  (f : (a : M) → M₂) (HSMul.hSMul.{u_6, u_3, u_3} (α := R) (↑n : R)⁻¹ x) =
    HSMul.hSMul.{u_7, u_4, u_4} (α := S) (β := M₂) (↑n : S)⁻¹ ((f : (a : M) → M₂) x : M₂)
Tactic: by_cases hS : (n : S) = 0