awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Sentence
rw : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ N ⊨ φ
rw₁ : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ Formula.Realize.{u, v, u_1, 0} (M := N) φ default
rw₂ :
  Formula.Realize.{u, v, u_1, 0} (M := N) φ (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default) ↔
    Formula.Realize.{u, v, u_1, 0} (M := N) φ default
rw₃ rw₄ : Formula.Realize.{u, v, u_1, 0} (M := N) φ default ↔ Formula.Realize.{u, v, u_1, 0} (M := N) φ default
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]

Premises used: FirstOrder.Language.Sentence.Realize, Inhabited.default, Function.comp, Unique.eq_default, FirstOrder.Language.StrongHomClass.realize_formula, DFunLike.coe
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
T : L.Theory
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
inst_4 : M ⊨ T
⊢ N ⊨ T

Tactic:
⟨fun φ hφ => (realize_sentence g φ).1 (Theory.realize_sentence_of_mem T hφ)⟩

Premises used: FirstOrder.Language.StrongHomClass.realize_sentence, FirstOrder.Language.Theory.Model.mk, Iff.mp, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
⊢ M ≅[L] N

Tactic:
elementarilyEquivalent_iff.2 (realize_sentence g)

Premises used: Iff.mpr, FirstOrder.Language.StrongHomClass.realize_sentence, FirstOrder.Language.elementarilyEquivalent_iff
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
rw : M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]
⊢ M ⊨ r.reflexive ↔ Std.Refl fun (x y : M) ↦ RelMap r ![x, y]

Tactic:
rw [refl_def]

Premises used: refl_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]

Tactic:
forall_congr' fun _ ↦ realize_rel₂

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Relations.reflexive, forall_congr', FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]

Tactic:
exact forall_congr' fun _ ↦ realize_rel₂

Premises used: forall_congr', FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
rw : M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]
⊢ M ⊨ r.irreflexive ↔ Std.Irrefl fun (x y : M) ↦ RelMap r ![x, y]

Tactic:
rw [irrefl_def]

Premises used: irrefl_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]

Tactic:
forall_congr' fun _ ↦ not_congr realize_rel₂

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.BoundedFormula.Realize, forall_congr', FirstOrder.Language.Relations.irreflexive, not_congr, FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]

Tactic:
exact forall_congr' fun _ ↦ not_congr realize_rel₂

Premises used: forall_congr', not_congr, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.symmetric ↔ Symmetric fun (x y : M) ↦ RelMap r ![x, y]

Tactic:
forall₂_congr fun _ _ ↦ imp_congr realize_rel₂ realize_rel₂

Premises used: FirstOrder.Language.Sentence.Realize, Symmetric, FirstOrder.Language.BoundedFormula.Realize, forall₂_congr, imp_congr, FirstOrder.Language.Relations.symmetric, FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
rw : M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b
⊢ M ⊨ r.antisymmetric ↔ Std.Antisymm fun (x y : M) ↦ RelMap r ![x, y]

Tactic:
rw [antisymm_def]

Premises used: antisymm_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b

Tactic:
forall₂_congr fun _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ .rfl

Premises used: FirstOrder.Language.Sentence.Realize, Iff.rfl, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Relations.antisymmetric, forall₂_congr, imp_congr, FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b

Tactic:
exact forall₂_congr fun _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ .rfl

Premises used: Iff.rfl, forall₂_congr, imp_congr, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
rw : M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]
⊢ M ⊨ r.transitive ↔ IsTrans M fun (x y : M) ↦ RelMap r ![x, y]

Tactic:
rw [isTrans_def]

Premises used: isTrans_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]

Tactic:
forall₃_congr fun _ _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ realize_rel₂

Premises used: FirstOrder.Language.Sentence.Realize, forall₃_congr, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Relations.transitive, imp_congr, FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]

Tactic:
exact forall₃_congr fun _ _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ realize_rel₂

Premises used: forall₃_congr, imp_congr, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
rw : M ⊨ r.total ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] ∨ RelMap r ![b, a]
⊢ M ⊨ r.total ↔ Std.Total fun (x y : M) ↦ RelMap r ![x, y]

Tactic:
rw [total_def]

Premises used: total_def
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.total ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] ∨ RelMap r ![b, a]

Tactic:
forall₂_congr fun _ _ ↦ realize_sup.trans <| or_congr realize_rel₂ realize_rel₂

Premises used: FirstOrder.Language.Relations.total, or_congr, FirstOrder.Language.Sentence.Realize, FirstOrder.Language.BoundedFormula.Realize, forall₂_congr, Iff.trans, FirstOrder.Language.BoundedFormula.realize_sup, FirstOrder.Language.Formula.Realize, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.total ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] ∨ RelMap r ![b, a]

