R : Type u_3
A : Type u_2
T : Type ?u.14182
B : Type u_1
ι : Type ?u.14188
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
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ Finset.sup (Finset.biUnion f.support fun a₁ => Finset.biUnion g.support fun a₂ => {a₁ + a₂}) degb ≤
    Finset.sup f.support degb + Finset.sup g.support degb
R : Type u_3
A : Type u_2
T : Type ?u.14182
B : Type u_1
ι : Type ?u.14188
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
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ Finset.sup (f * g).support degb ≤ Finset.sup f.support degb + Finset.sup g.support degb
refine' (Finset.sup_mono <| support_mul _ _).trans _
R : Type u_3
A : Type u_2
T : Type ?u.14182
B : Type u_1
ι : Type ?u.14188
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
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ (Finset.sup f.support fun x => Finset.sup g.support fun x_1 => degb (x + x_1)) ≤
    Finset.sup f.support degb + Finset.sup g.support degb
R : Type u_3
A : Type u_2
T : Type ?u.14182
B : Type u_1
ι : Type ?u.14188
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
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ Finset.sup (Finset.biUnion f.support fun a₁ => Finset.biUnion g.support fun a₂ => {a₁ + a₂}) degb ≤
    Finset.sup f.support degb + Finset.sup g.support degb
simp_rw [Finset.sup_biUnion, Finset.sup_singleton]
no goals
R : Type u_3
A : Type u_2
T : Type ?u.14182
B : Type u_1
ι : Type ?u.14188
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
degb : A → B
degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b
f g : AddMonoidAlgebra R A
⊢ (Finset.sup f.support fun x => Finset.sup g.support fun x_1 => degb (x + x_1)) ≤
    Finset.sup f.support degb + Finset.sup g.support degb
refine' Finset.sup_le fun fd fds => Finset.sup_le fun gd gds => degbm.trans <| add_le_add _ _ <;>
  exact Finset.le_sup ‹_›