awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
obtain : ∀ (a : A) (ha : a ∈ p.support) (he : supDegree D p = D a), Function.invFun D (supDegree D p) ∈ p.support
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D hp

Premises used: AddMonoidAlgebra.exists_supDegree_mem_support
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
hp : p ≠ 0
a : A
ha : a ∈ p.support
he : supDegree D p = D a
rwa : Function.invFun D (D a) ∈ p.support
rwa₁ rwa₂ rwa₃ rwa₄ : a ∈ p.support
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
rwa [he, Function.leftInverse_invFun hD]

Premises used: Function.leftInverse_invFun
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
⊢ leadingCoeff D p = 0 ↔ p = 0

Tactic:
⟨(fun h => ?_).mtr, fun h => h ▸ leadingCoeff_zero⟩

Premises used: Eq.rec, AddMonoidAlgebra.leadingCoeff_zero, Function.mtr, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
refine : ∀ (h : ¬p = 0), ¬leadingCoeff D p = 0
⊢ leadingCoeff D p = 0 ↔ p = 0

Tactic:
refine ⟨(fun h => ?_).mtr, fun h => h ▸ leadingCoeff_zero⟩
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
rw : Function.invFun D (supDegree D p) ∈ p.support
⊢ ¬leadingCoeff D p = 0

Tactic:
rw [leadingCoeff, ← Ne, ← Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff, Ne, AddMonoidAlgebra.leadingCoeff
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
supDegree_mem_support hD h

Premises used: AddMonoidAlgebra.supDegree_mem_support
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ Function.invFun D (supDegree D p) ∈ p.support

Tactic:
exact supDegree_mem_support hD h

Premises used: AddMonoidAlgebra.supDegree_mem_support
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
p : R[A]
D : A → B
inst_3 : AddZeroClass A
hD : Function.Injective D
⊢ leadingCoeff D p ≠ 0 ↔ p ≠ 0

Tactic:
(leadingCoeff_eq_zero hD).ne

Premises used: AddMonoidAlgebra.leadingCoeff_eq_zero, Iff.ne
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
rw : ¬p = q → supDegree D (p - q) < supDegree D p
⊢ supDegree D (p - q) < supDegree D p ∨ p = q

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ ¬p = q → supDegree D (p - q) < supDegree D p

Tactic:
fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_

Premises used: LE.le.lt_of_ne, AddMonoidAlgebra.supDegree_sub_le, LE.le.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
refine_1 : ∀ (he : ¬p = q), max (supDegree D p) (supDegree D q) ≤ supDegree D p
refine_2 : ∀ (he : ¬p = q), supDegree D (p - q) ≠ supDegree D p
⊢ ¬p = q → supDegree D (p - q) < supDegree D p

Tactic:
refine fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_

Premises used: LE.le.lt_of_ne, AddMonoidAlgebra.supDegree_sub_le, LE.le.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
refine_1 : max (supDegree D q) (supDegree D q) ≤ supDegree D q
refine_1₁ refine_1₂ : supDegree D q ≤ supDegree D q
⊢ max (supDegree D p) (supDegree D q) ≤ supDegree D p

Tactic:
rw [hd, sup_idem]

Premises used: sup_idem
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)

Tactic:
rw [← sub_eq_zero, ← leadingCoeff_eq_zero hD, leadingCoeff] at he

Premises used: sub_eq_zero, AddMonoidAlgebra.leadingCoeff_eq_zero, AddMonoidAlgebra.leadingCoeff
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
fun h => he ?_

Premises used: Not
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
refine_2 :
  ∀ (h : supDegree D (p - q) = supDegree D p),
    Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
refine fun h => he ?_
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
A : Type u_3
B : Type u_5
inst : LinearOrder B
inst_1 : OrderBot B
D : A → B
inst_2 : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst_3 : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)
h : supDegree D (p - q) = supDegree D p
refine_2 : Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) (0 : R)
refine_2₁ :
  HSub.hSub (α := R) (β := R) ((p : (a : A) → R) (Function.invFun D (supDegree D p)) : R)
      ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) =
    0
refine_2₂ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D p)) : R) = 0
refine_2₃ : HSub.hSub (β := R) (leadingCoeff D p) ((q : (a : A) → R) (Function.invFun D (supDegree D q)) : R) = 0
refine_2₄ : leadingCoeff D p - leadingCoeff D q = 0
refine_2₅ refine_2₆ refine_2₇ refine_2₈ : leadingCoeff D p = leadingCoeff D q
⊢ Eq.{u_8 + 1} (α := R) ((p - q : (a : A) → R) (Function.invFun D (supDegree D (p - q))) : R) (0 : R)

Tactic:
rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]

Premises used: Finsupp.sub_apply, sub_eq_zero, AddMonoidAlgebra.leadingCoeff
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)

Tactic:
rw [← s.add_sum_erase _ hi]

Premises used: Finset.add_sum_erase
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg :
  ∀ (hs : (s.erase i).Nonempty),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)

Tactic:
by_cases! hs : s.erase i = ∅

Premises used: Finset.erase
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
pos : supDegree D (f i) = supDegree D (f i) ∧ leadingCoeff D (f i) = leadingCoeff D (f i)
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)

Tactic:
rw [hs, Finset.sum_empty, add_zero]

Premises used: Finset.sum_empty, add_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i) = supDegree D (f i) ∧ leadingCoeff D (f i) = leadingCoeff D (f i)

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : s.erase i = ∅
⊢ supDegree D (f i) = supDegree D (f i) ∧ leadingCoeff D (f i) = leadingCoeff D (f i)

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
neg : supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
⊢ supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)

Tactic:
suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)

Tactic:
supDegree_sum_lt ?_ (fun j hj => ?_)

