L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      (s ×ˢ s ∩ diagonal αᶜ) =
    ⋃ (t : Finset ↑s),
      (fun ab =>
          Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
        (↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ∩
          diagonal αᶜ)
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ distinctConstantsTheory L s =
    ⋃ (t : Finset ↑s), distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t)
simp only [distinctConstantsTheory]
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      (s ×ˢ s ∩ diagonal αᶜ) =
    (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      ((⋃ (i : Finset ↑s),
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)) ∩
        diagonal αᶜ)
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      (s ×ˢ s ∩ diagonal αᶜ) =
    ⋃ (t : Finset ↑s),
      (fun ab =>
          Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
        (↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) t) ∩
          diagonal αᶜ)
rw [← image_iUnion, ← iUnion_inter]
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ s ×ˢ s =
    ⋃ (i : Finset ↑s),
      ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      (s ×ˢ s ∩ diagonal αᶜ) =
    (fun ab =>
        Formula.not (Term.equal (Constants.term (Language.con L ab.fst)) (Constants.term (Language.con L ab.snd)))) ''
      ((⋃ (i : Finset ↑s),
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
            ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)) ∩
        diagonal αᶜ)
refine' congr rfl (congr (congr rfl _) rfl)
case h.mk
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    (i, j) ∈
      ⋃ (i : Finset ↑s),
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
⊢ s ×ˢ s =
    ⋃ (i : Finset ↑s),
      ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
ext ⟨i, j⟩
case h.mk
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ i_1, (∃ x, { val := i, property := (_ : i ∈ s) } ∈ i_1) ∧ ∃ x, { val := j, property := (_ : j ∈ s) } ∈ i_1
case h.mk
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    (i, j) ∈
      ⋃ (i : Finset ↑s),
        ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i) ×ˢ
          ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
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]
case h.mk.refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ { val := i, property := (_ : i ∈ s) } ∈ {{ val := i, property := (_ : i ∈ s) }, { val := j, property := (_ : j ∈ s) }}

case h.mk.refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ { val := j, property := (_ : j ∈ s) } ∈ {{ val := i, property := (_ : i ∈ s) }, { val := j, property := (_ : j ∈ s) }}

case h.mk.refine'_3
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
⊢ (∃ i_1, (∃ x, { val := i, property := (_ : i ∈ s) } ∈ i_1) ∧ ∃ x, { val := j, property := (_ : j ∈ s) } ∈ i_1) →
    i ∈ s ∧ j ∈ s
case h.mk
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ i_1, (∃ x, { val := i, property := (_ : i ∈ s) } ∈ i_1) ∧ ∃ x, { val := j, property := (_ : j ∈ s) } ∈ i_1
refine' ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, _⟩, ⟨h.2, _⟩⟩, _⟩
no goals
case h.mk.refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ { val := i, property := (_ : i ∈ s) } ∈ {{ val := i, property := (_ : i ∈ s) }, { val := j, property := (_ : j ∈ s) }}
simp
no goals
case h.mk.refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
h : i ∈ s ∧ j ∈ s
⊢ { val := j, property := (_ : j ∈ s) } ∈ {{ val := i, property := (_ : i ∈ s) }, { val := j, property := (_ : j ∈ s) }}
simp
case h.mk.refine'_3.intro.intro.intro.intro
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
t : Finset ↑s
is : i ∈ s
h✝¹ : { val := i, property := (_ : i ∈ s) } ∈ t
js : j ∈ s
h✝ : { val := j, property := (_ : j ∈ s) } ∈ t
⊢ i ∈ s ∧ j ∈ s
case h.mk.refine'_3
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
⊢ (∃ i_1, (∃ x, { val := i, property := (_ : i ∈ s) } ∈ i_1) ∧ ∃ x, { val := j, property := (_ : j ∈ s) } ∈ i_1) →
    i ∈ s ∧ j ∈ s
rintro ⟨t, ⟨is, _⟩, ⟨js, _⟩⟩
no goals
case h.mk.refine'_3.intro.intro.intro.intro
L : Language
L' : Language
M : Type w
N : Type ?u.204492
P : Type ?u.204495
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.204523
n : ℕ
s : Set α
i j : α
t : Finset ↑s
is : i ∈ s
h✝¹ : { val := i, property := (_ : i ∈ s) } ∈ t
js : j ∈ s
h✝ : { val := j, property := (_ : j ∈ s) } ∈ t
⊢ i ∈ s ∧ j ∈ s
exact ⟨is, js⟩