-- 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.degree = (P.leadingCoeff • u • ↑S n).degree
⊢ head ≠ 0

Tactic:
by_cases n_eq_zero : n = 0

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 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
⊢ head ≠ 0

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
⊢ head ≠ 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
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
⊢ 0 < P.natDegree

Tactic:
omega

Result:
no goals

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
⊢ P ∈ span R (Set.range ↑S)

Tactic:
let head := P.leadingCoeff • u • S n

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
⊢ P ∈ span R (Set.range ↑S)

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
⊢ head ≠ 0

Tactic:
dsimp [head]

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 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

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

Tactic:
rw [degree_eq_natDegree, head_degree_eq_natDegree] at head_degree_eq

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
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.leadingCoeff

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