Theorem: Finset.premultimop_coe (Logic/Modal/LogicSymbol.lean)

State before:
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Finset F
⊢ ↑(Finset.premultimop i n s) = Set.premultimop i n ↑s
Tactic:
apply Finset.coe_preimage
State after:
no goals