Premises used: AddMonoidAlgebra.supDegree_sum_lt
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs neg : (s.erase i).Nonempty
neg₁ : ∀ (j : ι) (hj : j ∈ s.erase i), supDegree D (f j) < supDegree D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)

Tactic:
refine supDegree_sum_lt ?_ (fun j hj => ?_)

Premises used: AddMonoidAlgebra.supDegree_sum_lt
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ (s.erase i).Nonempty

Tactic:
hs
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ (s.erase i).Nonempty

Tactic:
exact hs
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ∈ s.erase i
⊢ j ≠ i ∧ j ∈ s

Tactic:
rw [Finset.mem_erase] at hj

Premises used: Finset.mem_erase
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
hmax j hj.2 hj.1

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ≠ i ∧ j ∈ s
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
exact hmax j hj.2 hj.1

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst_3 : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
rw rw₁ rw₂ :
  supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
    leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
pos :
  ∀ (hs : s.erase i = ∅),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg neg₁ :
  ∀ (hs : (s.erase i).Nonempty),
    supDegree D (f i + ∑ x ∈ s.erase i, f x) = supDegree D (f i) ∧
      leadingCoeff D (f i + ∑ x ∈ s.erase i, f x) = leadingCoeff D (f i)
neg₂ : ∀ (hs : (s.erase i).Nonempty), supDegree.{u_1, u_3, u_5} (R := R) D (∑ x ∈ s.erase i, f x) < supDegree D (f i)
neg₃ : ∀ (hs : (s.erase i).Nonempty), (s.erase i).Nonempty
neg₄ neg₅ : ∀ (hs : (s.erase i).Nonempty) (j : ι) (hj : j ∈ s.erase i), supDegree D (f j) < supDegree D (f i)
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ j ∈ s, f j) = supDegree D (f i) ∧
    leadingCoeff D (∑ j ∈ s, f j) = leadingCoeff D (f i)

Tactic:
classical
  rw [← s.add_sum_erase _ hi]
  by_cases! hs : s.erase i = ∅
  · rw [hs, Finset.sum_empty, add_zero]; exact ⟨rfl, rfl⟩
  suffices _ from ⟨supDegree_add_eq_left this, leadingCoeff_add_eq_left this⟩
  refine supDegree_sum_lt ?_ (fun j hj => ?_)
  · exact hs
  · rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1

Premises used: AddMonoidAlgebra.supDegree_sum_lt, Finset.mem_erase, Finset.sum_empty, add_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hs : ∃ i ∈ s, f i ≠ 0
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
obtain : ∀ (j : ι) (hj : j ∈ s) (hne : f j ≠ 0), Ne (α := R[A]) (∑ i ∈ s, f i) 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
obtain ⟨j, hj, hne⟩ := hs
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
obtain : ∀ (i : ι) (hi : i ∈ s) (he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
obtain ⟨i, hi, he⟩ := exists_mem_eq_sup _ ⟨j, hj⟩ (supDegree D ∘ f)

Premises used: Function.comp, Finset.exists_mem_eq_sup, AddMonoidAlgebra.supDegree, Exists.intro
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
pos : ∀ (h : ∀ k ∈ s, k = i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
neg : ∀ (h : ∃ k ∈ s, k ≠ i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
by_cases! h : ∀ k ∈ s, k = i
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
(sum_eq_single_of_mem j hj (fun k hk hne => ?_)).trans_ne hne

Premises used: Finset.sum_eq_single_of_mem, Eq.trans_ne
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
pos : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ j), f k = 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
refine (sum_eq_single_of_mem j hj (fun k hk hne => ?_)).trans_ne hne

Premises used: Finset.sum_eq_single_of_mem, Eq.trans_ne
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne_1 : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : k ≠ j
⊢ i ≠ i

Tactic:
rw [h k hk, h j hj] at hne
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne_1 : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ i
⊢ f k = 0

Tactic:
hne.irrefl.elim

Premises used: False.elim, Ne.irrefl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne_1 : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ i
⊢ f k = 0

Tactic:
exact hne.irrefl.elim

Premises used: False.elim, Ne.irrefl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∃ k ∈ s, k ≠ i
neg : ∀ (j : ι) (hj : j ∈ s) (hne : j ≠ i), Ne (α := R[A]) (∑ i ∈ s, f i) 0
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
obtain ⟨j, hj, hne⟩ := h
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
neg : supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≠ ⊥
⊢ Ne (α := R[A]) (∑ i ∈ s, f i) 0

Tactic:
apply ne_zero_of_supDegree_ne_bot (D := D)

Premises used: AddMonoidAlgebra.ne_zero_of_supDegree_ne_bot
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ i), supDegree D (f k) < supDegree D (f i)

Tactic:
have (k) (hk : k ∈ s) (hne : k ≠ i) : supDegree D (f k) < supDegree D (f i) :=
    ((le_sup hk).trans_eq he).lt_of_ne (hd.ne hk hi hne)
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ i), supDegree D (f k) < supDegree D (f i)
neg : supDegree D (f i) ≠ ⊥
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≠ ⊥

Tactic:
rw [(supDegree_leadingCoeff_sum_eq hi this).1]

Premises used: AddMonoidAlgebra.supDegree_leadingCoeff_sum_eq, And.left
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : LinearOrder B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst_3 : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) (↑s : Set ι)
j_1 : ι
hj_1 : j_1 ∈ s
hne_1 : f j_1 ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
this : ∀ (k : ι) (hk : k ∈ s) (hne : k ≠ i), supDegree D (f k) < supDegree D (f i)
⊢ supDegree D (f i) ≠ ⊥

Tactic:
(this j hj hne).ne_bot

Premises used: LT.lt.ne_bot