-- 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:
case insert
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
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)

Result:
case insert.inl
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 : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

case insert.inr.inl
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 : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

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

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

Tactic:
simp

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
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
y : S
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:
rw [IH, hy'] at H

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

Proof state:
case insert.inl
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 : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]

Result:
no goals

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)
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
specialize IH (h.mono fun _ => by simp +contextual)

Result:
case insert
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
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Proof state:
case neg.refine_2
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
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

Tactic:
simp [hy, hy0]

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
hy0 : f y ≠ 0
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
refine absurd H (h ?_ ?_ fun H => hx ?_)

Result:
case neg.refine_1
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
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

case neg.refine_2
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
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

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

Proof state:
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)
x✝ : S
⊢ x✝ ∈ {i | i ∈ s ∧ f i ≠ 0} → x✝ ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

Tactic:
simp +contextual

Result:
no goals

Proof state:
case neg.refine_1
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
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

Tactic:
simp [hx0]

Result:
no goals

Proof state:
case insert.inr.inl
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 : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

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

case insert.inr.inl.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 : (f x).degree = (s.sum f).degree
hs : s.Nonempty
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree