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
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
pos : ∀ (tail_eq_zero : tail = 0), Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P
neg : ∀ (tail_eq_zero : ¬tail = 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 tail_eq_zero : tail = 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
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
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P

Tactic:
simp [head_mem_span, sub_eq_iff_eq_add.mp tail_eq_zero]

Premises used: sub_eq_iff_eq_add, 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
neg : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) P

Tactic:
apply sub_mem_iff_left _ head_mem_span |>.mp

Premises used: Submodule.sub_mem_iff_left, 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
this : tail.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)

Tactic:
ih tail.natDegree ((natDegree_lt_iff_degree_lt tail_eq_zero).mpr this) ?_ rfl

Premises used: Iff.mpr, Set.Mem, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.natDegree, 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
this : tail.degree < (↑n : WithBot ℕ)
refine : Membership.mem (γ := Submodule R R[X]) (degreeLT R m) (P - head)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)

Tactic:
refine ih tail.natDegree ((natDegree_lt_iff_degree_lt tail_eq_zero).mpr this) ?_ rfl

Premises used: Iff.mpr, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.natDegree, 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
head_mem_span : Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) head
tail_eq_zero : ¬tail = 0
this : tail.degree < (↑n : WithBot ℕ)
⊢ tail.degree < (↑m : WithBot ℕ)

Tactic:
grw [(Nat.cast_lt (α := WithBot ℕ)).mpr hn] at this

Premises used: Iff.mpr, Nat.cast_lt
-- 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
this : tail.degree < (↑m : WithBot ℕ)
rwa rwa₁ rwa₂ rwa₃ : (P - head).degree < (↑m : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R m) (P - head)

Tactic:
rwa [Polynomial.mem_degreeLT]

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
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
neg : tail.degree < (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule R R[X]) (span R ((↑S : ℕ → R[X]) '' Set.Iio m)) (P - head)

Tactic:
suffices tail.degree < n by
      refine ih tail.natDegree ((natDegree_lt_iff_degree_lt tail_eq_zero).mpr this) ?_ rfl
      grw [(Nat.cast_lt (α := WithBot ℕ)).mpr hn] at this
      rwa [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
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 (u • (↑S : ℕ → R[X]) n).leadingCoeff

Tactic:
simpa [leadingCoeff_smul_of_smul_regular, IsSMulRegular.of_mul_eq_one leftinv, rightinv]
        using isRegular_one.right

Premises used: IsSMulRegular.of_mul_eq_one, IsRegular.right, Polynomial.leadingCoeff_smul_of_smul_regular, isRegular_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 (u • (↑S : ℕ → R[X]) n).leadingCoeff

Tactic:
have isRightRegular_smul_leadingCoeff : IsRightRegular (u • S n).leadingCoeff := by
      simpa [leadingCoeff_smul_of_smul_regular, IsSMulRegular.of_mul_eq_one leftinv, rightinv]
        using isRegular_one.right
-- 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 • (↑S : ℕ → R[X]) n).degree = ((↑S : ℕ → R[X]) n).degree

Tactic:
have u_degree_same := degree_smul_of_isRightRegular_leadingCoeff
      (left_ne_zero_of_mul_eq_one rightinv) (hCoeff n hn).isRegular.right
-- 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
⊢ (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
-- 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.leadingCoeff • u • (↑S : ℕ → R[X]) n).degree = (u • (↑S : ℕ → R[X]) n).degree
⊢ 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

Premises used: Polynomial.degree_eq_natDegree, Polynomial.Sequence.degree_eq, eq_comm
-- 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 ≠ 0

Tactic:
grind [degree_eq_bot]

Premises used: Polynomial.degree_eq_bot
-- 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 = (↑head.natDegree : WithBot ℕ)

Tactic:
have head_degree_eq_natDegree : head.degree = head.natDegree := degree_eq_natDegree <| by
      grind [degree_eq_bot]
-- 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 ℕ)
⊢ Eq (α := WithBot ℕ) (↑P.natDegree : WithBot ℕ) (↑head.natDegree : WithBot ℕ)

Tactic:
rw [degree_eq_natDegree p_ne_zero, head_degree_eq_natDegree] at head_degree_eq

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
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 ℕ)
head_degree_eq₁ : Eq (α := WithBot ℕ) (↑P.natDegree : WithBot ℕ) (↑head.natDegree : WithBot ℕ)
⊢ head.degree = (↑head.natDegree : WithBot ℕ)

Tactic:
rw [degree_eq_natDegree p_ne_zero, head_degree_eq_natDegree] at head_degree_eq

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
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 ℕ)
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
⊢ P.leadingCoeff = head.coeff head.natDegree

Tactic:
rw_mod_cast [← head_degree_eq, hp]
-- 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
dsimp : P.leadingCoeff = (P.leadingCoeff • u • (↑S : ℕ → R[X]) n).coeff n
⊢ P.leadingCoeff = head.coeff n

Tactic:
dsimp [head]
-- 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
nth_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 n

Tactic:
nth_rw 2 [← S.natDegree_eq n]

Premises used: Polynomial.Sequence.natDegree_eq