R : Type u_4
A : Type u_2
T : Type u_1
B : Type ?u.101250
ι : Type u_3
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
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✝² : AddCommMonoid T
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
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → AddMonoidAlgebra R A
⊢ ∑ i in s, Finset.inf (f i).support degt =
    Multiset.sum (Multiset.map ((fun f => Finset.inf f.support degt) ∘ fun i => f i) s.val)
R : Type u_4
A : Type u_2
T : Type u_1
B : Type ?u.101250
ι : Type u_3
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
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✝² : AddCommMonoid T
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
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → AddMonoidAlgebra R A
⊢ ∑ i in s, Finset.inf (f i).support degt =
    Multiset.sum (Multiset.map (fun f => Finset.inf f.support degt) (Multiset.map (fun i => f i) s.val))
rw [Multiset.map_map]
no goals
R : Type u_4
A : Type u_2
T : Type u_1
B : Type ?u.101250
ι : Type u_3
inst✝¹¹ : SemilatticeSup B
inst✝¹⁰ : OrderBot B
inst✝⁹ : SemilatticeInf T
inst✝⁸ : OrderTop T
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : AddCommMonoid B
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✝² : AddCommMonoid T
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
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → AddMonoidAlgebra R A
⊢ ∑ i in s, Finset.inf (f i).support degt =
    Multiset.sum (Multiset.map ((fun f => Finset.inf f.support degt) ∘ fun i => f i) s.val)
rfl