awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
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 ⋯)
⊢ 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
have h₂ : (∃ (i_1 : Finset (↑s : Type u')),
    (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i sorry ∈ i_1) ∧
      ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j sorry ∈ i_1) →
  i ∈ s ∧ j ∈ s
Tactic: refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have simp : 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: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have simp₁ : 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: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
simp₁ :
  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 α)ᶜ))
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have simp₂ : 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: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
simp₁ :
  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 α)ᶜ))
simp₂ :
  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 α)
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have 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)
Tactic: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
simp₁ :
  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 α)ᶜ))
simp₂ :
  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 α)
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)
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have h₁ : ∀ (i j : α),
  i ∈ s ∧ j ∈ s ↔
    ∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i sorry ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j sorry ∈ i_1
Tactic: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
simp₁ :
  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 α)ᶜ))
simp₂ :
  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 α)
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)
h₁ :
  ∀ (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
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have h₂ : ∀ (i j : α) (h : i ∈ s ∧ j ∈ s),
  Membership.mem (γ := Finset { x : α // x ∈ s })
    {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i sorry, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j sorry}
    (Subtype.mk (p := fun (a : α) ↦ a ∈ s) i sorry)
Tactic: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
simp₁ :
  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 α)ᶜ))
simp₂ :
  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 α)
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)
h₁ :
  ∀ (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
h₂ :
  ∀ (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 ⋯)
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have h₃ : ∀ (i j : α) (h : i ∈ s ∧ j ∈ s),
  Membership.mem (γ := Finset { x : α // x ∈ s })
    {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i sorry, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j sorry}
    (Subtype.mk (p := fun (a : α) ↦ a ∈ s) j sorry)
Tactic: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
simp :
  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 α)ᶜ))
simp₁ :
  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 α)ᶜ))
simp₂ :
  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 α)
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)
h₁ :
  ∀ (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
h₂ :
  ∀ (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 ⋯)
h₃ :
  ∀ (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 ⋯)
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)
have h₄ : ∀ (i j : α),
  (∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i sorry ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j sorry ∈ i_1) →
    i ∈ s ∧ j ∈ s
Tactic: classical
    simp only [distinctConstantsTheory]
    rw [← image_iUnion, ← iUnion_inter]
    refine congr(_ '' ($(?_) ∩ _))
    ext ⟨i, j⟩
    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]
    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
    · simp
    · simp
    · rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
      exact ⟨is, js⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
⊢ 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₂
have 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₂
Tactic: ⟨φ, ht₁⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : 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₂
have 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₂
Tactic: ⟨ψ, ht₂⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
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₂
have refine : x ∈ T.typesWith (φ ⊓ ψ) ∧ T.typesWith (φ ⊓ ψ) ⊆ t₁ ∩ t₂
Tactic: refine ⟨T.typesWith (φ ⊓ ψ), ⟨φ ⊓ ψ, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
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.typesWith (φ ⊓ ψ) ∧ T.typesWith (φ ⊓ ψ) ⊆ t₁ ∩ t₂
have rw : x ∈ t₁ ∩ t₂ ∧ t₁ ∩ t₂ ⊆ t₁ ∩ t₂
Tactic: rw [typesWith_inf, ht₁, ht₂]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ Eq (α := Set (T.CompleteType α)) (⋃₀ range T.typesWith) univ
have rw : Subset (α := Set (T.CompleteType α)) univ (⋃₀ range T.typesWith)
Tactic: rw [← Set.univ_subset_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
φ : L[[α]].Sentence
⊢ IsOpen (T.typesWith φ)ᶜ
have rw : IsOpen (T.typesWith ∼φ)
Tactic: rw [← typesWith_not]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
⊢ TotallySeparatedSpace (T.CompleteType α)
have rw : Pairwise fun (x1 x2 : T.CompleteType α) ↦ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
Tactic: rw [totallySeparatedSpace_iff_exists_isClopen]
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
hpq : p ≠ q
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
have hpq₁ : ∃ (x : L[[α]].Sentence), x ∉ p ↔ x ∈ q
Tactic: simp only [ne_eq, SetLike.ext_iff, not_forall, not_iff] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
hpq : ∃ (x : L[[α]].Sentence), x ∉ p ↔ x ∈ q
⊢ ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
have obtain : ∀ (φ : L[[α]].Sentence) (hφ : φ ∉ p ↔ φ ∈ q), ∃ (U : Set (T.CompleteType α)), IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ
Tactic: obtain ⟨φ, hφ⟩ := hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
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ᶜ
have inl : q ∈ (T.typesWith φ)ᶜ
Tactic: refine ⟨T.typesWith φ, isClopen_typesWith _, h, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Topology.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ q ∈ (T.typesWith φ)ᶜ
have inl : q ∉ T.typesWith φ
Tactic: rwa [mem_compl_iff, mem_typesWith_iff, ← hφ, not_not]