awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p q : T.CompleteType α
h :
  Eq (α := Set L[[α]].Sentence) ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) p)
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) q)
mk :
  ∀ (toTheory : L[[α]].Theory) (subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory)
    (isMaximal' : toTheory.IsMaximal)
    (h :
      Eq (α := Set L[[α]].Sentence)
        ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (CompleteType.mk (T := T) toTheory subset' isMaximal'))
        ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) q)),
    CompleteType.mk (T := T) toTheory subset' isMaximal' = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
q : T.CompleteType α
toTheory : L[[α]].Theory
subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory
isMaximal' : toTheory.IsMaximal
h :
  Eq (α := Set L[[α]].Sentence)
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (CompleteType.mk (T := T) toTheory subset' isMaximal'))
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) q)
mk :
  ∀ (toTheory_1 : L[[α]].Theory) (subset'_1 : (L.lhomWithConstants α).onTheory T ⊆ toTheory_1)
    (isMaximal'_1 : toTheory_1.IsMaximal)
    (h :
      Eq (α := Set L[[α]].Sentence)
        ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (CompleteType.mk (T := T) toTheory subset' isMaximal'))
        ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory))
          (CompleteType.mk (T := T) toTheory_1 subset'_1 isMaximal'_1))),
    CompleteType.mk (T := T) toTheory subset' isMaximal' = CompleteType.mk (T := T) toTheory_1 subset'_1 isMaximal'_1
⊢ CompleteType.mk (T := T) toTheory subset' isMaximal' = q

Tactic:
cases q
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
toTheory : L[[α]].Theory
subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory
isMaximal' : toTheory.IsMaximal
toTheory_1 : L[[α]].Theory
subset'_1 : (L.lhomWithConstants α).onTheory T ⊆ toTheory_1
isMaximal'_1 : toTheory_1.IsMaximal
h :
  Eq (α := Set L[[α]].Sentence)
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (mk (T := T) toTheory subset' isMaximal'))
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (mk (T := T) toTheory_1 subset'_1 isMaximal'_1))
⊢ mk (T := T) toTheory subset' isMaximal' = mk (T := T) toTheory_1 subset'_1 isMaximal'_1

Tactic:
congr
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
⊢ IsMaximal (↑p : Set L[[α]].Sentence)

Tactic:
p.isMaximal'

Premises used: FirstOrder.Language.Theory.CompleteType.isMaximal'
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
⊢ (L.lhomWithConstants α).onTheory T ⊆ (↑p : Set L[[α]].Sentence)

Tactic:
p.subset'

Premises used: FirstOrder.Language.Theory.CompleteType.subset'
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
⊢ φ ∈ p ∨ Formula.not φ ∈ p

Tactic:
p.isMaximal.mem_or_not_mem φ

Premises used: Set.Mem, FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
hT : T.IsSatisfiable
φ : L.Sentence
hφ : φ ∈ T
hφ' : ∼φ ∈ T
⊢ False

Tactic:
have ⟨M⟩ := hT
  (M.is_model.realize_of_mem _ hφ') (M.is_model.realize_of_mem _ hφ)

Premises used: False, FirstOrder.Language.Theory.Model.realize_of_mem, FirstOrder.Language.BoundedFormula.not, _private.0.FirstOrder.Language.Theory.CompleteType.false_of_mem_of_not_mem.match_1
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
⊢ φ ∈ p

Tactic:
(p.mem_or_not_mem φ).resolve_right fun con =>
    ((models_iff_not_satisfiable _).1 h)
      (p.isMaximal.1.mono (union_subset p.subset (singleton_subset_iff.2 con)))

Premises used: Iff.mpr, Set.singleton_subset_iff, FirstOrder.Language.Theory.CompleteType.mem_or_not_mem, Set.union_subset, And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, Iff.mp, Or.resolve_right, FirstOrder.Language.Theory.CompleteType.isMaximal, FirstOrder.Language.Theory.CompleteType.subset, FirstOrder.Language.Theory.models_iff_not_satisfiable
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier : Type (max (max u w) v)
struc : L[[α]].Structure Carrier
h : Model (L := L[[α]]) Carrier {φ, Formula.not φ}
nonempty' : Nonempty Carrier
⊢ Carrier ⊨ φ ∧ Carrier ⊨ Formula.not φ

Tactic:
simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h

Premises used: FirstOrder.Language.Theory.model_iff, forall_eq, forall_eq_or_imp, Set.mem_singleton_iff, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier : Type (max (max u w) v)
struc : L[[α]].Structure Carrier
nonempty' : Nonempty Carrier
h : Carrier ⊨ φ ∧ Carrier ⊨ Formula.not φ
⊢ False

Tactic:
h.2 h.1

Premises used: FirstOrder.Language.BoundedFormula.Realize, And.right, And.left
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier : Type (max (max u w) v)
struc : L[[α]].Structure Carrier
nonempty' : Nonempty Carrier
h : Carrier ⊨ φ ∧ Carrier ⊨ Formula.not φ
⊢ False

Tactic:
exact h.2 h.1

Premises used: And.right, And.left
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}

