awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt (a + b)) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt a + degt b) : Tᵒᵈ)

Tactic:
degtm _ _
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
m : Multiset R[A]
a b : A
⊢ LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt (a + b)) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt a + degt b) : Tᵒᵈ)

Tactic:
exact degtm _ _
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
ι : Type u_6
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
s : Finset ι
f : ι → R[A]
⊢ Finset.sup (Finsupp.support.{u_3, u_1} (M := R) (∏ i ∈ s, f i)) degb ≤ ∑ i ∈ s, (f i).support.sup degb

Tactic:
(sup_support_multiset_prod_le degb0 degbm _).trans_eq <| congr_arg _ <| Multiset.map_map _ _ _

Premises used: LE.le.trans_eq, AddMonoidAlgebra.sup_support_multiset_prod_le, congr_arg, Multiset.map_map
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
rw :
  Eq.{u_4 + 1} (α := T) (∑ i ∈ s, (f i).support.inf degt)
    (Multiset.sum (Multiset.map ((fun (f : R[A]) ↦ f.support.inf degt) ∘ fun (i : ι) ↦ f i) s.val))
⊢ Eq.{u_4 + 1} (α := T) (∑ i ∈ s, (f i).support.inf degt)
    (Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.inf degt) (Multiset.map (fun (i : ι) ↦ f i) s.val)))

Tactic:
rw [Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst : SemilatticeInf T
inst_1 : OrderTop T
inst_2 : CommSemiring R
inst_3 : AddCommMonoid A
inst_4 : AddCommMonoid T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ Eq.{u_4 + 1} (α := T) (∑ i ∈ s, (f i).support.inf degt)
    (Multiset.sum (Multiset.map ((fun (f : R[A]) ↦ f.support.inf degt) ∘ fun (i : ι) ↦ f i) s.val))

Tactic:
rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f g : R[A]
⊢ supDegree D (f + g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
sup_support_add_le D f g

Premises used: AddMonoidAlgebra.sup_support_add_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f : R'[A]
rw : (-f).support.sup D = supDegree D f
rw₁ : (-f).support.sup D = f.support.sup D
rw₂ rw₃ : f.support.sup D = f.support.sup D
⊢ supDegree D (-f) = supDegree D f

Tactic:
rw [supDegree, supDegree, Finsupp.support_neg]

Premises used: AddMonoidAlgebra.supDegree, Finsupp.support_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f g : R'[A]
rw : supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
⊢ supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
rw [sub_eq_add_neg, ← supDegree_neg (f := g)]

Premises used: sub_eq_add_neg, AddMonoidAlgebra.supDegree_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R' : Type u_2
A : Type u_3
B : Type u_5
inst : Ring R'
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)

Tactic:
apply supDegree_add_le

Premises used: AddMonoidAlgebra.supDegree_add_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≤ s.sup fun (i : ι) ↦ supDegree D (f i)

Tactic:
(Finset.sup_mono Finsupp.support_finsetSum).trans_eq (Finset.sup_biUnion _ _)

Premises used: LE.le.trans_eq, Finsupp.support_finsetSum, Finset.sup_mono, Finset.sup_biUnion, AddMonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≤ s.sup fun (i : ι) ↦ supDegree D (f i)

Tactic:
exact (Finset.sup_mono Finsupp.support_finsetSum).trans_eq (Finset.sup_biUnion _ _)

Premises used: LE.le.trans_eq, Finsupp.support_finsetSum, Finset.sup_mono, Finset.sup_biUnion
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_1, u_3, u_5} (R := R) D (∑ i ∈ s, f i) ≤ s.sup fun (i : ι) ↦ supDegree D (f i)

Tactic:
classical
  exact (Finset.sup_mono Finsupp.support_finsetSum).trans_eq (Finset.sup_biUnion _ _)

Premises used: LE.le.trans_eq, Finsupp.support_finsetSum, Finset.sup_mono, Finset.sup_biUnion
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
hr : r ≠ 0
rw : (Finsupp.support (single a r)).sup D = D a
rw₁ : Finset.sup {a} D = D a
rw₂ rw₃ : D a = D a
⊢ supDegree D (single a r) = D a

Tactic:
rw [supDegree, Finsupp.support_single a hr, Finset.sup_singleton]

Premises used: Finsupp.support_single, Finset.sup_singleton, AddMonoidAlgebra.supDegree
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
pos : ∀ (hr : r = 0), supDegree D (single a r) = ⊥
neg : ∀ (hr : ¬r = 0), supDegree D (single a r) = D a
⊢ supDegree D (single a r) = if r = 0 then ⊥ else D a

