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

Tactic:
have ry : IsRightRegular (S y).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
ry : IsRightRegular (↑S y).leadingCoeff
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

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) = ⊥
hpairwise : {i | i ∈ s ∧ g i • ↑S i ≠ 0}.Pairwise (Ne on fun i => (g i • ↑S i).degree)
⊢ g i = 0

Tactic:
obtain ⟨n, hn⟩ : ∃ n, (s.sup fun i ↦ (g i • S i).degree) = n := exists_eq'

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
⊢ g i = 0

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) = ⊥
⊢ g i = 0

Tactic:
have le_sup := Finset.le_sup hi (f := 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) = ⊥
le_sup : (fun i => (g i • ↑S i).degree) i ≤ 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
⊢ (↑S x).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
zgx : g x ≠ 0
zgy : g y ≠ 0
rx : IsRightRegular (↑S x).leadingCoeff
ry : IsRightRegular (↑S y).leadingCoeff
⊢ (Ne on fun i => (g i • ↑S i).degree) x y

Tactic:
simp [degree_smul_of_isRightRegular_leadingCoeff, rx, ry, zgx, zgy, xney]

Result:
no goals