awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hn : n < m
u : R
head : R[X] := P.leadingCoeff • u • (↑S : ℕ → R[X]) n
tail : R[X] := P - head
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
isRightRegular_smul_leadingCoeff : IsRightRegular (u • (↑S : ℕ → R[X]) n).leadingCoeff
u_degree_same : (u • (↑S : ℕ → R[X]) n).degree = ((↑S : ℕ → R[X]) n).degree
head_degree_eq_natDegree : head.degree = (↑head.natDegree : WithBot ℕ)
p_ne_zero : ¬P = 0
leftinv : ((↑S : ℕ → R[X]) n).leadingCoeff * u = 1
rightinv : u * ((↑S : ℕ → R[X]) n).leadingCoeff = 1
tail_eq_zero : ¬tail = 0
head_degree_eq : P.natDegree = head.natDegree
rw : P.leadingCoeff = P.leadingCoeff • (u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
rw₁ : P.leadingCoeff = P.leadingCoeff • u • ((↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
rw₂ : P.leadingCoeff = P.leadingCoeff • u • ((↑S : ℕ → R[X]) n).leadingCoeff
rw₃ : P.leadingCoeff = P.leadingCoeff * u • ((↑S : ℕ → R[X]) n).leadingCoeff
rw₄ : P.leadingCoeff = P.leadingCoeff * (u * ((↑S : ℕ → R[X]) n).leadingCoeff)
rw₅ : P.leadingCoeff = P.leadingCoeff * 1
rw₆ rw₇ : P.leadingCoeff = P.leadingCoeff
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree

Tactic:
rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_smul, smul_eq_mul, mul_one
-- 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • (↑S : ℕ → R[X]) n).leadingCoeff
u_degree_same : (u • (↑S : ℕ → R[X]) n).degree = ((↑S : ℕ → R[X]) n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree
head_degree_eq_natDegree : head.degree = (↑head.natDegree : WithBot ℕ)
⊢ P.leadingCoeff = head.leadingCoeff

Tactic:
have hPhead : P.leadingCoeff = head.leadingCoeff := by
      rw [degree_eq_natDegree p_ne_zero, head_degree_eq_natDegree] at head_degree_eq
      nth_rw 2 [← coeff_natDegree]
      rw_mod_cast [← head_degree_eq, hp]
      dsimp [head]
      nth_rw 2 [← S.natDegree_eq n]
      rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • (↑S : ℕ → R[X]) n).leadingCoeff
u_degree_same : (u • (↑S : ℕ → R[X]) n).degree = ((↑S : ℕ → R[X]) n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree
head_degree_eq_natDegree : head.degree = (↑head.natDegree : WithBot ℕ)
hPhead : P.leadingCoeff = head.leadingCoeff
⊢ (P - P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree < P.degree

Tactic:
have tail_degree_lt := P.degree_sub_lt head_degree_eq p_ne_zero hPhead
-- 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • (↑S : ℕ → R[X]) n).leadingCoeff
u_degree_same : (u • (↑S : ℕ → R[X]) n).degree = ((↑S : ℕ → R[X]) n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree
head_degree_eq_natDegree : head.degree = (↑head.natDegree : WithBot ℕ)
hPhead : P.leadingCoeff = head.leadingCoeff
tail_degree_lt : (P - P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree < P.degree
neg :
  ∀ (tail_degree_lt : (P - P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree < (↑P.natDegree : WithBot ℕ)),
    tail.degree < (↑n : WithBot ℕ)
neg₁ neg₂ neg₃ neg₄ :
  ∀ (tail_degree_lt : (P - P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree < (↑n : WithBot ℕ)),
    tail.degree < (↑n : WithBot ℕ)
⊢ tail.degree < (↑n : WithBot ℕ)

Tactic:
rwa [degree_eq_natDegree p_ne_zero, hp] at tail_degree_lt

Premises used: Polynomial.degree_eq_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
rw : Eq (α := Submodule R R[X]) (degreeLT R (Order.succ m)) (degreeLE R (↑m : WithBot ℕ))
⊢ span R ((↑S : ℕ → R[X]) '' Set.Iic m) = degreeLE R (↑m : WithBot ℕ)

Tactic:
rw [← Set.Iio_succ_eq_Iic, span_degreeLT _ (fun i hi => hCoeff i (Order.lt_succ_iff.mp hi))]

Premises used: Set.Iio_succ_eq_Iic, Order.lt_succ_iff, Iff.mp, Polynomial.Sequence.span_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
⊢ Eq (α := Submodule R R[X]) (degreeLT R (Order.succ m)) (degreeLE R (↑m : WithBot ℕ))

Tactic:
simp [← Polynomial.degreeLT_succ_eq_degreeLE]

Premises used: Polynomial.degreeLT_succ_eq_degreeLE
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
rw : ∀ (x : R[X]), Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) x
⊢ Eq (α := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) ⊤

Tactic:
rw [eq_top_iff']

Premises used: Submodule.eq_top_iff'
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
pos : ∀ (p_ne_zero : P = 0), Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P
neg : ∀ (p_ne_zero : P ≠ 0), Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) 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
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
p_ne_zero : P = 0
⊢ Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P

Tactic:
simp [p_ne_zero]
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
this : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio (P.natDegree + 1))) P
⊢ (↑S : ℕ → R[X]) '' Set.Iio (P.natDegree + 1) ⊆ Set.range (↑S : ℕ → R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
neg : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio (P.natDegree + 1))) P
⊢ Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P

Tactic:
suffices P ∈ span R (S '' Set.Iio (P.natDegree + 1)) from (span_mono (by simp)) this
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
⊢ ∀ i < P.natDegree + 1, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
neg : P.natDegree < P.natDegree + 1
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio (P.natDegree + 1))) P

Tactic:
rw [span_degreeLT _ (by grind), Polynomial.mem_degreeLT, ← natDegree_lt_iff_degree_lt p_ne_zero]

Premises used: Polynomial.natDegree_lt_iff_degree_lt, Polynomial.Sequence.span_degreeLT, Polynomial.mem_degreeLT
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
p_ne_zero : P ≠ 0
⊢ P.natDegree < P.natDegree + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
pos : ∀ (hsupzero : Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥), g i = 0
neg : ∀ (hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥), g i = 0
⊢ g i = 0

Tactic:
by_cases hsupzero : s.sup (fun i ↦ (g i • S i).degree) = ⊥

Premises used: Polynomial.Sequence.elems', Polynomial.degree, Finset.sup, HSMul.hSMul
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
⊢ LE.le (α := WithBot ℕ) ((fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) i)
    (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)

Tactic:
have le_sup := Finset.le_sup hi (f := fun i ↦ (g i • S i).degree)
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
le_sup :
  LE.le (α := WithBot ℕ) ((fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) i)
    (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
⊢ g i = 0

Tactic:
(smul_eq_zero_iff_left (S.ne_zero i)).mp <| degree_eq_bot.mp (eq_bot_mono le_sup hsupzero)

Premises used: smul_eq_zero_iff_left, Iff.mp, eq_bot_mono, Polynomial.Sequence.ne_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
le_sup :
  LE.le (α := WithBot ℕ) ((fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) i)
    (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
⊢ g i = 0

Tactic:
exact (smul_eq_zero_iff_left (S.ne_zero i)).mp <| degree_eq_bot.mp (eq_bot_mono le_sup hsupzero)

Premises used: smul_eq_zero_iff_left, Iff.mp, eq_bot_mono, Polynomial.Sequence.ne_zero, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
this :
  x ∈ s →
    ∀ (hx : g x • (↑S : ℕ → R[X]) x ≠ 0) ⦃y : ℕ⦄,
      Membership.mem (γ := Set ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0} y →
        x ≠ y → Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0} x →
    ∀ ⦃y : ℕ⦄,
      Membership.mem (γ := Set ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0} y →
        x ≠ y → Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y

Tactic:
⟨_, hx⟩
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
this :
  y ∈ s →
    ∀ (hy : g y • (↑S : ℕ → R[X]) y ≠ 0),
      x ≠ y → Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y
⊢ Membership.mem (γ := Set ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0} y →
    x ≠ y → Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y

Tactic:
⟨_, hy⟩
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
⊢ g x ≠ 0

Tactic:
have zgx : g x ≠ 0 := (smul_ne_zero_iff.mp hx).1
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
⊢ g y ≠ 0

Tactic:
have zgy : g y ≠ 0 := (smul_ne_zero_iff.mp hy).1
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
⊢ ((↑S : ℕ → R[X]) x).leadingCoeff ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
⊢ IsRightRegular ((↑S : ℕ → R[X]) x).leadingCoeff

Tactic:
have rx : IsRightRegular (S x).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular ((↑S : ℕ → R[X]) x).leadingCoeff
⊢ ((↑S : ℕ → R[X]) y).leadingCoeff ≠ 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular ((↑S : ℕ → R[X]) x).leadingCoeff
⊢ IsRightRegular ((↑S : ℕ → R[X]) y).leadingCoeff

Tactic:
have ry : IsRightRegular (S y).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
x : ℕ
left : x ∈ s
hx : g x • (↑S : ℕ → R[X]) x ≠ 0
y : ℕ
left_1 : y ∈ s
hy : g y • (↑S : ℕ → R[X]) y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular ((↑S : ℕ → R[X]) x).leadingCoeff
ry : IsRightRegular ((↑S : ℕ → R[X]) y).leadingCoeff
⊢ Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y

Tactic:
simp [degree_smul_of_isRightRegular_leadingCoeff, rx, ry, zgx, zgy, xney]

Premises used: Polynomial.degree_smul_of_isRightRegular_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
⊢ Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)

Tactic:
have hpairwise : {i | i ∈ s ∧ g i • S i ≠ 0}.Pairwise (Ne on fun i ↦ (g i • S i).degree) := by
    intro x ⟨_, hx⟩ y ⟨_, hy⟩ xney
    have zgx : g x ≠ 0 := (smul_ne_zero_iff.mp hx).1
    have zgy : g y ≠ 0 := (smul_ne_zero_iff.mp hy).1
    have rx : IsRightRegular (S x).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right
    have ry : IsRightRegular (S y).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right
    simp [degree_smul_of_isRightRegular_leadingCoeff, rx, ry, zgx, zgy, xney]
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
⊢ ∃ (n : WithBot ℕ), (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n

Tactic:
exists_eq'

Premises used: exists_eq'
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
neg : ∀ (n : WithBot ℕ) (hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n), g i = 0
⊢ g i = 0

Tactic:
obtain ⟨n, hn⟩ : ∃ n, (s.sup fun i ↦ (g i • S i).degree) = n := exists_eq'

Premises used: Polynomial.Sequence.elems', Polynomial.degree, exists_eq', Finset.sup, HSMul.hSMul
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
n : WithBot ℕ
hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n
⊢ g i = 0

Tactic:
degree_ne_bot.mp ?_ eqzero |>.elim

Premises used: False.elim, Iff.mp, Polynomial.degree_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
n : WithBot ℕ
hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n
neg : degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) ≠ ⊥
⊢ g i = 0

Tactic:
refine degree_ne_bot.mp ?_ eqzero |>.elim

Premises used: False.elim, Iff.mp, Polynomial.degree_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
n : WithBot ℕ
hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n
⊢ degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) = s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree

Tactic:
have hsum := degree_sum_eq_of_disjoint _ s hpairwise
-- Module: Mathlib.Algebra.Polynomial.Sequence
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
inst_1 : IsDomain R
s : Finset ℕ
g : ℕ → R
eqzero : Eq.{u_1 + 1} (α := R[X]) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) 0
i : ℕ
hi : i ∈ s
hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥
hpairwise :
  Set.Pairwise (α := ℕ) {i : ℕ | i ∈ s ∧ g i • (↑S : ℕ → R[X]) i ≠ 0}
    (Function.onFun (β := WithBot ℕ) Ne fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree)
n : WithBot ℕ
hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n
hsum : degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) = s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree
⊢ degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) ≠ ⊥

Tactic:
hsum.trans hn |>.trans_ne <| (ne_of_ne_of_eq (hsupzero ·.symm) hn).symm

Premises used: Ne.symm, Eq.trans_ne, Eq.symm, ne_of_ne_of_eq, Eq.trans