awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
h : ∀ {n : ℕ}, Eq (α := L.BoundedFormula α n) ((LHom.id L).onBoundedFormula falsum) (id falsum)
h₁ : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)), (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
h₂ :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (LHom.id L).onBoundedFormula (rel R ts) = id (rel R ts)
h₃ :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n) (ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁)
    (ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂), (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
h₄ :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1)) (ih3 : (LHom.id L).onBoundedFormula f = id f),
    (LHom.id L).onBoundedFormula f.all = id f.all
⊢ (LHom.id L).onBoundedFormula f = id f

Tactic:
induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.Term.bdEqual, id, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, FirstOrder.Language.LHom.onBoundedFormula, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.LHom.id_onTerm, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
h : ∀ (f : L.BoundedFormula α n), (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
⊢ Eq (α := L.BoundedFormula α n → L''.BoundedFormula α n) (φ.comp ψ).onBoundedFormula
    (φ.onBoundedFormula ∘ ψ.onBoundedFormula)

Tactic:
ext f
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 : ℕ
⊢ Eq (α := L''.BoundedFormula α n_1) ((φ.comp ψ).onBoundedFormula falsum)
    ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ (φ.comp ψ).onBoundedFormula (equal t₁ t₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁ t₂)

Tactic:
simp [Term.bdEqual]

Premises used: FirstOrder.Language.Term.bdEqual
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
h :
  (φ.onRelation (ψ.onRelation R)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts) =
    φ.onBoundedFormula ((ψ.onRelation R).boundedFormula (ψ.onTerm ∘ ts))
⊢ (φ.comp ψ).onBoundedFormula (rel R ts) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R ts)

Tactic:
simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]

Premises used: FirstOrder.Language.LHom.comp_onTerm, FirstOrder.Language.LHom.comp_onRelation, Function.comp_apply, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ (φ.onRelation (ψ.onRelation R)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts) =
    φ.onBoundedFormula ((ψ.onRelation R).boundedFormula (ψ.onTerm ∘ ts))

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (φ.comp ψ).onBoundedFormula f₁ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₁
ih2 : (φ.comp ψ).onBoundedFormula f₂ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₂
⊢ (φ.comp ψ).onBoundedFormula (f₁.imp f₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (f₁.imp f₂)

Tactic:
simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]

Premises used: Function.comp_apply, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
⊢ (φ.comp ψ).onBoundedFormula f.all = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f.all

Tactic:
simp only [ih3, onBoundedFormula, Function.comp_apply]

Premises used: Function.comp_apply, FirstOrder.Language.LHom.onBoundedFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
h :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula α n) ((φ.comp ψ).onBoundedFormula falsum)
      ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)
h₁ :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (equal t₁ t₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁ t₂)
h₂ :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (rel R ts) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R ts)
h₃ :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : (φ.comp ψ).onBoundedFormula f₁ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₁)
    (ih2 : (φ.comp ψ).onBoundedFormula f₂ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₂),
    (φ.comp ψ).onBoundedFormula (f₁.imp f₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (f₁.imp f₂)
h₄ :
  ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
    (ih3 : (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f),
    (φ.comp ψ).onBoundedFormula f.all = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f.all
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f

Tactic:
induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]

Premises used: FirstOrder.Language.BoundedFormula.imp, FirstOrder.Language.Term.bdEqual, FirstOrder.Language.LHom.comp_onTerm, FirstOrder.Language.LHom.comp_onRelation, FirstOrder.Language.BoundedFormula.equal, FirstOrder.Language.BoundedFormula.falsum, Function.comp_apply, FirstOrder.Language.LHom.onBoundedFormula, FirstOrder.Language.BoundedFormula.all, FirstOrder.Language.BoundedFormula.rel
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
g : L →ᴸ L'
T : L.Theory
φ : L'.Sentence
⊢ φ ∈ g.onTheory T ↔ ∃ φ₀ ∈ T, g.onSentence φ₀ = φ

Tactic:
Set.mem_image _ _ _

Premises used: Set.Mem, Set.mem_image, FirstOrder.Language.LHom.onTheory
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.onBoundedFormula ∘ φ.toLHom.onBoundedFormula) id
rw₁ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.comp φ.toLHom).onBoundedFormula id
rw₂ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (LHom.id L).onBoundedFormula id
rw₃ rw₄ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) id id
⊢ Function.LeftInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv,
      LHom.id_onBoundedFormula]

