-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).maximum

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : List.map natDegree l = []
⊢ l.sum = 0

Tactic:
rw [List.map_eq_nil_iff] at h

Result:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : l = []
⊢ l.sum = 0

Proof state:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
this : (List.map natDegree l).maximum = ↑(List.foldr max 0 (List.map natDegree l))
⊢ ↑l.sum.natDegree ≤ ↑(List.foldr max 0 (List.map natDegree l))

Tactic:
simpa using natDegree_list_sum_le l

Result:
no goals

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ ↑(List.foldr max ⊥ (List.map natDegree l)) = ↑(List.foldr max 0 (List.map natDegree l))

Tactic:
congr

Result:
no goals

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ ↑l.sum.natDegree ≤ (List.map natDegree l).maximum

Tactic:
suffices (l.map natDegree).maximum = ((l.map natDegree).foldr max 0 : ℕ) by
  rw [this]
  simpa using natDegree_list_sum_le l

Result:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ (List.map natDegree l).maximum = ↑(List.foldr max 0 (List.map natDegree l))

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ List.map natDegree l ≠ []

Tactic:
contrapose! h

Result:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : List.map natDegree l = []
⊢ l.sum = 0

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

Tactic:
rw [degree_eq_natDegree h]

Result:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ ↑l.sum.natDegree ≤ (List.map natDegree l).maximum

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : l = []
⊢ l.sum = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ (List.map natDegree l).maximum = ↑(List.foldr max 0 (List.map natDegree l))

Tactic:
rw [← List.foldr_max_of_ne_nil]

Result:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ ↑(List.foldr max ⊥ (List.map natDegree l)) = ↑(List.foldr max 0 (List.map natDegree l))

case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ List.map natDegree l ≠ []

Proof state:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

Tactic:
by_cases h : l.sum = 0

Result:
case pos
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : l.sum = 0
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

Proof state:
case pos
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : l.sum = 0
⊢ l.sum.degree ≤ (List.map natDegree l).maximum

Tactic:
simp [h]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
this : (List.map natDegree l).maximum = ↑(List.foldr max 0 (List.map natDegree l))
⊢ ↑l.sum.natDegree ≤ (List.map natDegree l).maximum

Tactic:
rw [this]

Result:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
h : ¬l.sum = 0
this : (List.map natDegree l).maximum = ↑(List.foldr max 0 (List.map natDegree l))
⊢ ↑l.sum.natDegree ≤ ↑(List.foldr max 0 (List.map natDegree l))