L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ (∀ (M : ModelType ↑p) (φ : BoundedFormula (L[[α]]) Empty 0), φ ∈ t → BoundedFormula.Realize φ default default) ↔
    ∀ (x : Sentence (L[[α]])), x ∈ ↑t → ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default
L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (Finset.toList t) ∈ p ↔ ↑t ⊆ ↑p
simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff,
  Sentence.Realize, Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]
no goals
L : Language
T : Theory L
α : Type w
p : CompleteType T α
t : Finset (Sentence (L[[α]]))
⊢ (∀ (M : ModelType ↑p) (φ : BoundedFormula (L[[α]]) Empty 0), φ ∈ t → BoundedFormula.Realize φ default default) ↔
    ∀ (x : Sentence (L[[α]])), x ∈ ↑t → ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default
exact ⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