-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- Polynomials in a polynomial sequence are linearly independent. -/
lemma linearIndependent :
    LinearIndependent R S := linearIndependent_iff'.mpr <| fun s g eqzero i hi ↦ by
  by_cases hsupzero : s.sup (fun i ↦ (g i • S i).degree) = ⊥
  · have le_sup := Finset.le_sup hi (f := fun i ↦ (g i • S i).degree)
    exact (smul_eq_zero_iff_left (S.ne_zero i)).mp <| degree_eq_bot.mp (eq_bot_mono le_sup hsupzero)
  have hpairwise : {i | i ∈ s ∧ g i • S i ≠ 0}.Pairwise (Ne on fun i ↦ (g i • S i).degree)

Proof state:
case pos
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : (s.sup fun i => (g i • ↑S i).degree) = ⊥
le_sup : (fun i => (g i • ↑S i).degree) i ≤ s.sup fun i => (g i • ↑S i).degree
⊢ g i = 0

Tactic:
exact (smul_eq_zero_iff_left (S.ne_zero i)).mp <| degree_eq_bot.mp (eq_bot_mono le_sup hsupzero)

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
⊢ g i = 0

Tactic:
have hpairwise : {i | i ∈ s ∧ g i • S i ≠ 0}.Pairwise (Ne on fun i ↦ (g i • S i).degree) := by
  intro x ⟨_, hx⟩ y ⟨_, hy⟩ xney
  have zgx : g x ≠ 0 := (smul_ne_zero_iff.mp hx).1
  have zgy : g y ≠ 0 := (smul_ne_zero_iff.mp hy).1
  have rx : IsRightRegular (S x).leadingCoeff := isRegular_of_ne_zero (by simp) |>.right
  have ry : IsRightRegular (S y).leadingCoeff := isRegular_of_ne_zero (by simp) |>.right
  simp [degree_smul_of_isRightRegular_leadingCoeff, rx, ry, zgx, zgy, xney]

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
hpairwise : {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)
⊢ g i = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular (↑S x).leadingCoeff
⊢ (↑S y).leadingCoeff ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Tactic:
have zgx : g x ≠ 0 := (smul_ne_zero_iff.mp hx).1

Result:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Proof state:
case neg.intro
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
hpairwise : {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)
n : WithBot ℕ
hn : (s.sup fun i => (g i • ↑S i).degree) = n
⊢ g i = 0

Tactic:
refine degree_ne_bot.mp ?_ eqzero |>.elim

Result:
case neg.intro
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
hpairwise : {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)
n : WithBot ℕ
hn : (s.sup fun i => (g i • ↑S i).degree) = n
⊢ (∑ i ∈ s, g i • ↑S i).degree ≠ ⊥

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
⊢ g i = 0

Tactic:
by_cases hsupzero : s.sup (fun i ↦ (g i • S i).degree) = ⊥

Result:
case pos
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : (s.sup fun i => (g i • ↑S i).degree) = ⊥
⊢ g i = 0

case neg
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
⊢ g i = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Tactic:
have rx : IsRightRegular (S x).leadingCoeff := isRegular_of_ne_zero (by simp) |>.right

Result:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular (↑S x).leadingCoeff
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Tactic:
have zgy : g y ≠ 0 := (smul_ne_zero_iff.mp hy).1

Result:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
zgx : g x ≠ 0
zgy : g y ≠ 0
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
⊢ {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)

Tactic:
intro x ⟨_, hx⟩ y ⟨_, hy⟩ xney

Result:
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
x : ℕ
left✝¹ : x ∈ s
hx : g x • ↑S x ≠ 0
y : ℕ
left✝ : y ∈ s
hy : g y • ↑S y ≠ 0
xney : x ≠ y
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Proof state:
case neg.intro
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
hpairwise : {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)
n : WithBot ℕ
hn : (s.sup fun i => (g i • ↑S i).degree) = n
⊢ (∑ i ∈ s, g i • ↑S i).degree ≠ ⊥

Tactic:
have hsum := degree_sum_eq_of_disjoint _ s hpairwise

Result:
case neg.intro
R : Type u_1
inst✝¹ : Ring R
S : Sequence R
inst✝ : NoZeroDivisors R
s : Finset ℕ
g : ℕ → R
eqzero : ∑ i ∈ s, g i • ↑S i = 0
i : ℕ
hi : i ∈ s
hsupzero : ¬(s.sup fun i => (g i • ↑S i).degree) = ⊥
hpairwise : {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)
n : WithBot ℕ
hn : (s.sup fun i => (g i • ↑S i).degree) = n
hsum : (∑ i ∈ s, g i • ↑S i).degree = s.sup fun i => (g i • ↑S i).degree
⊢ (∑ i ∈ s, g i • ↑S i).degree ≠ ⊥