. intro p hp;
  obtain ⟨q, hq₁, hq₂⟩ := hp;
  simp_all [Set.premultimop];
case a
ι : 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
⊢ Set.multimop i n (Set.premultimop i n s) ⊆ s

case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)
case a
ι : 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
⊢ s ⊆ Set.multimop i n (Set.premultimop i n s)