awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
⊢ tail.degree < (↑n : WithBot ℕ)
have head_degree_eq : (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree = (u • (↑S : ℕ → R[X]) n).degree
Tactic: have head_degree_eq := degree_smul_of_isRightRegular_leadingCoeff
      (leadingCoeff_ne_zero.mpr p_ne_zero) isRightRegular_smul_leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree = (u • (↑S : ℕ → R[X]) n).degree
⊢ tail.degree < (↑n : WithBot ℕ)
have head_degree_eq₁ : P.degree = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree
Tactic: rw [u_degree_same, S.degree_eq n, ← hp, eq_comm,
      ← degree_eq_natDegree p_ne_zero, hp] at head_degree_eq
Cleared hypotheses: head_degree_eq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
⊢ tail.degree < (↑n : WithBot ℕ)
have head_degree_eq_natDegree : head.degree = (↑head.natDegree : WithBot ℕ)
Tactic: have head_degree_eq_natDegree : head.degree = head.natDegree := degree_eq_natDegree <| by
      grind [degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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
have head_degree_eq₁ : Eq (α := WithBot ℕ) (↑P.natDegree : WithBot ℕ) (↑head.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree p_ne_zero, head_degree_eq_natDegree] at head_degree_eq
Cleared hypotheses: head_degree_eq, head_degree_eq_natDegree
-- 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 : Eq (α := WithBot ℕ) (↑P.natDegree : WithBot ℕ) (↑head.natDegree : WithBot ℕ)
head_degree_eq_natDegree : head.degree = (↑head.natDegree : WithBot ℕ)
⊢ P.leadingCoeff = head.coeff head.natDegree
have rw_mod_cast : ∀ (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), P.leadingCoeff = head.coeff n
Tactic: rw_mod_cast [← head_degree_eq, hp]
Cleared hypotheses: p_ne_zero, leftinv, rightinv, tail_eq_zero, head_degree_eq
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff n
have nth_rw : P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
Tactic: nth_rw 2 [← S.natDegree_eq n]
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw : 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]
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw₁ : 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]
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw₂ : P.leadingCoeff = P.leadingCoeff • u • ((↑S : ℕ → R[X]) n).leadingCoeff
Tactic: rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw₃ : P.leadingCoeff = P.leadingCoeff * u • ((↑S : ℕ → R[X]) n).leadingCoeff
Tactic: rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw₄ : P.leadingCoeff = P.leadingCoeff * (u * ((↑S : ℕ → R[X]) n).leadingCoeff)
Tactic: rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- 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
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)
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw₅ : P.leadingCoeff = P.leadingCoeff * 1
Tactic: rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- 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
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
⊢ P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff ((↑S : ℕ → R[X]) n).natDegree
have rw₆ : P.leadingCoeff = P.leadingCoeff
Tactic: rw [coeff_smul, coeff_smul, coeff_natDegree, smul_eq_mul, smul_eq_mul, rightinv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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 ℕ)
⊢ tail.degree < (↑n : WithBot ℕ)
have hPhead : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Sequence (hypothesis)
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 < (↑n : WithBot ℕ)
have tail_degree_lt : (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