Tactic:
split_ifs with hr
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
hr : r = 0
⊢ supDegree D (single a r) = ⊥

Tactic:
simp [supDegree_single_ne_zero, hr]

Premises used: AddMonoidAlgebra.supDegree_single_ne_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
a : A
r : R
hr : ¬r = 0
⊢ supDegree D (single a r) = D a

Tactic:
simp [supDegree_single_ne_zero, hr]

Premises used: AddMonoidAlgebra.supDegree_single_ne_zero
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
a : A
hlt : ¬D a ≤ supDegree D p
contrapose! : ∀ (hlt : Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)), D a ≤ supDegree D p
⊢ Eq.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)

Tactic:
contrapose! hlt
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
a : A
hlt : Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)
⊢ D a ≤ supDegree D p

Tactic:
Finset.le_sup (Finsupp.mem_support_iff.2 hlt)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finset.le_sup
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
a : A
hlt : Ne.{u_1 + 1} (α := R) ((p : (a : A) → R) a : R) (0 : R)
⊢ D a ≤ supDegree D p

Tactic:
exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)

Premises used: Iff.mpr, Finsupp.mem_support_iff, Finset.le_sup
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
s : R[A]
hs : s.support.Nonempty
rw : (↑(s.support.sup' hs D) : WithBot B) = (↑(s.support.sup D) : WithBot B)
rw₁ rw₂ : (↑(s.support.sup D) : WithBot B) = (↑(s.support.sup D) : WithBot B)
⊢ s.support.sup (WithBot.some ∘ D) = (↑(s.support.sup D) : WithBot B)

Tactic:
rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]

Premises used: Finset.coe_sup', Finset.sup'_eq_sup
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
a : A
hmem : a ∈ p.support
hmax : IsMaxOn D (↑p.support : Set A) a
⊢ supDegree D p = D a

Tactic:
sup_eq_of_isMaxOn hmem hmax

Premises used: sup_eq_of_isMaxOn
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
⊢ supDegree.{u_1, u_3, u_5} (R := R) D 0 = ⊥

Tactic:
simp [supDegree]

Premises used: AddMonoidAlgebra.supDegree
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
⊢ supDegree D p ≠ ⊥ → p ≠ 0

Tactic:
mt (fun h => h ▸ supDegree_zero)

Premises used: AddMonoidAlgebra.supDegree_zero, mt, Eq.rec, 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 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
b : B
h : ¬supDegree D p ≤ b
⊢ p ≠ 0

Tactic:
ne_zero_of_supDegree_ne_bot (fun he => h <| he ▸ bot_le)

Premises used: Eq.rec, AddMonoidAlgebra.ne_zero_of_supDegree_ne_bot, Eq.symm, bot_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p : R[A]
inst_3 : AddZeroClass A
b : B
hb : b ∈ Set.range D
hmem : Function.invFun D b ∈ p.support
hmax : ∀ a ∈ p.support, D a ≤ b
⊢ supDegree D p = b

Tactic:
sup_eq_of_max hb hmem hmax

Premises used: sup_eq_of_max
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
⊢ supDegree D (p * q) ≤ supDegree D p + supDegree D q

Tactic:
sup_support_mul_le (fun {_ _} => (hadd _ _).le) p q

Premises used: Eq.le, AddMonoidAlgebra.sup_support_mul_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)

Tactic:
s.induction ?_ ?_

Premises used: Finset.induction
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
refine_1 : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
refine_2 :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)

Tactic:
refine s.induction ?_ ?_
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
refine_1 : (if Eq.{u_7 + 1} (α := R) 1 0 then ⊥ else D 0) ≤ 0
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)

Tactic:
rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]

Premises used: Finset.prod_empty, AddMonoidAlgebra.supDegree_single, Finset.sum_empty, AddMonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
pos : Eq.{u_7 + 1} (α := R) 1 0 → LE.le.{u_9} (α := B) ⊥ 0
neg : ¬Eq.{u_7 + 1} (α := R) 1 0 → D 0 ≤ 0
⊢ (if Eq.{u_7 + 1} (α := R) 1 0 then ⊥ else D 0) ≤ 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h : Eq.{u_7 + 1} (α := R) 1 0
⊢ LE.le.{u_9} (α := B) ⊥ 0

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h : ¬Eq.{u_7 + 1} (α := R) 1 0
⊢ D 0 ≤ 0

Tactic:
hzero.le

Premises used: Eq.le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
h : Eq.{u_7 + 1} (α := R) 1 0
⊢ LE.le.{u_9} (α := B) ⊥ 0

