awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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
⊢ tail.degree < (↑n : WithBot ℕ)
have neg : ∀ (tail_degree_lt : (P - P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree < (↑P.natDegree : WithBot ℕ)),
  tail.degree < (↑n : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree p_ne_zero, hp] at tail_degree_lt
Cleared hypotheses: tail_degree_lt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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 ℕ)
⊢ tail.degree < (↑n : WithBot ℕ)
have neg₁ : ∀ (tail_degree_lt : (P - P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree < (↑n : WithBot ℕ)),
  tail.degree < (↑n : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree p_ne_zero, hp] at tail_degree_lt
Cleared hypotheses: tail_degree_lt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
m : ℕ
hCoeff : ∀ i ≤ m, IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
⊢ span R ((↑S : ℕ → R[X]) '' Set.Iic m) = degreeLE R (↑m : WithBot ℕ)
have rw : Eq (α := Submodule R R[X]) (degreeLT R (Order.succ 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))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
⊢ Eq (α := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) ⊤
have rw : ∀ (x : R[X]), Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) x
Tactic: rw [eq_top_iff']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
Goal:
R : Type u_1
inst : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit ((↑S : ℕ → R[X]) i).leadingCoeff
P : R[X]
⊢ Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P
have pos : ∀ (p_ne_zero : P = 0), Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P
Tactic: by_cases! p_ne_zero : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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
⊢ Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P
have neg : ∀ (p_ne_zero : P ≠ 0), Membership.mem (γ := Submodule R R[X]) (span R (Set.range (↑S : ℕ → R[X]))) P
Tactic: by_cases! p_ne_zero : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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
have neg : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio (P.natDegree + 1))) P
Tactic: suffices P ∈ span R (S '' Set.Iio (P.natDegree + 1)) from (span_mono (by simp)) this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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 ((↑S : ℕ → R[X]) '' Set.Iio (P.natDegree + 1))) P
have neg : P.natDegree < P.natDegree + 1
Tactic: rw [span_degreeLT _ (by grind), Polynomial.mem_degreeLT, ← natDegree_lt_iff_degree_lt p_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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
⊢ g i = 0
have pos : ∀ (hsupzero : Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥), g i = 0
Tactic: by_cases hsupzero : s.sup (fun i ↦ (g i • S i).degree) = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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
⊢ g i = 0
have neg : ∀ (hsupzero : ¬Eq (α := WithBot ℕ) (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) ⊥), g i = 0
Tactic: by_cases hsupzero : s.sup (fun i ↦ (g i • S i).degree) = ⊥
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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) ⊥
⊢ g i = 0
have 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)
Tactic: have le_sup := Finset.le_sup hi (f := fun i ↦ (g i • S i).degree)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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 : ℕ
⊢ 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
have 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
Tactic: ⟨_, hx⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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 : ℕ
⊢ 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
have 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
Tactic: ⟨_, hy⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
⊢ Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y
have zgx : g x ≠ 0
Tactic: have zgx : g x ≠ 0 := (smul_ne_zero_iff.mp hx).1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
⊢ Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y
have zgy : g y ≠ 0
Tactic: have zgy : g y ≠ 0 := (smul_ne_zero_iff.mp hy).1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
⊢ Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y
have rx : IsRightRegular ((↑S : ℕ → R[X]) x).leadingCoeff
Tactic: have rx : IsRightRegular (S x).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
⊢ Function.onFun (β := WithBot ℕ) Ne (fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) x y
have ry : IsRightRegular ((↑S : ℕ → R[X]) y).leadingCoeff
Tactic: have ry : IsRightRegular (S y).leadingCoeff := IsRegular.of_ne_zero (by simp) |>.right
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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) ⊥
⊢ g i = 0
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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)
⊢ g i = 0
have neg : ∀ (n : WithBot ℕ) (hn : (s.sup fun (i : ℕ) ↦ (g i • (↑S : ℕ → R[X]) i).degree) = n), g i = 0
Tactic: obtain ⟨n, hn⟩ : ∃ n, (s.sup fun i ↦ (g i • S i).degree) = n := exists_eq'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (goal)
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
have neg : degree.{u_1} (R := R) (∑ i ∈ s, g i • (↑S : ℕ → R[X]) i) ≠ ⊥
Tactic: refine degree_ne_bot.mp ?_ eqzero |>.elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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) ≠ ⊥
have 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
Tactic: have hsum := degree_sum_eq_of_disjoint _ s hpairwise
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
⊢ p.smeval x = p.sum (smul_pow x)
have rw : p.sum (smul_pow x) = p.sum (smul_pow x)
Tactic: rw [smeval_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
p : R[X]
⊢ eval r p = p.smeval r
have rw : (p.sum fun (e : ℕ) (a : R) ↦ a * r ^ e) = p.sum (smul_pow r)
Tactic: rw [eval_eq_sum, smeval_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x
have rw : (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e)) = p.sum (smul_pow x)
Tactic: rw [smeval_eq_sum, eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_3
inst : Semiring R
S : Type u_4
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
p : R[X]
x : S
⊢ (p.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e)) =
    p.sum (smul_pow x)
have e_f : ∀ (e : ℕ) (a : R), HMul.hMul (α := S) ((RingHom.smulOneHom : (a : R) → S) a : S) (x ^ e) = smul_pow x e a
Tactic: congr 1 with e a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : MulActionWithZero R S
x : S
⊢ smeval.{u_1, u_2} (R := R) 1 x = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (HPow.hPow (β := ℕ) x 0) = HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0)
Tactic: rw [← C_1, smeval_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
⊢ (p + q).smeval x = p.smeval x + q.smeval x
have simp : (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)
Tactic: simp only [smeval_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)
have refine_1 : ∀ (x_1 : ℕ), smul_pow.{u_1, u_2} (R := R) x x_1 0 = 0
Tactic: refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
refine_1 : ∀ (x_1 : ℕ), smul_pow.{u_1, u_2} (R := R) x x_1 0 = 0
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)
have refine_2 : ∀ (x_1 : ℕ) (x_2 x_3 : R), smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
Tactic: refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
⊢ smul_pow.{u_1, u_2} (R := R) x x_1 0 = 0
have refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ x_1) = 0
Tactic: rw [smul_pow, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
refine_1 : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ x_1) = 0
⊢ smul_pow.{u_1, u_2} (R := R) x x_1 0 = 0
have refine_1₁ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [smul_pow, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
x_2 x_3 : R
⊢ smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
have refine_2 : (x_2 + x_3) • x ^ x_1 = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
Tactic: rw [smul_pow, smul_pow, smul_pow, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
x_2 x_3 : R
refine_2 : (x_2 + x_3) • x ^ x_1 = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
⊢ smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
have refine_2₁ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + smul_pow x x_1 x_3
Tactic: rw [smul_pow, smul_pow, smul_pow, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
x_2 x_3 : R
refine_2 : (x_2 + x_3) • x ^ x_1 = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
refine_2₁ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + smul_pow x x_1 x_3
⊢ smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
have refine_2₂ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + x_3 • x ^ x_1
Tactic: rw [smul_pow, smul_pow, smul_pow, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
p q : R[X]
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
x_1 : ℕ
x_2 x_3 : R
refine_2 : (x_2 + x_3) • x ^ x_1 = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
refine_2₁ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + smul_pow x x_1 x_3
refine_2₂ : (x_2 + x_3) • x ^ x_1 = x_2 • x ^ x_1 + x_3 • x ^ x_1
⊢ smul_pow x x_1 (x_2 + x_3) = smul_pow x x_1 x_2 + smul_pow x x_1 x_3
have refine_2₃ : x_2 • x ^ x_1 + x_3 • x ^ x_1 = x_2 • x ^ x_1 + x_3 • x ^ x_1
Tactic: rw [smul_pow, smul_pow, smul_pow, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
ih : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
⊢ smeval.{u_1, u_2} (R := R) (↑(n + 1) : R[X]) x = (n + 1) • HPow.hPow (β := ℕ) x 0
have succ : (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1).smeval x = (n + 1) • HPow.hPow (β := ℕ) x 0
Tactic: rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
ih : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
succ : (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1).smeval x = (n + 1) • HPow.hPow (β := ℕ) x 0
⊢ smeval.{u_1, u_2} (R := R) (↑(n + 1) : R[X]) x = (n + 1) • HPow.hPow (β := ℕ) x 0
have succ₁ : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
Tactic: rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
ih : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
succ : (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1).smeval x = (n + 1) • HPow.hPow (β := ℕ) x 0
succ₁ : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
⊢ smeval.{u_1, u_2} (R := R) (↑(n + 1) : R[X]) x = (n + 1) • HPow.hPow (β := ℕ) x 0
have succ₂ : n • HPow.hPow (β := ℕ) x 0 + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
Tactic: rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Smeval (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : AddCommMonoid S
inst_2 : Pow S ℕ
inst_3 : Module R S
x : S
n : ℕ
ih : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x = n • HPow.hPow (β := ℕ) x 0
succ : (HAdd.hAdd (α := R[X]) (↑n : R[X]) 1).smeval x = (n + 1) • HPow.hPow (β := ℕ) x 0
succ₁ : smeval.{u_1, u_2} (R := R) (↑n : R[X]) x + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
succ₂ : n • HPow.hPow (β := ℕ) x 0 + smeval.{u_1, u_2} (R := R) 1 x = (n + 1) • HPow.hPow (β := ℕ) x 0
⊢ smeval.{u_1, u_2} (R := R) (↑(n + 1) : R[X]) x = (n + 1) • HPow.hPow (β := ℕ) x 0
have succ₃ : n • HPow.hPow (β := ℕ) x 0 + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) x 0) = (n + 1) • HPow.hPow (β := ℕ) x 0
Tactic: rw [n.cast_succ, smeval_add, ih, smeval_one, ← add_nsmul]