-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S)
    (h : Set.Pairwise { i | i ∈ s ∧ f i ≠ 0 } (Ne on natDegree ∘ f)) :
    natDegree (s.sum f) = s.sup fun i => natDegree (f i)

Proof state:
case pos.intro.intro.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

Tactic:
by_cases hb' : f b = 0

Result:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

Proof state:
case pos.intro.intro.h
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)

Tactic:
exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')

Result:
no goals

Proof state:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).natDegree = s.sup fun i => (f i).natDegree

Tactic:
refine natDegree_eq_of_degree_eq_some ?_

Result:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).degree = ↑(s.sup fun i => (f i).natDegree)

Proof state:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ↑(f b).natDegree ≤ (f x).degree

Tactic:
contrapose! hx'

Result:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
hx' : (f x).degree < ↑(f b).natDegree
⊢ f x = 0

Proof state:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).degree = ↑(s.sup fun i => (f i).natDegree)

Tactic:
rw [degree_sum_eq_of_disjoint]

Result:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup fun i => (f i).degree) = ↑(s.sup fun i => (f i).natDegree)

case pos.intro.intro.h
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)

Proof state:
case pos.intro.intro.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ (WithBot.some ∘ fun i => (f i).natDegree) b ≤ s.sup' hs fun i => (f i).degree

Tactic:
simp only [Finset.le_sup'_iff, exists_prop, Function.comp_apply]

Result:
case pos.intro.intro.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

Proof state:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i => (f i).natDegree

Tactic:
rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]

Result:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ ∀ s_1 ∈ s, (f s_1).natDegree = ⊥

Proof state:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i => (f i).degree) = s.sup' hs (WithBot.some ∘ fun i => (f i).natDegree)

Tactic:
refine le_antisymm ?_ ?_

Result:
case pos.intro.intro.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i => (f i).degree) ≤ s.sup' hs (WithBot.some ∘ fun i => (f i).natDegree)

case pos.intro.intro.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ s.sup' hs (WithBot.some ∘ fun i => (f i).natDegree) ≤ s.sup' hs fun i => (f i).degree

Proof state:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup fun i => (f i).degree) = ↑(s.sup fun i => (f i).natDegree)

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
  Nat.cast_withBot, Finset.coe_sup' hs, ←
  Finset.sup'_eq_sup hs]

Result:
case pos.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sup' hs fun i => (f i).degree) = s.sup' hs (WithBot.some ∘ fun i => (f i).natDegree)

Proof state:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
hx' : (f x).degree < ↑(f b).natDegree
⊢ f x = 0

Tactic:
simpa [← Nat.cast_withBot, hb', degree_eq_bot] using hx'

Result:
no goals

Proof state:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ¬∃ x ∈ s, f x ≠ 0
⊢ (s.sum f).natDegree = s.sup fun i => (f i).natDegree

Tactic:
push_neg at H

Result:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i => (f i).natDegree

Proof state:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ∃ b_1 ∈ s, ↑(f b).natDegree ≤ (f b_1).degree

Tactic:
exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩

Result:
no goals