Tactic:
exacts [bot_le, hzero.le]

Premises used: Eq.le, bot_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s_1 : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
ih : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
refine_2 : supDegree D (f i * ∏ x ∈ s, f x) ≤ supDegree D (f i) + ∑ x ∈ s, supDegree D (f x)
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ insert i s, f i) ≤ ∑ i ∈ insert i s, supDegree D (f i)

Tactic:
rw [Finset.prod_insert his, Finset.sum_insert his]

Premises used: Finset.prod_insert, Finset.sum_insert
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s_1 : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
ih : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
⊢ supDegree D (f i) + supDegree.{u_7, u_8, u_9} (R := R) D (∏ x ∈ s, f x) ≤
    supDegree D (f i) + ∑ x ∈ s, supDegree D (f x)

Tactic:
gcongr
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s_1 : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
ih : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
⊢ supDegree D (f i * ∏ x ∈ s, f x) ≤ supDegree D (f i) + ∑ x ∈ s, supDegree D (f x)

Tactic:
exact (supDegree_mul_le hadd).trans (by gcongr)

Premises used: AddMonoidAlgebra.supDegree_mul_le, LE.le.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_7
A : Type u_8
B : Type u_9
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : SemilatticeSup B
inst_4 : OrderBot B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
refine_1 : supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
refine_2 refine_2₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
        supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
⊢ supDegree.{u_7, u_8, u_9} (R := R) D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)

Tactic:
classical
  refine s.induction ?_ ?_
  · rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
    split_ifs; exacts [bot_le, hzero.le]
  · intro i s his ih
    rw [Finset.prod_insert his, Finset.sum_insert his]
    exact (supDegree_mul_le hadd).trans (by gcongr)

Premises used: Finset.prod_empty, AddMonoidAlgebra.supDegree_single, Eq.le, AddMonoidAlgebra.supDegree_mul_le, Finset.sum_empty, LE.le.trans, bot_le, AddMonoidAlgebra.one_def
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
simp_rw :
  (∑ x ∈ p.support,
      ∑ x_1 ∈ q.support,
        if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
⊢ (p * q : (a : A) → R) (ap + aq) = HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)

Tactic:
simp_rw [mul_apply, Finsupp.sum]

Premises used: AddMonoidAlgebra.mul_apply, Finsupp.sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h₀ :
  ∀ b ∈ q.support,
    b ≠ aq →
      (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R)
        else 0) =
        0
h₁ :
  aq ∉ q.support →
    (if ap + aq = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)
      else 0) =
      0
h₂ :
  ∀ b ∈ p.support,
    b ≠ ap →
      Eq.{u_1 + 1} (α := R)
        (∑ x ∈ q.support,
          if b + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) b : R) ((q : (a : A) → R) x : R)
          else 0)
        0
h₃ :
  ap ∉ p.support →
    Eq.{u_1 + 1} (α := R)
      (∑ x ∈ q.support,
        if ap + x = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) x : R)
        else 0)
      0
⊢ (∑ x ∈ p.support,
      ∑ x_1 ∈ q.support,
        if x + x_1 = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) x : R) ((q : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) aq : R)

Tactic:
rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]

Premises used: if_pos, Finset.sum_eq_single, rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ q.support,
    b ≠ aq →
      (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R)
        else 0) =
        0

Tactic:
fun a ha hne => if_neg (fun he => ?_)

Premises used: if_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
h₀ : ∀ (a : A) (ha : a ∈ q.support) (hne : a ≠ aq) (he : ap + a = ap + aq), False
⊢ ∀ b ∈ q.support,
    b ≠ aq →
      (if ap + b = ap + aq then HMul.hMul (α := R) (β := R) ((p : (a : A) → R) ap : R) ((q : (a : A) → R) b : R)
        else 0) =
        0

Tactic:
refine fun a ha hne => if_neg (fun he => ?_)

Premises used: if_neg
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ q.support
hne : a ≠ aq
he : ap + a = ap + aq
⊢ D (ap + a) = D (ap + aq)

Tactic:
apply_fun D at he
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : Semiring R
inst_1 : SemilatticeSup B
inst_2 : OrderBot B
D : A → B
p q : R[A]
inst_3 : AddZeroClass A
inst_4 : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst_5 : AddLeftStrictMono B
inst_6 : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ q.support
hne : a ≠ aq
he : D (ap + a) = D (ap + aq)
⊢ D ap + D a = D ap + D aq

Tactic:
simp_rw [hadd] at he