awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
hpq : p ≠ q
⊢ ∃ (x : L[[α]].Sentence), x ∉ p ↔ x ∈ q

Tactic:
simp only [ne_eq, SetLike.ext_iff, not_forall, not_iff] at hpq

Premises used: SetLike.ext_iff, ne_eq, not_iff, Classical.not_forall
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
hpq : ∃ (x : L[[α]].Sentence), x ∉ p ↔ x ∈ q
obtain : ∀ (φ : L[[α]].Sentence) (hφ : φ ∉ p ↔ φ ∈ q), ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
obtain ⟨φ, hφ⟩ := hpq
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩

Premises used: FirstOrder.Language.Theory.typesWith, And.intro, Exists.intro, CompleteType.isClopen_typesWith
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
inl : q ∈ (T.typesWith φ)ᶜ
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
inl : q ∉ T.typesWith φ
inl₁ : φ ∉ q
inl₂ : ¬φ ∉ p
inl₃ inl₄ inl₅ inl₆ : φ ∈ p
⊢ q ∈ (T.typesWith φ)ᶜ

Tactic:
rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]

Premises used: Classical.not_not, Set.mem_compl_iff, FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩

Premises used: FirstOrder.Language.Theory.typesWith, FirstOrder.Language.BoundedFormula.not, And.intro, Exists.intro, CompleteType.isClopen_typesWith
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
inr : q ∈ (T.typesWith ∼φ)ᶜ
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : Formula.not φ ∈ p
inr : q ∉ T.typesWith ∼φ
inr₁ : ∼φ ∉ q
inr₂ : ¬φ ∉ q
inr₃ : ¬¬φ ∉ p
inr₄ : φ ∉ p
inr₅ inr₆ inr₇ inr₈ : Formula.not φ ∈ p
⊢ q ∈ (T.typesWith ∼φ)ᶜ

Tactic:
rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]

Premises used: Classical.not_not, FirstOrder.Language.Theory.CompleteType.not_mem_iff, Set.mem_compl_iff, FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
⊢ φ ∈ p ∨ Formula.not φ ∈ p

Tactic:
cases mem_or_not_mem p φ with
  | inl h =>
    refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]
  | inr h =>
    refine ⟨T.typesWith ∼φ, isClopen_typesWith _, h, ?_⟩
    rwa [mem_compl_iff, mem_typesWith_iff, not_mem_iff, ← hφ, not_not, ← not_mem_iff]

Premises used: FirstOrder.Language.Theory.CompleteType.mem_or_not_mem, Classical.not_not, FirstOrder.Language.Theory.CompleteType.not_mem_iff, Set.mem_compl_iff, FirstOrder.Language.Theory.CompleteType.mem_typesWith_iff
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
isCompact_univ : IsCompact (X := T.CompleteType α) univ
⊢ CompactSpace (T.CompleteType α)

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
isCompact_univ :
  ∀ (f : Ultrafilter (T.CompleteType α)),
    (↑f : Filter (T.CompleteType α)) ≤ Filter.principal univ →
      ∃ (x : T.CompleteType α),
        Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑f : Filter (T.CompleteType α)) ≤ nhds x
⊢ IsCompact (X := T.CompleteType α) univ

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Premises used: isCompact_iff_ultrafilter_le_nhds
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ ∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑F : Filter (T.CompleteType α)) ≤ nhds x