Tactic:
exact forall₂_congr fun _ _ ↦ realize_sup.trans <| or_congr realize_rel₂ realize_rel₂

Premises used: or_congr, forall₂_congr, Iff.trans, FirstOrder.Language.BoundedFormula.realize_sup, FirstOrder.Language.BoundedFormula.realize_rel₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
rw :
  (∃ (xs : Fin n → M),
      BoundedFormula.Realize.{u, v, w, 0} (L := L) (α := Empty)
        (List.foldr (fun (x1 x2 : L.BoundedFormula Empty n) ↦ x1 ⊓ x2) ⊤
          (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n))))
        default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
⊢ M ⊨ Sentence.cardGe L n ↔ (↑n : Cardinal.{w}) ≤ #M

Tactic:
rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
    BoundedFormula.realize_exs]

Premises used: FirstOrder.Language.Sentence.Realize, Cardinal.lift_mk_le, Cardinal.lift_lift, Cardinal.lift_mk_fin, FirstOrder.Language.BoundedFormula.realize_exs, FirstOrder.Language.Sentence.cardGe, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
simp_rw :
  (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n),
        Membership.mem (γ := List (L.BoundedFormula Empty n))
            (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))
            φ →
          φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
⊢ (∃ (xs : Fin n → M),
      BoundedFormula.Realize.{u, v, w, 0} (L := L) (α := Empty)
        (List.foldr (fun (x1 x2 : L.BoundedFormula Empty n) ↦ x1 ⊓ x2) ⊤
          (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n))))
        default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)

Tactic:
simp_rw [BoundedFormula.realize_foldr_inf]

Premises used: FirstOrder.Language.BoundedFormula.realize_foldr_inf
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
simp :
  (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
⊢ (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n),
        Membership.mem (γ := List (L.BoundedFormula Empty n))
            (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))
            φ →
          φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)

Tactic:
simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne, List.mem_product,
    List.mem_finRange, forall_exists_index, and_imp, List.mem_filter, true_and]

Premises used: List.mem_product, and_imp, forall_exists_index, Ne, List.mem_finRange, List.mem_filter, Function.comp_apply, List.mem_map, Prod.exists, true_and
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
⊢ (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)

Tactic:
⟨?_, fun xs => ⟨xs.some, ?_⟩⟩

