-- 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:
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.natDegree = ↑head.natDegree
head_degree_eq_natDegree : head.degree = ↑head.natDegree
⊢ P.leadingCoeff = head.coeff head.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

Tactic:
rw_mod_cast [← head_degree_eq, hp]

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 = head.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

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
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
in_span : ↑S n ∈ span R (Set.range ↑S)
smul_span : (P.leadingCoeff • u) • ↑S n ∈ span R (Set.range ↑S)
⊢ head ∈ span R (Set.range ↑S)

Tactic:
rwa [smul_assoc] at smul_span

Result:
no goals

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
head_degree_eq_natDegree : head.degree = ↑head.natDegree
hPhead : P.leadingCoeff = head.leadingCoeff
tail_degree_lt : (P - P.leadingCoeff • u • ↑S n).degree < P.degree
⊢ tail.degree < ↑n

Tactic:
rwa [degree_eq_natDegree p_ne_zero, hp] at tail_degree_lt

Result:
no goals

Proof state:
case pos
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
⊢ ¬P.leadingCoeff • u • ↑S n = 0

Tactic:
rw [n_eq_zero, ← coeff_natDegree, natDegree_eq] at rightinv

Result:
case pos
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 0).coeff 0 = 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
⊢ ¬P.leadingCoeff • u • ↑S n = 0

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
head_degree_eq_natDegree : head.degree = ↑head.natDegree
hPhead : P.leadingCoeff = head.leadingCoeff
⊢ tail.degree < ↑n

Tactic:
have tail_degree_lt := P.degree_sub_lt head_degree_eq p_ne_zero hPhead

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
head_degree_eq_natDegree : head.degree = ↑head.natDegree
hPhead : P.leadingCoeff = head.leadingCoeff
tail_degree_lt : (P - P.leadingCoeff • u • ↑S n).degree < P.degree
⊢ tail.degree < ↑n