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 : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : Add A
inst_4 : Add B
inst_5 : AddLeftMono B
inst_6 : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
grw : (f.support + g.support).sup degb ≤ f.support.sup degb + g.support.sup degb
grw₁ grw₂ grw₃ grw₄ :
  ∀ (_fd : A) (fds : _fd ∈ f.support) (_gd : A) (gds : _gd ∈ g.support),
    degb (_fd + _gd) ≤ f.support.sup degb + g.support.sup degb
⊢ (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb

Tactic:
classical
  grw [support_mul, Finset.sup_add_le]
  rintro _fd fds _gd gds
  grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]

Premises used: Finset.sup_add_le, AddMonoidAlgebra.support_mul
-- 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 : Semiring R
inst_3 : Add A
inst_4 : Add T
inst_5 : AddLeftMono T
inst_6 : AddRightMono T
degt : A → T
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
f g : R[A]
⊢ f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt

Tactic:
sup_support_mul_le (B := Tᵒᵈ) degtm f g

Premises used: AddMonoidAlgebra.sup_support_mul_le, OrderDual, Finset.inf
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
rw : ∀ (b : A), Membership.mem (γ := Finset A) (Finsupp.support.{u_3, u_1} (M := R) 1) b → degb b ≤ 0
⊢ Finset.sup (Finsupp.support.{u_3, u_1} (M := R) (List.prod [])) degb ≤
    List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) [])

Tactic:
rw [List.map_nil, Finset.sup_le_iff, List.prod_nil, List.sum_nil]

Premises used: List.sum_nil, List.prod_nil, Finset.sup_le_iff, List.map_nil
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
a : A
ha : Membership.mem (γ := Finset A) (Finsupp.support.{u_3, u_1} (M := R) 1) a
rwa rwa₁ rwa₂ rwa₃ : degb 0 ≤ 0
⊢ degb a ≤ 0

Tactic:
rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]

Premises used: Finset.mem_singleton, Iff.mp, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
⊢ ∀ (b : A), Membership.mem (γ := Finset A) (Finsupp.support.{u_3, u_1} (M := R) 1) b → degb b ≤ 0

Tactic:
exact fun a ha => by rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
f : R[A]
fs : List R[A]
rw : (f * fs.prod).support.sup degb ≤ f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
⊢ (f :: fs).prod.support.sup degb ≤ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) (f :: fs))

Tactic:
rw [List.prod_cons, List.map_cons, List.sum_cons]

Premises used: List.map_cons, List.sum_cons, List.prod_cons
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
f : R[A]
fs : List R[A]
grw :
  f.support.sup degb + fs.prod.support.sup degb ≤
    f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
grw₁ grw₂ :
  f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs) ≤
    f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)
⊢ (f * fs.prod).support.sup degb ≤ f.support.sup degb + List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) fs)

Tactic:
grw [sup_support_mul_le degbm, sup_support_list_prod_le degb0 degbm]

Premises used: AddMonoidAlgebra.sup_support_mul_le
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
⊢ List.sum (List.map (fun (f : R[A]) ↦ f.support.inf degt) l) ≤ l.prod.support.inf degt

Tactic:
OrderDual.ofDual_le_ofDual.mpr ?_

