-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- A polynomial sequence spans `R[X]` if all of its elements' leading coefficients are units. -/
protected lemma span (hCoeff : ∀ i, IsUnit (S i).leadingCoeff) : span R (Set.range S) = ⊤

Proof state:
case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
n_eq_zero : ¬n = 0
⊢ ?m.19938 < head.degree

R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
n_eq_zero : ¬n = 0
⊢ WithBot ℕ

Tactic:
rw [← head_degree_eq]

Result:
case neg
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
n_eq_zero : ¬n = 0
⊢ ?m.19938 < P.degree

R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
n_eq_zero : ¬n = 0
⊢ WithBot ℕ

Proof state:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
⊢ P ∈ span R (Set.range ↑S)

Tactic:
nontriviality R using Subsingleton.eq_zero P

Result:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
P : R[X]
a✝ : Nontrivial R
⊢ P ∈ span R (Set.range ↑S)

Proof state:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
u : R
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
p_ne_zero : ¬P = 0
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
tail_eq_zero : ¬tail = 0
head_degree_eq : P.natDegree = head.natDegree
⊢ P.leadingCoeff = (P.leadingCoeff • u • ↑S n).coeff n

R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
⊢ P ≠ 0

Tactic:
nth_rw 2 [← S.natDegree_eq n]

Result:
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
u : R
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
p_ne_zero : ¬P = 0
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
tail_eq_zero : ¬tail = 0
head_degree_eq : P.natDegree = head.natDegree
⊢ P.leadingCoeff = (P.leadingCoeff • u • ↑S n).coeff (↑S n).natDegree

R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
tail_eq_zero : ¬tail = 0
isRightRegular_smul_leadingCoeff : IsRightRegular (u • ↑S n).leadingCoeff
u_degree_same : (u • ↑S n).degree = (↑S n).degree
head_degree_eq : P.degree = (P.leadingCoeff • u • ↑S n).degree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
⊢ P ≠ 0

Proof state:
case neg.intro.intro
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
⊢ P ∈ span R (Set.range ↑S)

Tactic:
have head_mem_span : head ∈ span R (Set.range S) := by
  have in_span : S n ∈ span R (Set.range S) := subset_span (by simp)
  have smul_span := smul_mem (span R (Set.range S)) (P.leadingCoeff • u) in_span
  rwa [smul_assoc] at smul_span

Result:
case neg.intro.intro
R : Type u_1
inst✝ : Ring R
S : Sequence R
hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff
a✝ : Nontrivial R
n : ℕ
ih : ∀ m < n, ∀ (P : R[X]), P.natDegree = m → P ∈ span R (Set.range ↑S)
P : R[X]
hp : P.natDegree = n
p_ne_zero : ¬P = 0
u : R
leftinv : (↑S n).leadingCoeff * u = 1
rightinv : u * (↑S n).leadingCoeff = 1
head : R[X] := P.leadingCoeff • u • ↑S n
tail : R[X] := P - head
head_mem_span : head ∈ span R (Set.range ↑S)
⊢ P ∈ span R (Set.range ↑S)