Premises used: FirstOrder.Language.LHom.comp_onBoundedFormula, Function.leftInverse_iff_comp, FirstOrder.Language.LHom.id_onBoundedFormula, FirstOrder.Language.LEquiv.left_inv
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.onBoundedFormula ∘ φ.invLHom.onBoundedFormula) id
rw₁ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.comp φ.invLHom).onBoundedFormula id
rw₂ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (LHom.id L').onBoundedFormula id
rw₃ rw₄ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) id id
⊢ Function.RightInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula

Tactic:
rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv,
      LHom.id_onBoundedFormula]

Premises used: FirstOrder.Language.LEquiv.right_inv, Function.rightInverse_iff_comp, FirstOrder.Language.LHom.comp_onBoundedFormula, FirstOrder.Language.LHom.id_onBoundedFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
φ : L ≃ᴸ L'
⊢ Eq (α := L'.BoundedFormula α n ≃ L.BoundedFormula α n) (_root_.Equiv.symm φ.onBoundedFormula) φ.symm.onBoundedFormula

Tactic:
rfl

Premises used: FirstOrder.Language.LEquiv.onBoundedFormula, Equiv.symm, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
φ : L ≃ᴸ L'
⊢ Eq (α := (a : L.Formula α) → L'.Formula α) (⇑φ.onFormula : (a : L.Formula α) → L'.Formula α) φ.toLHom.onFormula

Tactic:
rfl

Premises used: rfl, FirstOrder.Language.LHom.onFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
L' : Language
α : Type u'
φ : L ≃ᴸ L'
⊢ Eq (α := L'.Formula α ≃ L.Formula α) (_root_.Equiv.symm φ.onFormula) φ.symm.onFormula

Tactic:
rfl

Premises used: FirstOrder.Language.LEquiv.onBoundedFormula, Equiv.symm, rfl, FirstOrder.Language.LEquiv.onFormula
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
φ : L.Formula α
⊢ Eq (α := L[[α]].Sentence) ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ.not : L[[α]].Sentence)
    (Formula.not ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ) : L[[α]].Formula Empty)

Tactic:
rfl

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.not, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
φ ψ : L.Formula α
⊢ Eq (α := L[[α]].Sentence) ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) (φ ⊓ ψ) : L[[α]].Sentence)
    ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ ⊓ (equivSentence : (a : L.Formula α) → L[[α]].Sentence) ψ :
      L[[α]].Sentence)

Tactic:
rfl

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.not, rfl
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s t : Set α
h : s ⊆ t
⊢ Subset (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (t ×ˢ t ∩ (diagonal α)ᶜ))

Tactic:
gcongr
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
⊢ Monotone (α := Set α) L.distinctConstantsTheory

Tactic:
fun _s _t st =>
  L.distinctConstantsTheory_mono st

Premises used: Monotone, FirstOrder.Language.distinctConstantsTheory_mono
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
⊢ Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) L.distinctConstantsTheory

Tactic:
Monotone.directed_le monotone_distinctConstantsTheory

