exact (H ⟨t, ht⟩).RealizeSet hσ
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
σ : Sentence L
hσ : σ ∈ t
⊢ A ⟨t, ⋯⟩ ⊧ₘ σ
no goals