Tactic:
⟨⟨{φ | T.typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩

Premises used: FirstOrder.Language.Theory.typesWith, setOf, Membership.mem, Exists.intro, FirstOrder.Language.Theory.CompleteType.mk
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ : (L.lhomWithConstants α).onTheory T ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
isCompact_univ₁ : IsMaximal (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
isCompact_univ₂ :
  Membership.mem (γ := Set (T.CompleteType α)) univ
      (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯) ∧
    (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)
⊢ ∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) univ x ∧ (↑F : Filter (T.CompleteType α)) ≤ nhds x

Tactic:
refine ⟨⟨{φ | T.typesWith φ ∈ F}, ?_, ?_⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
x : φ ∈ (L.lhomWithConstants α).onTheory T
⊢ Membership.mem (γ := Set L[[α]].Sentence) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ

Tactic:
F.mem_of_superset Filter.univ_mem (fun p _ ↦ p.subset x)

Premises used: Set.Mem, setOf, Filter.univ_mem, FirstOrder.Language.Theory.CompleteType.subset, Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
x : φ ∈ (L.lhomWithConstants α).onTheory T
⊢ Membership.mem (γ := Set L[[α]].Sentence) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ

Tactic:
exact F.mem_of_superset Filter.univ_mem (fun p _ ↦ p.subset x)

Premises used: Filter.univ_mem, FirstOrder.Language.Theory.CompleteType.subset, Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ :
  IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ∧
    ∀ (φ : L[[α]].Sentence),
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
        Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
⊢ IsMaximal (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}

Tactic:
rw [Theory.IsMaximal, Theory.isSatisfiable_iff_isFinitelySatisfiable]

Premises used: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, FirstOrder.Language.Theory.IsMaximal
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ∧
    ∀ (φ : L[[α]].Sentence),
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
        Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ : IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
isCompact_univ₁ :
  ∀ (φ : L[[α]].Sentence),
    Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)
⊢ IsFinitelySatisfiable (L := L[[α]]) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ∧
    ∀ (φ : L[[α]].Sentence),
      Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
        Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
φ : L[[α]].Sentence
hφ : φ ∈ x
⊢ T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))

Tactic:
hx hφ

Premises used: Set.Mem, setOf
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
φ : L[[α]].Sentence
hφ : φ ∈ x
⊢ T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))

Tactic:
exact hx hφ
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
⊢ ∀ φ ∈ x, T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))

Tactic:
have : ∀ φ ∈ x, T.typesWith φ ∈ F.toFilter := by intro φ hφ; exact hx hφ
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
this : ∀ φ ∈ x, T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))
⊢ ⋂ i ∈ x, T.typesWith i ∈ (↑F : Filter (T.CompleteType α))

Tactic:
rw [← Filter.biInter_finset_mem x] at this

Premises used: Filter.biInter_finset_mem
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T.typesWith φ ∈ F}
this : ⋂ i ∈ x, T.typesWith i ∈ (↑F : Filter (T.CompleteType α))
isCompact_univ :
  ∀ (T_1 : T.CompleteType α) (T_inter : Membership.mem (γ := Set (T.CompleteType α)) (⋂ i ∈ x, T.typesWith i) T_1),
    IsSatisfiable (↑x : Set L[[α]].Sentence)
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)

Tactic:
obtain ⟨T, T_inter⟩ := F.neBot.nonempty_of_mem this

