rcases Meaningful.exists_unrealize (𝓜 := 𝓜) with ⟨f, hf⟩
case intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
⊢ Meaningful s
case intro.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
f : F
hf : ¬𝓜 ⊧ f
⊢ Meaningful s