awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) a) + p.degree = p.degree

Tactic:
simp [left_ne_zero_of_mul h]

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
inst : Semiring R
f g : R[X]
⊢ (f * g).coeff (f.natDegree + g.natDegree) = f.coeff f.natDegree * g.coeff g.natDegree

Tactic:
simp only [coeff_natDegree, coeff_mul_degree_add_degree]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_mul_degree_add_degree
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p q : R[X]
h : p.natDegree + q.natDegree < m + n
⊢ (p * q).coeff (m + n) = 0

Tactic:
coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt h)

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.natDegree_mul_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (HPow.hPow (β := ℕ) p 0).coeff (0 * n) = HPow.hPow (β := ℕ) (p.coeff n) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m_1 n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
rw : (p ^ m).natDegree ≤ m * n
⊢ (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)

Tactic:
rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]

Premises used: pow_succ, Polynomial.coeff_mul_add_eq_of_natDegree_le, Nat.succ_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m_1 n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
natDegree_pow_le.trans (le_trans ?_ (le_refl _))

Premises used: le_refl, Polynomial.natDegree_pow_le, LE.le.trans, le_trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m_1 n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
refine : m * p.natDegree ≤ m * n
⊢ (p ^ m).natDegree ≤ m * n

Tactic:
refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))

