awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P ≠ 0
h_deg_mul : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).natDegree = P.natDegree + 1
d : ℕ
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul :
  (SignType.sign : (a : R) → SignType)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff =
    s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC :
  Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).leadingCoeff :
      SignType)
    (1 : SignType)
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : Eq (α := SignType) ((SignType.sign : (a : R) → SignType) P.nextCoeff : SignType) (-1 : SignType)
h₁ : P.nextCoeff ≠ 0
ih :
  P.eraseLead.signVariations + 1 ≤
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P.eraseLead).signVariations
this : P.signVariations = P.eraseLead.signVariations + 1
⊢ Eq (α := SignType)
    ((SignType.sign : (a : R) → SignType)
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * P).nextCoeff :
      SignType)
    (-1 : SignType)

Tactic:
grind [← sign_eq_neg_one_iff, coeff_X_sub_C_mul, nextCoeff]

Premises used: Polynomial.coeff_X_sub_C_mul, Polynomial.nextCoeff, sign_eq_neg_one_iff
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
generalize :
  ∀ (num_pos_roots : ℕ) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = num_pos_roots),
    num_pos_roots ≤ P.signVariations
⊢ Multiset.countP (fun (x : R) ↦ 0 < x) P.roots ≤ P.signVariations

Tactic:
generalize h : P.roots.countP (0 < ·) = num_pos_roots

Premises used: Polynomial.roots, LT.lt, OfNat.ofNat, Multiset.countP
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
num_pos_roots : ℕ
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = num_pos_roots
zero : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = 0), 0 ≤ P.signVariations
succ :
  ∀ (n : ℕ),
    (∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations) →
      ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1), n + 1 ≤ P.signVariations
⊢ num_pos_roots ≤ P.signVariations

Tactic:
induction num_pos_roots generalizing P
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = 0
⊢ 0 ≤ P.signVariations

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = 0
⊢ 0 ≤ P.signVariations

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1
⊢ P ≠ 0

Tactic:
grind [roots_zero, Multiset.countP_zero]

Premises used: Polynomial.roots_zero, Multiset.countP_zero
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1
⊢ P ≠ 0

Tactic:
have hp : P ≠ 0 := by grind [roots_zero, Multiset.countP_zero]
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1
hp : P ≠ 0
⊢ ∃ x ∈ P.roots, 0 < x

Tactic:
grind [Multiset.countP_pos]

Premises used: Multiset.countP_pos
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1
hp : P ≠ 0
succ : ∀ (η : R) (η_root : η ∈ P.roots) (η_pos : 0 < η), n + 1 ≤ P.signVariations
⊢ n + 1 ≤ P.signVariations

Tactic:
obtain ⟨η, η_root, η_pos⟩ : ∃ x, x ∈ P.roots ∧ 0 < x := by grind [Multiset.countP_pos]

Premises used: Polynomial.roots
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
P : R[X]
h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n + 1
hp : P ≠ 0
η : R
η_root : η ∈ P.roots
η_pos : 0 < η
succ :
  ∀ (Q : R[X])
    (h :
      Multiset.countP (fun (x : R) ↦ 0 < x)
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
        n + 1)
    (hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0)
    (η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots),
    n + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).signVariations
⊢ n + 1 ≤ P.signVariations

Tactic:
obtain ⟨Q, rfl⟩ := dvd_iff_isRoot.mpr (isRoot_of_mem_roots η_root)

Premises used: Iff.mpr, Polynomial.isRoot_of_mem_roots, Polynomial.dvd_iff_isRoot, rfl
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h :
  Multiset.countP (fun (x : R) ↦ 0 < x)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
    n + 1
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0
η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots
succ : Q ≠ 0
succ₁ : Multiset.countP (fun (x : R) ↦ 0 < x) Q.roots = n
⊢ n + 1 ≤ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).signVariations

Tactic:
grw [ih Q, succ_signVariations_le_X_sub_C_mul η_pos]