Tactic:
have h : ¬IsSatisfiable ({φ, φ.not} : L[[α]].Theory) := by
      rintro ⟨@⟨_, _, h, _⟩⟩
      simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
      exact h.2 h.1
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
⊢ False

Tactic:
h (p.isMaximal.1.mono ?_)

Premises used: And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
refine : {φ, Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)
⊢ False

Tactic:
refine h (p.isMaximal.1.mono ?_)

Premises used: And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, FirstOrder.Language.Theory.CompleteType.isMaximal
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
rw : φ ∈ (↑p : Set L[[α]].Sentence) ∧ Formula.not φ ∈ (↑p : Set L[[α]].Sentence)
⊢ {φ, Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)

Tactic:
rw [insert_subset_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
⊢ φ ∈ (↑p : Set L[[α]].Sentence) ∧ Formula.not φ ∈ (↑p : Set L[[α]].Sentence)

Tactic:
⟨ht, hf⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
⊢ φ ∈ (↑p : Set L[[α]].Sentence) ∧ Formula.not φ ∈ (↑p : Set L[[α]].Sentence)

Tactic:
exact ⟨ht, hf⟩
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p}ᶜ {p : T.CompleteType α | Formula.not φ ∈ p}

Tactic:
ext fun _ => (not_mem_iff _ _).symm

Premises used: Set.ext, FirstOrder.Language.Theory.CompleteType.not_mem_iff, Iff.symm
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
rw :
  ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔
    ∃ (x : T.CompleteType α),
      Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} ∅ ↔
    ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]

Premises used: iff_not_comm, Classical.not_not, Set.not_nonempty_iff_eq_empty, Set.Nonempty
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔
    ∃ (x : T.CompleteType α),
      Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x

Tactic:
⟨fun h =>
      ⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
          completeTheory.isMaximal L[[α]] h.some⟩,
        (((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
      ?_⟩

Premises used: FirstOrder.Language.completeTheory, Set.subset_union_right, FirstOrder.Language.completeTheory.isMaximal, HasSubset.Subset.trans, FirstOrder.Language.withConstants, Nonempty.some, Set.subset_union_left, Iff.intro, Exists.intro, FirstOrder.Language.Theory.ModelType.Carrier, FirstOrder.Language.Theory.completeTheory.subset, FirstOrder.Language.Theory.CompleteType.mk
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  (∃ (x : T.CompleteType α),
      Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x) →
    ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔
    ∃ (x : T.CompleteType α),
      Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x

Tactic:
refine
    ⟨fun h =>
      ⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
          completeTheory.isMaximal L[[α]] h.some⟩,
        (((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
      ?_⟩
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
p : T.CompleteType α
hp : Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} p
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
p.isMaximal.1.mono (union_subset p.subset hp)

Premises used: Set.union_subset, And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, FirstOrder.Language.Theory.CompleteType.isMaximal, FirstOrder.Language.Theory.CompleteType.subset
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
p : T.CompleteType α
hp : Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} p
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
exact p.isMaximal.1.mono (union_subset p.subset hp)

Premises used: Set.union_subset, And.left, FirstOrder.Language.Theory.IsSatisfiable.mono, FirstOrder.Language.Theory.CompleteType.isMaximal, FirstOrder.Language.Theory.CompleteType.subset
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
rw :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | Formula.not φ ∈ p} ∅ ↔
    Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | {Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)} ∅
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]

Premises used: FirstOrder.Language.Theory.CompleteType.compl_setOf_mem, Set.compl_empty_iff, FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff, FirstOrder.Language.Theory.models_iff_not_satisfiable
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | Formula.not φ ∈ p} ∅ ↔
    Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | {Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)} ∅

