no goals
ι✝ : Type ?u.809418
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝¹ : CommMonoid β
ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
s t : Finset ι
f : ι → M
h : s ⊆ t
⊢ s.val ≤ t.val
simpa