Premises used: Polynomial.succ_signVariations_le_X_sub_C_mul
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h :
  Multiset.countP (fun (x : R) ↦ 0 < x)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
    n + 1
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0
η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots
⊢ Q ≠ 0

Tactic:
right_ne_zero_of_mul hp

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h :
  Multiset.countP (fun (x : R) ↦ 0 < x)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
    n + 1
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0
η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots
⊢ Q ≠ 0

Tactic:
exact right_ne_zero_of_mul hp

Premises used: right_ne_zero_of_mul
-- Module: Mathlib.Algebra.Polynomial.RuleOfSigns
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
ih : ∀ (P : R[X]) (h : Multiset.countP (fun (x : R) ↦ 0 < x) P.roots = n), n ≤ P.signVariations
η : R
η_pos : 0 < η
Q : R[X]
h :
  Multiset.countP (fun (x : R) ↦ 0 < x)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots =
    n + 1
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q ≠ 0
η_root : η ∈ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) η : R[X]) * Q).roots
⊢ Multiset.countP (fun (x : R) ↦ 0 < x) Q.roots = n

Tactic:
simp [← h, roots_mul (ne_zero_of_mem_roots η_root), η_pos, ← Nat.succ.injEq]

Premises used: Nat.succ.injEq, Polynomial.ne_zero_of_mem_roots, Polynomial.roots_mul
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Semiring R
S : Sequence R
i : ℕ
⊢ ((↑S : ℕ → R[X]) i).degree = (↑i : WithBot ℕ)

Tactic:
S.degree_eq' i

Premises used: Polynomial.Sequence.degree_eq'
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Semiring R
S : Sequence R
i : ℕ
⊢ ((↑S : ℕ → R[X]) i).natDegree = i

Tactic:
natDegree_eq_of_degree_eq_some <| S.degree_eq i

Premises used: Polynomial.Sequence.degree_eq, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Semiring R
S : Sequence R
i : ℕ
⊢ ((↑S : ℕ → R[X]) i).degree ≠ ⊥

Tactic:
simp [S.degree_eq i]

Premises used: Polynomial.Sequence.degree_eq
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Semiring R
S : Sequence R
x x_1 : ℕ
⊢ x < x_1 → (degree ∘ (↑S : ℕ → R[X])) x < (degree ∘ (↑S : ℕ → R[X])) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Semiring R
S : Sequence R
x x_1 : ℕ
⊢ x < x_1 → (natDegree ∘ (↑S : ℕ → R[X])) x < (natDegree ∘ (↑S : ℕ → R[X])) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h₁ : (↑S : ℕ → R[X]) '' Set.Iio m ⊆ (↑(degreeLT R m) : Set R[X])
h₂ : degreeLT R m ≤ span R ((↑S : ℕ → R[X]) '' Set.Iio m)
⊢ span R ((↑S : ℕ → R[X]) '' Set.Iio m) = degreeLT R m

Tactic:
apply span_eq_of_le

Premises used: Submodule.span_eq_of_le
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
hP : P ∈ (↑S : ℕ → R[X]) '' Set.Iio m
h₁ :
  ∀ (i : ℕ) (hi : i ∈ Set.Iio m) (hP : (↑S : ℕ → R[X]) i ∈ (↑S : ℕ → R[X]) '' Set.Iio m),
    (↑S : ℕ → R[X]) i ∈ (↑(degreeLT R m) : Set R[X])
⊢ P ∈ (↑(degreeLT R m) : Set R[X])

Tactic:
obtain ⟨i, hi, rfl⟩ := (Set.mem_image _ _ _).mp hP

Premises used: Set.mem_image, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : (↑S : ℕ → R[X]) i ∈ (↑S : ℕ → R[X]) '' Set.Iio m
h₁ : i < m
⊢ (↑S : ℕ → R[X]) i ∈ (↑(degreeLT R m) : Set R[X])

Tactic:
rw [SetLike.mem_coe, Polynomial.mem_degreeLT, S.degree_eq i, Nat.cast_lt]