Tactic:
simp
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  ∀ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x ↔
      Membership.mem (γ := Set (T.CompleteType α))
        (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S)) x
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))

Tactic:
ext
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
x : T.CompleteType α
⊢ Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x ↔
    Membership.mem (γ := Set (T.CompleteType α))
      (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S)) x

Tactic:
simp [subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))

Tactic:
have h : { p : T.CompleteType α | S ⊆ ↑p } = ⋂₀ ((fun φ => { p | φ ∈ p }) '' S) := by
    ext
    simp [subset_def]
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
simp_rw :
  (∀ (s : Set (T.CompleteType α)),
      Membership.mem (γ := Set (Set (T.CompleteType α)))
          ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
        s = Set.univ) ↔
    ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} Set.univ ↔
    ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]

Premises used: Set.sInter_eq_univ, FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
⊢ (∀ (s : Set (T.CompleteType α)),
      Membership.mem (γ := Set (Set (T.CompleteType α)))
          ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
        s = Set.univ) ↔
    ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ

Tactic:
⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, ?_⟩

Premises used: setOf, Membership.mem, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
refine :
  (∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ) →
    ∀ (s : Set (T.CompleteType α)),
      Membership.mem (γ := Set (Set (T.CompleteType α)))
          ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
        s = Set.univ
⊢ (∀ (s : Set (T.CompleteType α)),
      Membership.mem (γ := Set (Set (T.CompleteType α)))
          ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
        s = Set.univ) ↔
    ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ

Tactic:
refine ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h_1 :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
h : ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ
φ : L[[α]].Sentence
h1 : φ ∈ S
⊢ Eq (α := Set (T.CompleteType α))
    ((fun (φ : L[[α]].Sentence) ↦ ({p : T.CompleteType α | φ ∈ p} : Set (T.CompleteType α))) φ) Set.univ

Tactic:
h _ h1
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h_1 :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
h : ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ
φ : L[[α]].Sentence
h1 : φ ∈ S
⊢ Eq (α := Set (T.CompleteType α))
    ((fun (φ : L[[α]].Sentence) ↦ ({p : T.CompleteType α | φ ∈ p} : Set (T.CompleteType α))) φ) Set.univ

Tactic:
exact h _ h1
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
rw : Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable
⊢ Nonempty (T.CompleteType α) ↔ T.IsSatisfiable

Tactic:
rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]

Premises used: FirstOrder.Language.Theory.isSatisfiable_onTheory_iff, FirstOrder.Language.lhomWithConstants_injective
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
rw :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | ∅ ⊆ (↑p : Set L[[α]].Sentence)} ∅ ↔
    Eq (α := Set (T.CompleteType α)) Set.univ ∅
⊢ Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable

Tactic:
rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne, not_iff_comm,
    ← union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]

Premises used: Set.union_empty, Ne, Set.nonempty_iff_univ_nonempty, Set.nonempty_iff_ne_empty, FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff, FirstOrder.Language.lhomWithConstants, not_iff_comm, FirstOrder.Language.LHom.onTheory
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | ∅ ⊆ (↑p : Set L[[α]].Sentence)} ∅ ↔
    Eq (α := Set (T.CompleteType α)) Set.univ ∅

Tactic:
simp
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
⊢ Nonempty (CompleteType.{u, v, w} (L := L) ∅ α)

Tactic:
nonempty_iff.2 (isSatisfiable_empty L)

