simp_all [Set.premultimop]
case a.intro.intro
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p✝ q✝ : F
s t : Set F
h : s ⊆ Set.multimop i n t
p q : F
hq₁ : q ∈ Set.premultimop i n s
hq₂ : (mop i)^[n] q = p
⊢ p ∈ s
no goals