R : Type u_3
A : Type u_2
T : Type u_1
B : Type ?u.19667
ι : Type ?u.19670
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
⊢ ∀ {a b : A}, degt (a + b) ≤ degt a + degt b
R : Type u_3
A : Type u_2
T : Type u_1
B : Type ?u.19667
ι : Type ?u.19670
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
⊢ Finset.inf f.support degt + Finset.inf g.support degt ≤ Finset.inf (f * g).support degt
refine' OrderDual.ofDual_le_ofDual.mpr <| sup_support_mul_le (_) f g
R : Type u_3
A : Type u_2
T : Type u_1
B : Type ?u.19667
ι : Type ?u.19670
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
a b : A
⊢ degt (a + b) ≤ degt a + degt b
R : Type u_3
A : Type u_2
T : Type u_1
B : Type ?u.19667
ι : Type ?u.19670
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
⊢ ∀ {a b : A}, degt (a + b) ≤ degt a + degt b
intros a b
no goals
R : Type u_3
A : Type u_2
T : Type u_1
B : Type ?u.19667
ι : Type ?u.19670
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : Semiring R
inst✝⁶ : Add A
inst✝⁵ : Add B
inst✝⁴ : Add T
inst✝³ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
degt : A → T
degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)
f g : AddMonoidAlgebra R A
a b : A
⊢ degt (a + b) ≤ degt a + degt b
exact OrderDual.ofDual_le_ofDual.mp degtm