-- Module: Mathlib.ModelTheory.Syntax
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 ⋯)
h₄ :
  ∀ (i j : α),
    (∃ (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
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 ⋯)
h₆ h₇ :
  ∀ (i j : α),
    (∃ (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
⊢ L.distinctConstantsTheory s =
    ⋃ (t : Finset (↑s : Type u')),
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : 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⟩

Premises used: Set.mem_iUnion, Set.mem_image, Function.Embedding.coe_subtype, Subtype.exists, exists_eq_right, Set.prodMk_mem_set_prod_eq, FirstOrder.Language.distinctConstantsTheory, exists_and_right, Set.iUnion_inter, Set.image_iUnion, Finset.coe_map, Finset.mem_coe