Premises used: Nonempty.some, Iff.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
refine_1 :
  (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) →
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
refine_2 :
  ∀ (xs : Nonempty.{max (w + 1) 1} (Fin n ↪ M)) (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true →
      ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize (M := M) default (⇑xs.some : (a : Fin n) → M)
⊢ (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)

Tactic:
refine ⟨?_, fun xs => ⟨xs.some, ?_⟩⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
⊢ Nonempty.{max (w + 1) 1} (Fin n ↪ M)

Tactic:
⟨⟨xs, fun i j ij => ?_⟩⟩

Premises used: Function.Embedding.mk, Nonempty.intro
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
refine_1 : ∀ (i j : Fin n) (ij : xs i = xs j), i = j
⊢ Nonempty.{max (w + 1) 1} (Fin n ↪ M)

Tactic:
refine ⟨⟨xs, fun i j ij => ?_⟩⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : xs i = xs j
refine_1 : ∀ (ij : i ≠ j), xs i ≠ xs j
⊢ i = j

Tactic:
contrapose! ij
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ (decide ¬i = j) = true

Tactic:
simpa using ij
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : i ≠ j
⊢ xs i ≠ xs j

Tactic:
exact h _ i j (by simpa using ij) rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Nonempty.{max (w + 1) 1} (Fin n ↪ M)
i j : Fin n
ij : (decide ¬i = j) = true
⊢ BoundedFormula.Realize.{u, v, w, 0} (L := L) (M := M) (α := Empty) (∼(var (Sum.inr i) =' var (Sum.inr j))) default
    (⇑xs.some : (a : Fin n) → M)

Tactic:
simpa using ij
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ M ⊨ L.infiniteTheory ↔ Infinite M

Tactic:
simp [infiniteTheory, infinite_iff, aleph0_le]

Premises used: FirstOrder.Language.infiniteTheory, Cardinal.aleph0_le, Cardinal.infinite_iff
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
T : L.Theory
h : Infinite M
⊢ M ⊨ L.infiniteTheory

Tactic:
L.model_infiniteTheory_iff.2 h

Premises used: Iff.mpr, FirstOrder.Language.model_infiniteTheory_iff
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ M ⊨ L.nonemptyTheory ↔ Nonempty M

Tactic:
simp only [nonemptyTheory, Theory.model_iff, Set.mem_singleton_iff, forall_eq,
    Sentence.realize_cardGe, Nat.cast_one, Cardinal.one_le_iff_ne_zero, mk_ne_zero_iff]

Premises used: Cardinal.mk_ne_zero_iff, FirstOrder.Language.Sentence.realize_cardGe, FirstOrder.Language.Theory.model_iff, forall_eq, Cardinal.one_le_iff_ne_zero, Set.mem_singleton_iff, FirstOrder.Language.nonemptyTheory, Nat.cast_one
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
T : L.Theory
h : Nonempty M
⊢ M ⊨ L.nonemptyTheory

Tactic:
L.model_nonemptyTheory_iff.2 h

Premises used: Iff.mpr, FirstOrder.Language.model_nonemptyTheory_iff
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
simp :
  (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ) ↔
    Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
⊢ M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s

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

Premises used: and_imp, FirstOrder.Language.Theory.model_iff, Set.mem_image, forall_exists_index, FirstOrder.Language.distinctConstantsTheory, Prod.exists
-- Module: Mathlib.ModelTheory.Semantics
Goal:
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 α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ) ↔
    Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s

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

Premises used: Iff.intro
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
refine_1 :
  ∀
    (h :
      ∀ (φ : L[[α]].Sentence) (x x_1 : α),
        (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ)
    (a : α) (as : a ∈ s) (b : α) (bs : b ∈ s)
    (ab : Eq.{w + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)),
    a = b
refine_2 :
  Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s →
    ∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
⊢ (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ) ↔
    Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s

Tactic:
refine ⟨fun h a as b bs ab => ?_, ?_⟩
-- Module: Mathlib.ModelTheory.Semantics
Goal:
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 α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : Eq.{w + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)
refine_1 : ∀ (ab : a ≠ b), Ne.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
⊢ a = b

Tactic:
contrapose! ab
-- Module: Mathlib.ModelTheory.Semantics
Goal:
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 α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
⊢ M ⊨ Formula.not (Term.equal (L.con a).term (L.con b).term)

Tactic:
have h' := h _ a b ⟨⟨as, bs⟩, ab⟩ rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
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 α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : M ⊨ Formula.not (Term.equal (L.con a).term (L.con b).term)
⊢ ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)

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

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.Formula.realize_equal, FirstOrder.Language.Term.realize_constants, FirstOrder.Language.Formula.realize_not
-- Module: Mathlib.ModelTheory.Semantics
Goal:
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 α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
⊢ Ne.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)

Tactic:
h'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
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 α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
⊢ Ne.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)

Tactic:
exact h'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h : Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
refine_2 : ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
⊢ M ⊨ Formula.not (Term.equal (L.con a).term (L.con b).term)

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

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.Formula.realize_equal, FirstOrder.Language.Term.realize_constants, FirstOrder.Language.Formula.realize_not
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h : Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)

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

Premises used: Not
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h : Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)

Tactic:
exact fun contra => ab (h as bs contra)
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
α : Type u'
s : Set α
M : Type w
inst : L[[α]].Structure M
h : M ⊨ L.distinctConstantsTheory s
⊢ lift.{w, u'} #(↑s : Type u') ≤ lift.{u', w} #M

Tactic:
lift_mk_le'.2 ⟨⟨_, Set.injOn_iff_injective.1 ((L.model_distinctConstantsTheory s).1 h)⟩⟩

Premises used: Iff.mpr, Function.Embedding.mk, Set.injOn_iff_injective, Nonempty.intro, FirstOrder.Language.model_distinctConstantsTheory, Iff.mp, Cardinal.lift_mk_le'
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
h : M ≅[L] N
⊢ N ≅[L] M

Tactic:
h.symm

Premises used: FirstOrder.Language.ElementarilyEquivalent, Eq.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
MN : M ≅[L] N
NP : N ≅[L] P
⊢ M ≅[L] P

Tactic:
MN.trans NP

Premises used: FirstOrder.Language.ElementarilyEquivalent, Eq.trans
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
h : M ≅[L] N
⊢ L.completeTheory M = L.completeTheory N

Tactic:
h

Premises used: FirstOrder.Language.ElementarilyEquivalent
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
h : M ≅[L] N
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
(elementarilyEquivalent_iff.1 h) φ

Premises used: FirstOrder.Language.elementarilyEquivalent_iff, Iff.mp