Premises used: Ultrafilter.neBot, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T_1 : L.Theory
α : Type u_1
F : Ultrafilter (T_1.CompleteType α)
h : (↑F : Filter (T_1.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T_1.typesWith φ ∈ F}
this : ⋂ i ∈ x, T_1.typesWith i ∈ (↑F : Filter (T_1.CompleteType α))
T : T_1.CompleteType α
T_inter : Membership.mem (γ := Set (T_1.CompleteType α)) (⋂ i ∈ x, T_1.typesWith i) T
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (T_inter : ∀ (i : L[[α]].Sentence) (j : i ∈ x), T ∈ T_1.typesWith i),
    (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)
⊢ (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)

Tactic:
rwa [Set.mem_iInter₂] at T_inter

Premises used: Set.mem_iInter₂
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T_1 : L.Theory
α : Type u_1
F : Ultrafilter (T_1.CompleteType α)
h : (↑F : Filter (T_1.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T_1.typesWith φ ∈ F}
this : ⋂ i ∈ x, T_1.typesWith i ∈ (↑F : Filter (T_1.CompleteType α))
T : T_1.CompleteType α
T_inter : Membership.mem (γ := Set (T_1.CompleteType α)) (⋂ i ∈ x, T_1.typesWith i) T
⊢ (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)

Tactic:
have subset : (x : Set _) ⊆ T.toTheory := by rwa [Set.mem_iInter₂] at T_inter
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T_1 : L.Theory
α : Type u_1
F : Ultrafilter (T_1.CompleteType α)
h : (↑F : Filter (T_1.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T_1.typesWith φ ∈ F}
this : ⋂ i ∈ x, T_1.typesWith i ∈ (↑F : Filter (T_1.CompleteType α))
T : T_1.CompleteType α
T_inter : Membership.mem (γ := Set (T_1.CompleteType α)) (⋂ i ∈ x, T_1.typesWith i) T
subset : (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)

Tactic:
T.isMaximal.1.mono subset

Premises used: And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T_1 : L.Theory
α : Type u_1
F : Ultrafilter (T_1.CompleteType α)
h : (↑F : Filter (T_1.CompleteType α)) ≤ Filter.principal univ
x : Finset L[[α]].Sentence
hx : (↑x : Set L[[α]].Sentence) ⊆ {φ : L[[α]].Sentence | T_1.typesWith φ ∈ F}
this : ⋂ i ∈ x, T_1.typesWith i ∈ (↑F : Filter (T_1.CompleteType α))
T : T_1.CompleteType α
T_inter : Membership.mem (γ := Set (T_1.CompleteType α)) (⋂ i ∈ x, T_1.typesWith i) T
subset : (↑x : Set L[[α]].Sentence) ⊆ (↑T : L[[α]].Theory)
⊢ IsSatisfiable (↑x : Set L[[α]].Sentence)

Tactic:
exact T.isMaximal.1.mono subset

Premises used: And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
isCompact_univ : T.typesWith φ ∈ F ∨ (T.typesWith φ)ᶜ ∈ F
⊢ Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} φ ∨
    Membership.mem (γ := L[[α]].Theory) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} (Formula.not φ)

Tactic:
simp only [mem_setOf_eq, typesWith_not]

Premises used: Set.mem_setOf_eq, FirstOrder.Language.Theory.CompleteType.typesWith_not
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ T.typesWith φ ∈ F ∨ (T.typesWith φ)ᶜ ∈ F

Tactic:
Ultrafilter.mem_or_compl_mem F (T.typesWith φ)

Premises used: Set.Mem, FirstOrder.Language.Theory.typesWith, setOf, Ultrafilter.mem_or_compl_mem
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
⊢ T.typesWith φ ∈ F ∨ (T.typesWith φ)ᶜ ∈ F

Tactic:
exact Ultrafilter.mem_or_compl_mem F (T.typesWith φ)

Premises used: FirstOrder.Language.Theory.typesWith, Ultrafilter.mem_or_compl_mem
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
⊢ Membership.mem (γ := Set (T.CompleteType α)) univ
      (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯) ∧
    (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)

Tactic:
⟨mem_univ _, ?_⟩

Premises used: And.intro, Set.mem_univ
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ :
  (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)
⊢ Membership.mem (γ := Set (T.CompleteType α)) univ
      (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯) ∧
    (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)

Tactic:
refine ⟨mem_univ _, ?_⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ :
  (↑F : Filter (T.CompleteType α)) ≤
    ⨅ (s : Set (T.CompleteType α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (T.CompleteType α)))
          {s : Set (T.CompleteType α) |
            CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ s ∧
              Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) s}
          s),
        Filter.principal s
⊢ (↑F : Filter (T.CompleteType α)) ≤ nhds (CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯)

Tactic:
rw [nhds_generateFrom]

Premises used: TopologicalSpace.nhds_generateFrom
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
isCompact_univ :
  ∀ (i : Set (T.CompleteType α))
    (j :
      Membership.mem (γ := Set (Set (T.CompleteType α)))
        {s : Set (T.CompleteType α) |
          CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ s ∧
            Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) s}
        i),
    (↑F : Filter (T.CompleteType α)) ≤ Filter.principal i