Premises used: Iff.mpr, OrderDual.ofDual_le_ofDual, Multiset.foldr, Finset.fold, List.sum, Finset.inf, Multiset.fold
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
refine :
  LE.le (α := Tᵒᵈ)
    (Quot.lift (r := (⇑(List.isSetoid T) : List T → List T → Prop))
      (fun (l : List T) ↦ List.foldr (fun (x1 x2 : T) ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.support.val))
    (List.foldr (fun (x1 x2 : T) ↦ x1 + x2) 0 (List.map (fun (f : R[A]) ↦ f.support.inf degt) l))
⊢ List.sum (List.map (fun (f : R[A]) ↦ f.support.inf degt) l) ≤ l.prod.support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr ?_

Premises used: Iff.mpr, OrderDual.ofDual_le_ofDual
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
⊢ LE.le (α := Tᵒᵈ)
    (Quot.lift (r := (⇑(List.isSetoid T) : List T → List T → Prop))
      (fun (l : List T) ↦ List.foldr (fun (x1 x2 : T) ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.support.val))
    (List.foldr (fun (x1 x2 : T) ↦ x1 + x2) 0 (List.map (fun (f : R[A]) ↦ f.support.inf degt) l))

Tactic:
sup_support_list_prod_le ?_ ?_ l

Premises used: AddMonoidAlgebra.sup_support_list_prod_le, Multiset.foldr, Finset.fold, List.sum, Finset.sup, OrderDual, Finset.inf, Multiset.fold
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
refine_1 : degt 0 ≤ 0
refine_2 : ∀ (a b : A), degt (a + b) ≤ degt a + degt b
⊢ LE.le (α := Tᵒᵈ)
    (Quot.lift (r := (⇑(List.isSetoid T) : List T → List T → Prop))
      (fun (l : List T) ↦ List.foldr (fun (x1 x2 : T) ↦ x1 ⊓ x2) ⊤ l) ⋯ (Multiset.map degt l.prod.support.val))
    (List.foldr (fun (x1 x2 : T) ↦ x1 + x2) 0 (List.map (fun (f : R[A]) ↦ f.support.inf degt) l))

Tactic:
refine sup_support_list_prod_le ?_ ?_ l

Premises used: AddMonoidAlgebra.sup_support_list_prod_le
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
⊢ degt 0 ≤ 0

Tactic:
(OrderDual.ofDual_le_ofDual.mp ?_)

Premises used: OrderDual.ofDual_le_ofDual, Iff.mp
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
refine_1 : LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) 0 : T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt 0) : T)
⊢ degt 0 ≤ 0

Tactic:
refine (OrderDual.ofDual_le_ofDual.mp ?_)

Premises used: OrderDual.ofDual_le_ofDual, Iff.mp
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
⊢ LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) 0 : T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt 0) : T)

Tactic:
degt0
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
⊢ LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) 0 : T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt 0) : T)

Tactic:
exact degt0
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b

Tactic:
(fun a b => OrderDual.ofDual_le_ofDual.mp ?_)

Premises used: OrderDual.ofDual_le_ofDual, Iff.mp
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
refine_2 :
  ∀ (a b : A),
    LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt a + degt b) : T)
      ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt (a + b)) : T)
⊢ ∀ (a b : A), degt (a + b) ≤ degt a + degt b

Tactic:
refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)

Premises used: OrderDual.ofDual_le_ofDual, Iff.mp
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
a b : A
⊢ LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt a + degt b) : T)
    ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt (a + b)) : T)

Tactic:
degtm a b
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
l : List R[A]
a b : A
⊢ LE.le (α := T) ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt a + degt b) : T)
    ((OrderDual.ofDual : (a : Tᵒᵈ) → T) (degt (a + b)) : T)

Tactic:
exact degtm a b
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
n : ℕ
f : R[A]
rw : (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum
⊢ (f ^ n).support.sup degb ≤ n • f.support.sup degb

Tactic:
rw [← List.prod_replicate, ← List.sum_replicate]

Premises used: List.sum_replicate, List.prod_replicate
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
n : ℕ
f : R[A]
⊢ (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum

Tactic:
(sup_support_list_prod_le degb0 degbm _).trans_eq ?_

Premises used: AddMonoidAlgebra.sup_support_list_prod_le, LE.le.trans_eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
n : ℕ
f : R[A]
refine :
  List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) (List.replicate n f)) =
    (List.replicate n (f.support.sup degb)).sum
⊢ (List.replicate n f).prod.support.sup degb ≤ (List.replicate n (f.support.sup degb)).sum

Tactic:
refine (sup_support_list_prod_le degb0 degbm _).trans_eq ?_

Premises used: AddMonoidAlgebra.sup_support_list_prod_le, LE.le.trans_eq
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
inst : SemilatticeSup B
inst_1 : OrderBot B
inst_2 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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
n : ℕ
f : R[A]
rw rw₁ : (List.replicate n (f.support.sup degb)).sum = (List.replicate n (f.support.sup degb)).sum
⊢ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) (List.replicate n f)) =
    (List.replicate n (f.support.sup degb)).sum

