rw[compactness_aux]
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u