⊢ (↑F : Filter (T.CompleteType α)) ≤
    ⨅ (s : Set (T.CompleteType α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (T.CompleteType α)))
          {s : Set (T.CompleteType α) |
            CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ s ∧
              Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) s}
          s),
        Filter.principal s

Tactic:
apply le_iInf₂

Premises used: le_iInf₂
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
hφ : CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ T.typesWith φ
isCompact_univ : T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))
⊢ (↑F : Filter (T.CompleteType α)) ≤ Filter.principal (T.typesWith φ)

Tactic:
rw [Filter.le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
hφ : CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ T.typesWith φ
⊢ T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))

Tactic:
hφ

Premises used: Set.Mem, FirstOrder.Language.Theory.typesWith, setOf
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
h : (↑F : Filter (T.CompleteType α)) ≤ Filter.principal univ
φ : L[[α]].Sentence
hφ : CompleteType.mk (T := T) {φ : L[[α]].Sentence | T.typesWith φ ∈ F} ⋯ ⋯ ∈ T.typesWith φ
⊢ T.typesWith φ ∈ (↑F : Filter (T.CompleteType α))

Tactic:
exact hφ
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ BaireSpace (T.CompleteType α)

Tactic:
BaireSpace.of_t2Space_locallyCompactSpace

Premises used: BaireSpace.of_t2Space_locallyCompactSpace
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ funMap f x ≈ funMap f y

Tactic:
mem_of_superset (iInter_mem.2 xy) fun a ha => ?_

Premises used: Iff.mpr, Filter.Eventually, Filter.iInter_mem, Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
refine :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a),
    Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ funMap f x a = funMap f y a) x_1} a
⊢ funMap f x ≈ funMap f y

Tactic:
refine mem_of_superset (iInter_mem.2 xy) fun a ha => ?_

Premises used: Iff.mpr, Filter.iInter_mem, Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : Membership.mem (γ := Set α) (⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1}) a
⊢ ∀ (i : Fin n), x i a = y i a

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq] at ha

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
f : L.Functions n
x y : Fin n → (a : α) → M a
xy : x ≈ y
a : α
ha : ∀ (i : Fin n), x i a = y i a
⊢ Membership.mem (γ := Set α) {x_1 : α | (fun (a : α) ↦ funMap f x a = funMap f y a) x_1} a

Tactic:
simp only [Set.mem_setOf_eq, ha]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
rw : RelMap r x ↔ RelMap r y
⊢ RelMap r x = RelMap r y

Tactic:
rw [← iff_eq_eq]

Premises used: iff_eq_eq
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
⊢ RelMap r x ↔ RelMap r y

Tactic:
⟨fun hx => ?_, fun hy => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
refine_1 : ∀ (hx : RelMap r x), RelMap r y
refine_2 : ∀ (hy : RelMap r y), RelMap r x
⊢ RelMap r x ↔ RelMap r y

Tactic:
refine ⟨fun hx => ?_, fun hy => ?_⟩
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
⊢ RelMap r y

Tactic:
mem_of_superset (inter_mem hx (iInter_mem.2 xy)) ?_

Premises used: Iff.mpr, Filter.Eventually, Filter.inter_mem, Filter.iInter_mem, Filter.mem_of_superset
-- Module: Mathlib.ModelTheory.Ultraproducts
Goal:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst : (a : α) → Structure.{u, v, u_2} L (M a)
n : ℕ
r : L.Relations n
x y : Fin n → (a : α) → M a
xy : x ≈ y
hx : RelMap r x
refine_1 :
  Subset.{u_1} (α := Set α)
    ({x_1 : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ x i a) x_1} ∩
      ⋂ (i : Fin n), {x_1 : α | (fun (a : α) ↦ x i a = y i a) x_1})
    {x : α | (fun (a : α) ↦ RelMap.{u, v, u_2} (M := M a) r fun (i : Fin n) ↦ y i a) x}
⊢ RelMap r y

Tactic:
refine mem_of_superset (inter_mem hx (iInter_mem.2 xy)) ?_

Premises used: Iff.mpr, Filter.inter_mem, Filter.iInter_mem, Filter.mem_of_superset