Tactic:
rw [List.map_replicate]

Premises used: List.map_replicate
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
n : ℕ
f : R[A]
⊢ n • f.support.inf degt ≤ (f ^ n).support.inf degt

Tactic:
OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f

Premises used: Iff.mpr, OrderDual.ofDual_le_ofDual, Multiset.foldr, Finset.fold, AddMonoidAlgebra.sup_support_pow_le, Iff.mp, Finset.inf, Multiset.fold
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
n : ℕ
f : R[A]
refine_1 :
  LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)
refine_2 :
  ∀ (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ᵒᵈ)
⊢ n • f.support.inf degt ≤ (f ^ n).support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f

Premises used: Iff.mpr, OrderDual.ofDual_le_ofDual, AddMonoidAlgebra.sup_support_pow_le, Iff.mp
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
n : ℕ
f : R[A]
⊢ LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)

Tactic:
degt0
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
n : ℕ
f : R[A]
⊢ LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)

Tactic:
exact degt0
-- 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
n : ℕ
f : 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 : Semiring R
inst_3 : AddMonoid A
inst_4 : AddMonoid 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)
n : ℕ
f : 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
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
m : Multiset R[A]
h :
  ∀ (a : List R[A]),
    (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a)).support.sup degb ≤
      Multiset.sum
        (Multiset.map (fun (f : R[A]) ↦ f.support.sup degb)
          (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a))
⊢ m.prod.support.sup degb ≤ Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.sup degb) m)

Tactic:
induction m using Quot.inductionOn
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
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
a : List R[A]
h : a.prod.support.sup degb ≤ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) a)
⊢ (Multiset.prod (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a)).support.sup degb ≤
    Multiset.sum
      (Multiset.map (fun (f : R[A]) ↦ f.support.sup degb)
        (Quot.mk (⇑(List.isSetoid R[A]) : List R[A] → List R[A] → Prop) a))

Tactic:
rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]

Premises used: Multiset.sum_coe, Multiset.map_coe, Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
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
a : List R[A]
⊢ a.prod.support.sup degb ≤ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) a)

Tactic:
sup_support_list_prod_le degb0 degbm _

Premises used: AddMonoidAlgebra.sup_support_list_prod_le
-- Module: Mathlib.Algebra.MonoidAlgebra.Degree
Goal:
R : Type u_1
A : Type u_3
B : Type u_5
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
a : List R[A]
⊢ a.prod.support.sup degb ≤ List.sum (List.map (fun (f : R[A]) ↦ f.support.sup degb) a)

Tactic:
exact sup_support_list_prod_le degb0 degbm _

Premises used: AddMonoidAlgebra.sup_support_list_prod_le
-- 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]
⊢ Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.inf degt) m) ≤ m.prod.support.inf degt

Tactic:
OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m

Premises used: Multiset.sum, Iff.mpr, OrderDual.ofDual_le_ofDual, Multiset.foldr, Finset.fold, AddMonoidAlgebra.sup_support_multiset_prod_le, Iff.mp, Finset.inf, Multiset.fold
-- 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]
refine_1 :
  LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)
refine_2 :
  ∀ (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ᵒᵈ)
⊢ Multiset.sum (Multiset.map (fun (f : R[A]) ↦ f.support.inf degt) m) ≤ m.prod.support.inf degt

Tactic:
refine OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m

Premises used: Iff.mpr, OrderDual.ofDual_le_ofDual, AddMonoidAlgebra.sup_support_multiset_prod_le, Iff.mp
-- 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]
⊢ LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)

Tactic:
degt0
-- 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]
⊢ LE.le (α := Tᵒᵈ) ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) (degt 0) : Tᵒᵈ)
    ((OrderDual.ofDual : (a : Tᵒᵈᵒᵈ) → Tᵒᵈ) 0 : Tᵒᵈ)

Tactic:
exact degt0