Premises used: Iff.mpr, FirstOrder.Language.Theory.CompleteType.nonempty_iff, FirstOrder.Language.Theory.isSatisfiable_empty
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
h :
  ∀ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) (⋂ (i : ι), {p : T.CompleteType α | S i ⊆ (↑p : Set L[[α]].Sentence)})
        x ↔
      Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | ⋃ (i : ι), S i ⊆ (↑p : Set L[[α]].Sentence)}
        x
⊢ Eq (α := Set (T.CompleteType α)) (⋂ (i : ι), {p : T.CompleteType α | S i ⊆ (↑p : Set L[[α]].Sentence)})
    {p : T.CompleteType α | ⋃ (i : ι), S i ⊆ (↑p : Set L[[α]].Sentence)}

Tactic:
ext
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
x : T.CompleteType α
⊢ Membership.mem (γ := Set (T.CompleteType α)) (⋂ (i : ι), {p : T.CompleteType α | S i ⊆ (↑p : Set L[[α]].Sentence)})
      x ↔
    Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | ⋃ (i : ι), S i ⊆ (↑p : Set L[[α]].Sentence)} x

Tactic:
simp only [mem_iInter, mem_setOf_eq, iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff, Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
simp_rw :
  (∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
      ∀ φ ∈ t, φ.Realize (M := (↑M : Type (max (max u w) v))) default default) ↔
    ∀ x ∈ (↑t : Set L[[α]].Sentence),
      ∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
        BoundedFormula.Realize (M := (↑M : Type (max (max u w) v))) x default default
⊢ List.foldr (fun (x1 x2 : L[[α]].Sentence) ↦ x1 ⊓ x2) ⊤ t.toList ∈ p ↔
    (↑t : Set L[[α]].Sentence) ⊆ (↑p : Set L[[α]].Sentence)

Tactic:
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]

Premises used: FirstOrder.Language.Sentence.Realize, Set.subset_def, FirstOrder.Language.Theory.models_sentence_iff, FirstOrder.Language.BoundedFormula.realize_foldr_inf, SetLike.mem_coe, FirstOrder.Language.Theory.IsMaximal.mem_iff_models, Finset.mem_toList, FirstOrder.Language.Theory.CompleteType.isMaximal, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ (∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
      ∀ φ ∈ t, φ.Realize (M := (↑M : Type (max (max u w) v))) default default) ↔
    ∀ x ∈ (↑t : Set L[[α]].Sentence),
      ∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
        BoundedFormula.Realize (M := (↑M : Type (max (max u w) v))) x default default

Tactic:
⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ (∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
      ∀ φ ∈ t, φ.Realize (M := (↑M : Type (max (max u w) v))) default default) ↔
    ∀ x ∈ (↑t : Set L[[α]].Sentence),
      ∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
        BoundedFormula.Realize (M := (↑M : Type (max (max u w) v))) x default default

Tactic:
exact ⟨fun h φ hφ M => h _ _ hφ, fun h M φ hφ => h _ hφ _⟩
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
M : Type w'
inst : L.Structure M
inst_1 : Nonempty M
inst_2 : M ⊨ T
v : α → M
φ : L[[α]].Sentence
⊢ φ ∈ T.typeOf v ↔
    Formula.Realize.{u, v, w', w} (L := L)
      ((_root_.Equiv.symm Formula.equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) v

Tactic:
letI : (constantsOn α).Structure M := constantsOn.structure v
  mem_completeTheory.trans (Formula.realize_equivSentence_symm _ _ _).symm

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.completeTheory, Set.Mem, setOf, FirstOrder.Language.mem_completeTheory, Iff.trans, Iff.symm, FirstOrder.Language.Formula.Realize, FirstOrder.Language.Formula.realize_equivSentence_symm
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
M : Type w'
inst : L.Structure M
inst_1 : Nonempty M
inst_2 : M ⊨ T
v : α → M
φ : L.Formula α
⊢ Membership.mem (α := L[[α]].Sentence) (T.typeOf v)
      ((Formula.equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ : L[[α]].Sentence) ↔
    φ.Realize v

Tactic:
simp
-- Module: Mathlib.ModelTheory.Types
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
p : T.CompleteType α
⊢ p ∈ T.typesWith φ ↔ φ ∈ p

Tactic:
rfl