constructor <;> simp_all
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ p ∈ Finset.multimop i n s ↔ p ∈ Set.multimop i n ↑s
no goals