Premises used: Polynomial.Sequence.degree_eq, SetLike.mem_coe, Nat.cast_lt, Polynomial.mem_degreeLT
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : (↑S : ℕ → R[X]) i ∈ (↑S : ℕ → R[X]) '' Set.Iio m
⊢ i < m

Tactic:
Set.mem_Iio.mp hi

Premises used: Set.mem_Iio, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
i : ℕ
hi : i ∈ Set.Iio m
hP : (↑S : ℕ → R[X]) i ∈ (↑S : ℕ → R[X]) '' Set.Iio m
⊢ i < m

Tactic:
exact Set.mem_Iio.mp hi

Premises used: Set.mem_Iio, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
⊢ Nontrivial R

Tactic:
nontriviality R using Subsingleton.eq_zero P
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
h : Nontrivial R
generalize :
  ∀ (n : ℕ) (hp : P.natDegree = n), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P

Tactic:
generalize hp : P.natDegree = n

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
pos : ∀ (p_ne_zero : P = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
neg : ∀ (p_ne_zero : P ≠ 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P

Tactic:
by_cases! p_ne_zero : P = 0
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P = 0
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P

Tactic:
simp [p_ne_zero]
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ P.degree < (↑m : WithBot ℕ)

Tactic:
rw [Polynomial.mem_degreeLT] at hP

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hP₁ : P.degree < (↑m : WithBot ℕ)
⊢ P.natDegree = n

Tactic:
rw [Polynomial.mem_degreeLT] at hP

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hP₁ : P.degree < (↑m : WithBot ℕ)
hp₁ : P.natDegree = n
⊢ P ≠ 0

Tactic:
rw [Polynomial.mem_degreeLT] at hP

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : P.degree < (↑m : WithBot ℕ)
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ P.degree = (↑P.natDegree : WithBot ℕ)

Tactic:
have := Polynomial.degree_eq_natDegree p_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : P.degree < (↑m : WithBot ℕ)
hp : P.natDegree = n
p_ne_zero : P ≠ 0
this : P.degree = (↑P.natDegree : WithBot ℕ)
⊢ n < m

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
⊢ n < m

Tactic:
have hn : n < m := by
      rw [Polynomial.mem_degreeLT] at hP
      have := Polynomial.degree_eq_natDegree p_ne_zero
      aesop
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
neg :
  ∀ (u : R) (leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1) (rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1),
    Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P

Tactic:
obtain ⟨u, leftinv, rightinv⟩ := isUnit_iff_exists.mp <| hCoeff n hn

Premises used: isUnit_iff_exists, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
⊢ n ∈ Set.Iio m

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) ((↑S : ℕ → R[X]) n)

Tactic:
have in_span : S n ∈ span R (S '' Set.Iio m) := subset_span ⟨n, by simp [hn], rfl⟩
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
in_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) ((↑S : ℕ → R[X]) n)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m))
    ((P.leadingCoeff • u) • (↑S : ℕ → R[X]) n)

Tactic:
have smul_span := smul_mem (span R (S '' Set.Iio m)) (P.leadingCoeff • u) in_span
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
in_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) ((↑S : ℕ → R[X]) n)
smul_span :
  Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m))
    ((P.leadingCoeff • u) • (↑S : ℕ → R[X]) n)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (smul_span :
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m))
        (P.leadingCoeff • u • (↑S : ℕ → R[X]) n)),
    Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head

Tactic:
rwa [smul_assoc] at smul_span

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i < m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
h : Nontrivial R
n : ℕ
ih :
  ∀ m_1 < n,
    ∀ ⦃P : R[X]⦄ (hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P) (hp : P.natDegree = m_1),
      Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
P : R[X]
hP : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) P
hp : P.natDegree = n
p_ne_zero : P ≠ 0
hn : n < m
u : R
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head

Tactic:
have head_mem_span : head ∈ span R (S '' Set.Iio m) := by
      have in_span : S n ∈ span R (S '' Set.Iio m) := subset_span ⟨n, by simp [hn], rfl⟩
      have smul_span := smul_mem (span R (S '' Set.Iio m)) (P.leadingCoeff • u) in_span
      rwa [smul_assoc] at smul_span