-- Mathlib/ModelTheory/Semantics.lean
theorem model_distinctConstantsTheory {M : Type w} [L[[α]].Structure M] (s : Set α) :
    M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i : α => (L.con i : M)) s

Proof state:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : M ⊨ ((L.con a).term.equal (L.con b).term).not
⊢ ↑(L.con a) ≠ ↑(L.con b)

Tactic:
simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal,
  Term.realize_constants] at h'

Result:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : ¬↑(L.con a) = ↑(L.con b)
⊢ ↑(L.con a) ≠ ↑(L.con b)

Proof state:
case refine_2
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ Set.InjOn (fun i => ↑(L.con i)) s →
    ∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ

Tactic:
rintro h φ a b ⟨⟨as, bs⟩, ab⟩ rfl

Result:
case refine_2.intro.intro
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h : Set.InjOn (fun i => ↑(L.con i)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ M ⊨ ((L.con a).term.equal (L.con b).term).not

Proof state:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : ¬↑(L.con a) = ↑(L.con b)
⊢ ↑(L.con a) ≠ ↑(L.con b)

Tactic:
exact h'

Result:
no goals

Proof state:
case refine_2.intro.intro
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h : Set.InjOn (fun i => ↑(L.con i)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ M ⊨ ((L.con a).term.equal (L.con b).term).not

Tactic:
simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants]

Result:
case refine_2.intro.intro
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h : Set.InjOn (fun i => ↑(L.con i)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ ¬↑(L.con a) = ↑(L.con b)

Proof state:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
⊢ ↑(L.con a) ≠ ↑(L.con b)

Tactic:
have h' := h _ a b ⟨⟨as, bs⟩, ab⟩ rfl

Result:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : M ⊨ ((L.con a).term.equal (L.con b).term).not
⊢ ↑(L.con a) ≠ ↑(L.con b)

Proof state:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(L.con i)) a = (fun i => ↑(L.con i)) b
⊢ a = b

Tactic:
contrapose! ab

Result:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
⊢ ↑(L.con a) ≠ ↑(L.con b)

Proof state:
case refine_2.intro.intro
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h : Set.InjOn (fun i => ↑(L.con i)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ ¬↑(L.con a) = ↑(L.con b)

Tactic:
exact fun contra => ab (h as bs contra)

Result:
no goals

Proof state:
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i => ↑(L.con i)) s

Tactic:
simp only [distinctConstantsTheory, Theory.model_iff, Set.mem_image, Set.mem_inter,
  Set.mem_prod, Set.mem_compl, Prod.exists, forall_exists_index, and_imp]

Result:
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ) ↔
    Set.InjOn (fun i => ↑(L.con i)) s

Proof state:
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ) ↔
    Set.InjOn (fun i => ↑(L.con i)) s

Tactic:
refine ⟨fun h a as b bs ab => ?_, ?_⟩

Result:
case refine_1
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(L.con i)) a = (fun i => ↑(L.con i)) b
⊢ a = b

case refine_2
L : Language
α : Type u'
M : Type w
inst✝ : L[[α]].Structure M
s : Set α
⊢ Set.InjOn (fun i => ↑(L.con i)) s →
    ∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