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

Proof state:
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ f y ≠ 0

Tactic:
contrapose! H

Result:
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
H : f y = 0
⊢ (f x).degree ≠ (f y).degree

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

Tactic:
simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]

Result:
case insert
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f) → (s.sum f).degree = s.sup fun i => (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Proof state:
case insert.inr.inl.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
hx : x ∉ ∅
h : {i | i ∈ insert x ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (∅.sum f).degree = ∅.sup fun i => (f i).degree
H : (f x).degree = (∅.sum f).degree
⊢ (f x + ∑ x ∈ ∅, f x).degree = (f x).degree ⊔ ∅.sup fun i => (f i).degree

Tactic:
simp

Result:
no goals

Proof state:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
have hy0 : f y ≠ 0 := by
  contrapose! H
  simpa [H, degree_eq_bot] using hx0

Result:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Proof state:
case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
H : (s.sum f).degree < (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]

Result:
no goals

Proof state:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
simp [hx0, IH]

Result:
no goals

Proof state:
case neg.refine_3
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H✝ : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s

Tactic:
exact H.symm ▸ hy

Result:
no goals

Proof state:
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
by_cases hx0 : f x = 0

Result:
case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Proof state:
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
hx0 : ¬f x = 0
H : f y = 0
⊢ (f x).degree ≠ (f y).degree

Tactic:
simpa [H, degree_eq_bot] using hx0

Result:
no goals

Proof state:
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 degree ∘ f)
⊢ (s.sum f).degree = s.sup fun i => (f i).degree

Tactic:
induction' s using Finset.induction_on with x s hx IH

Result:
case empty
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
h : {i | i ∈ ∅ ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
⊢ (∅.sum f).degree = ∅.sup fun i => (f i).degree

case insert
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f) → (s.sum f).degree = s.sup fun i => (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
⊢ ((insert x s).sum f).degree = (insert x s).sup fun i => (f i).degree