Premises used: le_refl, Polynomial.natDegree_pow_le, LE.le.trans, le_trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m_1 n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ m * p.natDegree ≤ m * n

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
zero : (HPow.hPow (β := ℕ) p 0).coeff (0 * n) = HPow.hPow (β := ℕ) (p.coeff n) 0
succ : ∀ (m : ℕ) (hm : (p ^ m).coeff (m * n) = p.coeff n ^ m), (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m

Tactic:
induction m with
  | zero => simp
  | succ m hm =>
    rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
    refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
    gcongr

Premises used: le_refl, pow_succ, Polynomial.coeff_mul_add_eq_of_natDegree_le, Nat.succ_mul, Polynomial.natDegree_pow_le, LE.le.trans, le_trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
inl : ∀ (mno : m * n ≤ m * n), (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0
inr : ∀ (h : o ≠ m * n), (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
rcases eq_or_ne o (m * n) with rfl | h

Premises used: HMul.hMul, eq_or_ne, rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0

Tactic:
simpa only [ite_true] using coeff_pow_of_natDegree_le pn

Premises used: ite_true, Polynomial.coeff_pow_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
h : o ≠ m * n
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0

Tactic:
simpa only [h, ite_false] using coeff_eq_zero_of_natDegree_lt <|
      lt_of_le_of_lt (natDegree_pow_le_of_le m pn) (lt_of_le_of_ne mno h.symm)

Premises used: lt_of_le_of_lt, ite_false, Ne.symm, Polynomial.natDegree_pow_le_of_le, Polynomial.coeff_eq_zero_of_natDegree_lt, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Semiring R
p q : R[X]
qn : q.natDegree < n
⊢ (p + q).coeff n = p.coeff n

Tactic:
(coeff_add _ _ _).trans <|
    (congr_arg _ <| coeff_eq_zero_of_natDegree_lt <| qn).trans <| add_zero _

Premises used: Polynomial.coeff_add, congr_arg, Polynomial.coeff_eq_zero_of_natDegree_lt, add_zero, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Semiring R
p q : R[X]
pn : p.natDegree < n
rw : (q + p).coeff n = q.coeff n
⊢ (p + q).coeff n = q.coeff n

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (q + p).coeff n = q.coeff n

Tactic:
coeff_add_eq_left_of_lt pn

Premises used: Polynomial.coeff_add_eq_left_of_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
n : ℕ
inst : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (q + p).coeff n = q.coeff n

Tactic:
exact coeff_add_eq_left_of_lt pn

Premises used: Polynomial.coeff_add_eq_left_of_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH :
  ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)), (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ ((Insert.insert x s).sum f).degree = (Insert.insert x s).sup fun (i : S) ↦ (f i).degree

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

Premises used: Finset.sup_insert, Finset.sum_insert, not_false_iff
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH :
  ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)), (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
x_1 : S
⊢ Membership.mem (γ := Set S) {i : S | i ∈ s ∧ f i ≠ 0} x_1 →
    Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} x_1

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH :
  ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)), (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree

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

Premises used: Set.Pairwise.mono
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
insert :
  ∀ (H : (f x).degree < (s.sum f).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
insert₁ :
  ∀ (H : (f x).degree = (s.sum f).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
insert₂ :
  ∀ (H : (s.sum f).degree < (f x).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

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

Premises used: Polynomial.degree, Finset.sum, lt_trichotomy
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree < (s.sum f).degree
insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree
insert₁ : (f x + ∑ x ∈ s, f x).degree = (s.sum f).degree
insert₂ insert₃ : (s.sum f).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

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

Premises used: Iff.mpr, Polynomial.degree_add_eq_right_of_degree_lt, LT.lt.le, sup_eq_right
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
insert :
  ∀ (hx : x ∉ ∅)
    (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) (Insert.insert x ∅) i ∧ f i ≠ 0} (Ne on degree ∘ f))
    (IH : (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree) (H : (f x).degree = (Finset.sum ∅ f).degree),
    (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (sup ∅ fun (i : S) ↦ (f i).degree)
insert₁ : ∀ (hs : s.Nonempty), (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

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

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
hx : x ∉ ∅
h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) (insert x ∅) i ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
H : (f x).degree = (Finset.sum ∅ f).degree
⊢ (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (sup ∅ fun (i : S) ↦ (f i).degree)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
insert :
  ∀ (y : S) (hy : y ∈ s) (hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

Tactic:
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)

Premises used: Polynomial.degree, Finset.exists_mem_eq_sup
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
insert :
  ∀ (hs : s.Nonempty) (y : S) (H : (f x).degree = (f y).degree) (hy : y ∈ s)
    (hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

Tactic:
rw [IH, hy'] at H
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
pos : ∀ (hx0 : f x = 0), (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
neg : ∀ (hx0 : ¬f x = 0), (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

Tactic:
by_cases hx0 : f x = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

Tactic:
simp [hx0, IH]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
contrapose! : ∀ (H : f y = 0), (f x).degree ≠ (f y).degree
⊢ f y ≠ 0

Tactic:
contrapose! H
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (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

Premises used: Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
⊢ f y ≠ 0

Tactic:
have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

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

Premises used: absurd
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
neg : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} x
neg₁ : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} y
neg₂ : ∀ (H : x = y), x ∈ s
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

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

Premises used: absurd
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} x

Tactic:
simp [hx0]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} y

Tactic:
simp [hy, hy0]
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H_1 : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s

Tactic:
H.symm ▸ hy

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
hs : s.Nonempty
y : S
H_1 : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s

Tactic:
exact H.symm ▸ hy
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (s.sum f).degree < (f x).degree
insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree
insert₁ : (f x + ∑ x ∈ s, f x).degree = (f x).degree
insert₂ insert₃ : (f x).degree = (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)

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

Premises used: Iff.mpr, sup_eq_left, LT.lt.le, Polynomial.degree_add_eq_left_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
empty :
  ∀ (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)),
    (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
insert :
  ∀ (x : S) (s : Finset S) (hx : x ∉ s)
    (IH :
      ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)),
        (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree)
    (h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)),
    ((Insert.insert x s).sum f).degree = (Insert.insert x s).sup fun (i : S) ↦ (f i).degree
⊢ (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]

Premises used: Finset.sup_insert, Insert.insert, Finset.sum_insert, not_false_iff, rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
empty :
  ∀ (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)),
    (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
insert :
  ∀ (x : S) (s : Finset S) (hx : x ∉ s)
    (IH :
      ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)),
        (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree)
    (h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)),
    ((Insert.insert x s).sum f).degree = (Insert.insert x s).sup fun (i : S) ↦ (f i).degree
⊢ (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]

Premises used: Finset.sup_insert, Insert.insert, Finset.sum_insert, not_false_iff, rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
pos : ∀ (H : ∃ x ∈ s, f x ≠ 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
neg : ∀ (H : ∀ (x : S) (_ : x ∈ s), f x = 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree

Tactic:
by_cases! H : ∃ x ∈ s, f x ≠ 0
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∃ x ∈ s, f x ≠ 0
pos : ∀ (x : S) (hx : x ∈ s) (hx' : f x ≠ 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree

Tactic:
obtain ⟨x, hx, hx'⟩ := H
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
⊢ s.Nonempty

Tactic:
have hs : s.Nonempty := ⟨x, hx⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.Lemmas
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree

Tactic:
natDegree_eq_of_degree_eq_some ?_

Premises used: Polynomial.natDegree_eq_of_degree_eq_some