Premises used: FirstOrder.Language.monotone_distinctConstantsTheory, Monotone.directed_le
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
rw :
  Eq (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
      ((⋃ (i : Finset (↑s : Type u')),
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)) ∩
        (diagonal α)ᶜ))
⊢ Eq (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    (⋃ (t : Finset (↑s : Type u')),
      (fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
        ((↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α) ∩
          (diagonal α)ᶜ))

Tactic:
rw [← image_iUnion, ← iUnion_inter]

Premises used: Set.iUnion_inter, Set.image_iUnion
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
⊢ Eq (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
      ((⋃ (i : Finset (↑s : Type u')),
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)) ∩
        (diagonal α)ᶜ))

Tactic:
congr(_ '' ($(?_) ∩ _))

Premises used: FirstOrder.Language.Constants.term, congrArg, Compl.compl, id, FirstOrder.Language.Term.equal, Prod.fst, Inter.inter, Set.diagonal, FirstOrder.Language.con, FirstOrder.Language.Formula.not, Set.image, Prod.snd
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
refine :
  s ×ˢ s =
    ⋃ (i : Finset (↑s : Type u')),
      (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
⊢ Eq (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
      ((⋃ (i : Finset (↑s : Type u')),
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)) ∩
        (diagonal α)ᶜ))

Tactic:
refine congr(_ '' ($(?_) ∩ _))
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
h :
  ∀ (i j : α),
    (i, j) ∈ s ×ˢ s ↔
      Membership.mem (γ := Set (α × α))
        (⋃ (i : Finset (↑s : Type u')),
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
        (i, j)
⊢ s ×ˢ s =
    ⋃ (i : Finset (↑s : Type u')),
      (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)

Tactic:
ext ⟨i, j⟩
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
h :
  i ∈ s ∧ j ∈ s ↔
    ∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ i_1
⊢ (i, j) ∈ s ×ˢ s ↔
    Membership.mem (γ := Set (α × α))
      (⋃ (i : Finset (↑s : Type u')),
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
      (i, j)

Tactic:
simp only [prodMk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion,
      mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right]

Premises used: Set.mem_iUnion, Set.mem_image, Function.Embedding.coe_subtype, Subtype.exists, exists_eq_right, Set.prodMk_mem_set_prod_eq, exists_and_right, Finset.coe_map, Finset.mem_coe
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ i_1

Tactic:
⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩

Premises used: Insert.insert, And.right, And.left, And.intro, Iff.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
h :
  ∀ (h : i ∈ s ∧ j ∈ s),
    Membership.mem (γ := Finset { x : α // x ∈ s })
      {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i ⋯, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j ⋯}
      (Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯)
h₁ :
  ∀ (h : i ∈ s ∧ j ∈ s),
    Membership.mem (γ := Finset { x : α // x ∈ s })
      {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i ⋯, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j ⋯}
      (Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯)
h₂ :
  (∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ i_1) →
    i ∈ s ∧ j ∈ s
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ i_1

Tactic:
refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ Membership.mem (γ := Finset { x : α // x ∈ s })
    {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i ⋯, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j ⋯}
    (Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ Membership.mem (γ := Finset { x : α // x ∈ s })
    {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i ⋯, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j ⋯}
    (Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
t : Finset (↑s : Type u')
is : i ∈ s
h : Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ t
js : j ∈ s
h_1 : Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ t
⊢ i ∈ s ∧ j ∈ s

Tactic:
⟨is, js⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Syntax
Goal:
L : Language
α : Type u'
s : Set α
i j : α
t : Finset (↑s : Type u')
is : i ∈ s
h : Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ t
js : j ∈ s
h_1 : Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ t
⊢ i ∈ s ∧ j ∈ s

Tactic:
exact ⟨is, js⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
this :
  ∀ (φ : L[[α]].Sentence) (ht₁ : T.typesWith φ = t₁) (t₂ : Set (T.CompleteType α)),
    Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₂ →
      ∀ x ∈ t₁ ∩ t₂,
        ∃ (t₃ : Set (T.CompleteType α)),
          Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₁ →
    ∀ (t₂ : Set (T.CompleteType α)),
      Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₂ →
        ∀ x ∈ t₁ ∩ t₂,
          ∃ (t₃ : Set (T.CompleteType α)),
            Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
⟨φ, ht₁⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
this :
  ∀ (ψ : L[[α]].Sentence) (ht₂ : T.typesWith ψ = t₂),
    ∀ x ∈ t₁ ∩ t₂,
      ∃ (t₃ : Set (T.CompleteType α)),
        Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₂ →
    ∀ x ∈ t₁ ∩ t₂,
      ∃ (t₃ : Set (T.CompleteType α)),
        Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
⟨ψ, ht₂⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ (t₃ : Set (T.CompleteType α)),
    Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
⟨T.typesWith (φ ⊓ ψ), ⟨φ ⊓ ψ, rfl⟩, ?_⟩

Premises used: FirstOrder.Language.Theory.typesWith, And.intro, Exists.intro, Min.min, rfl
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
refine : x ∈ T.typesWith (φ ⊓ ψ) ∧ T.typesWith (φ ⊓ ψ) ⊆ t₁ ∩ t₂
⊢ ∃ (t₃ : Set (T.CompleteType α)),
    Membership.mem (γ := Set (Set (T.CompleteType α))) (range T.typesWith) t₃ ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
refine ⟨T.typesWith (φ ⊓ ψ), ⟨φ ⊓ ψ, rfl⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
rw : x ∈ t₁ ∩ t₂ ∧ t₁ ∩ t₂ ⊆ t₁ ∩ t₂
⊢ x ∈ T.typesWith (φ ⊓ ψ) ∧ T.typesWith (φ ⊓ ψ) ⊆ t₁ ∩ t₂

Tactic:
rw [typesWith_inf, ht₁, ht₂]

Premises used: FirstOrder.Language.Theory.CompleteType.typesWith_inf
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
⊢ x ∈ t₁ ∩ t₂ ∧ t₁ ∩ t₂ ⊆ t₁ ∩ t₂

Tactic:
⟨hx, fun _ ↦ id⟩

Premises used: id, And.intro
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
⊢ x ∈ t₁ ∩ t₂ ∧ t₁ ∩ t₂ ⊆ t₁ ∩ t₂

Tactic:
exact ⟨hx, fun _ ↦ id⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
rw : Subset (α := Set (T.CompleteType α)) univ (⋃₀ range T.typesWith)
⊢ Eq (α := Set (T.CompleteType α)) (⋃₀ range T.typesWith) univ

Tactic:
rw [← Set.univ_subset_iff]

Premises used: Set.univ_subset_iff
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ Subset (α := Set (T.CompleteType α)) univ (⋃₀ range T.typesWith)

Tactic:
Set.subset_sUnion_of_mem ⟨_, typesWith_top⟩

Premises used: Exists.intro, Set.subset_sUnion_of_mem, FirstOrder.Language.Theory.CompleteType.typesWith_top
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ Subset (α := Set (T.CompleteType α)) univ (⋃₀ range T.typesWith)

Tactic:
exact Set.subset_sUnion_of_mem ⟨_, typesWith_top⟩
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith φ)

Tactic:
isOpen_generateFrom_of_mem ⟨φ, rfl⟩

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
rw : IsOpen (T.typesWith ∼φ)
⊢ IsOpen (T.typesWith φ)ᶜ

Tactic:
rw [← typesWith_not]

Premises used: FirstOrder.Language.Theory.CompleteType.typesWith_not
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith ∼φ)

Tactic:
isOpen_typesWith _

Premises used: CompleteType.isOpen_typesWith
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith ∼φ)

Tactic:
exact isOpen_typesWith _

Premises used: CompleteType.isOpen_typesWith
-- Module: Mathlib.ModelTheory.Topology.Types
Goal:
L : Language
T : L.Theory
α : Type u_1
rw : Pairwise fun (x1 x2 : T.CompleteType α) ↦ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
⊢ TotallySeparatedSpace (T.CompleteType α)

Tactic:
rw [totallySeparatedSpace_iff_exists_isClopen]

Premises used: totallySeparatedSpace_iff_exists_isClopen