-- Mathlib/ModelTheory/Syntax.lean
theorem distinctConstantsTheory_eq_iUnion (s : Set α) :
    L.distinctConstantsTheory s =
      ⋃ t : Finset s,
        L.distinctConstantsTheory (t.map (Function.Embedding.subtype fun x => x ∈ s))

Proof state:
case h.mk.refine_3.intro.intro.intro.intro
L : Language
α : Type u'
s : Set α
i j : α
t : Finset ↑s
is : i ∈ s
h✝¹ : ⟨i, ⋯⟩ ∈ t
js : j ∈ s
h✝ : ⟨j, ⋯⟩ ∈ t
⊢ i ∈ s ∧ j ∈ s

Tactic:
exact ⟨is, js⟩

Result:
no goals

Proof state:
L : Language
α : Type u'
s : Set α
⊢ (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ((⋃ i,
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)) ∩
        (diagonal α)ᶜ)

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

Result:
L : Language
α : Type u'
s : Set α
⊢ s ×ˢ s =
    ⋃ i,
      ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Proof state:
case h.mk
L : Language
α : Type u'
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔ ∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1

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

Result:
case h.mk.refine_1
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨i, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

case h.mk.refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

case h.mk.refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Proof state:
L : Language
α : Type u'
s : Set α
⊢ s ×ˢ s =
    ⋃ i,
      ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Tactic:
ext ⟨i, j⟩

Result:
case h.mk
L : Language
α : Type u'
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    (i, j) ∈
      ⋃ i,
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Proof state:
L : Language
α : Type u'
s : Set α
⊢ (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    ⋃ t,
      (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
        (↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ∩
          (diagonal α)ᶜ)

Tactic:
rw [← image_iUnion, ← iUnion_inter]

Result:
L : Language
α : Type u'
s : Set α
⊢ (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
      ((⋃ i,
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)) ∩
        (diagonal α)ᶜ)

Proof state:
case h.mk.refine_2
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨j, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

Tactic:
simp

Result:
no goals

Proof state:
case h.mk
L : Language
α : Type u'
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    (i, j) ∈
      ⋃ i,
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

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

Result:
case h.mk
L : Language
α : Type u'
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔ ∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1

Proof state:
case h.mk.refine_1
L : Language
α : Type u'
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ ⟨i, ⋯⟩ ∈ {⟨i, ⋯⟩, ⟨j, ⋯⟩}

Tactic:
simp

Result:
no goals

Proof state:
L : Language
α : Type u'
s : Set α
⊢ L.distinctConstantsTheory s =
    ⋃ t, L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)

Tactic:
simp only [distinctConstantsTheory]

Result:
L : Language
α : Type u'
s : Set α
⊢ (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (diagonal α)ᶜ) =
    ⋃ t,
      (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) ''
        (↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ∩
          (diagonal α)ᶜ)

Proof state:
case h.mk.refine_3
L : Language
α : Type u'
s : Set α
i j : α
⊢ (∃ i_1, (∃ (x : i ∈ s), ⟨i, ⋯⟩ ∈ i_1) ∧ ∃ (x : j ∈ s), ⟨j, ⋯⟩ ∈ i_1) → i ∈ s ∧ j ∈ s

Tactic:
rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩

Result:
case h.mk.refine_3.intro.intro.intro.intro
L : Language
α : Type u'
s : Set α
i j : α
t : Finset ↑s
is : i ∈ s
h✝¹ : ⟨i, ⋯⟩ ∈ t
js : j ∈ s
h✝ : ⟨j, ⋯⟩ ∈ t
⊢ i ∈ s ∧ j ∈ s