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
T : L.Theory
h : M ≅[L] N
rw : T ⊆ L.completeTheory M ↔ N ⊨ T
rw₁ : T ⊆ L.completeTheory M ↔ T ⊆ L.completeTheory N
rw₂ rw₃ : T ⊆ L.completeTheory N ↔ T ⊆ L.completeTheory N
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
    h.completeTheory_eq]

Premises used: FirstOrder.Language.ElementarilyEquivalent.completeTheory_eq, FirstOrder.Language.Theory.model_iff_subset_completeTheory
-- 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
MT : M ⊨ T
h : M ≅[L] N
⊢ N ⊨ T

Tactic:
h.theory_model_iff.1 MT

Premises used: FirstOrder.Language.ElementarilyEquivalent.theory_model_iff, Iff.mp
-- 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
⊢ Nonempty M ↔ Nonempty N

Tactic:
(model_nonemptyTheory_iff L).symm.trans (h.theory_model_iff.trans (model_nonemptyTheory_iff L))

Premises used: FirstOrder.Language.ElementarilyEquivalent.theory_model_iff, Iff.trans, FirstOrder.Language.model_nonemptyTheory_iff, Iff.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
Mn : Nonempty M
h : M ≅[L] N
⊢ Nonempty N

Tactic:
h.nonempty_iff.1 Mn

Premises used: FirstOrder.Language.ElementarilyEquivalent.nonempty_iff, Iff.mp
-- 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
⊢ Infinite M ↔ Infinite N

Tactic:
(model_infiniteTheory_iff L).symm.trans (h.theory_model_iff.trans (model_infiniteTheory_iff L))

Premises used: FirstOrder.Language.ElementarilyEquivalent.theory_model_iff, FirstOrder.Language.model_infiniteTheory_iff, Iff.trans, Iff.symm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
Mi : Infinite M
h : M ≅[L] N
⊢ Infinite N

Tactic:
h.infinite_iff.1 Mi

Premises used: FirstOrder.Language.ElementarilyEquivalent.infinite_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
simp :
  ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
      sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) = #((n : ℕ) × L.BoundedFormula Empty (n + 1))

Tactic:
simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']

Premises used: FirstOrder.Language.skolem₁_Functions, Cardinal.sum_add_distrib', Cardinal.mk_sigma, FirstOrder.Language.card_functions_sum
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
h : ∀ (i : ℕ), lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
| (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
    sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
enter [2, 1, i]
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
i : ℕ
h : #(L.BoundedFormula Empty (i + 1))
| lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [lift_id'.{u, v}]
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
h : ∀ (i : ℕ), #(L.BoundedFormula Empty (i + 1))
| (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
    sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))

Tactic:
enter [2, 1, i]; rw [lift_id'.{u, v}]
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
conv_lhs :
  ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) + sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
⊢ ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
      sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
rw : (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
rw₁ : ℵ₀ ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
⊢ ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) + sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [add_comm, add_eq_max, max_eq_left]

Premises used: max_eq_left, add_comm, Cardinal.add_eq_max
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
H : ∀ (n : ℕ), lift.{max u v, u} #(L.Functions n) ≤ #(L.BoundedFormula Empty (n + 1))
⊢ (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
gcongr with n
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
n : ℕ
H : Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))
⊢ lift.{max u v, u} #(L.Functions n) ≤ #(L.BoundedFormula Empty (n + 1))

Tactic:
rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]

Premises used: Cardinal.lift_lift
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
n : ℕ
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))

Tactic:
⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => ?_⟩⟩

Premises used: Inhabited.default, FirstOrder.Language.Term.bdEqual, Function.Embedding.mk, Nonempty.intro, FirstOrder.Language.Term.func
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
n : ℕ
H :
  ∀ (f g : L.Functions n)
    (h :
      Eq (α := L.BoundedFormula Empty (n + 1))
        ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) f)
        ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) g)),
    f = g
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))

Tactic:
refine ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => ?_⟩⟩
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
n : ℕ
f g : L.Functions n
h :
  Eq (α := L.BoundedFormula Empty (n + 1))
    ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) f)
    ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) g)
H : f = f
⊢ f = g

Tactic:
rcases h with ⟨rfl, ⟨rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
n : ℕ
f : L.Functions n
⊢ f = f

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
rw : ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))
⊢ ℵ₀ ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [← mk_sigma]

Premises used: Cardinal.mk_sigma
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))

Tactic:
infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
      (Sigma.mk.inj_iff.1 xy).1)

Premises used: Infinite.of_injective, Cardinal.infinite_iff, Bot.bot, And.left, Iff.mp, Sigma.mk.inj_iff, Sigma.mk
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))

Tactic:
exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
      (Sigma.mk.inj_iff.1 xy).1)

Premises used: Infinite.of_injective, Cardinal.infinite_iff, And.left, Iff.mp, Sigma.mk.inj_iff
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
rw : #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ max ℵ₀ L.card

Tactic:
rw [card_functions_sum_skolem₁]

Premises used: FirstOrder.Language.card_functions_sum_skolem₁
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
trans : #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)
trans₁ : #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card

Tactic:
trans #(Σ n, L.BoundedFormula Empty n)

Premises used: Empty, FirstOrder.Language.BoundedFormula, Sigma
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)

Tactic:
⟨⟨Sigma.map Nat.succ fun _ => id,
          Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩

Premises used: Function.Embedding.mk, id, Function.Injective.sigma_map, Nonempty.intro, Function.injective_id, Nat.succ_injective, Sigma.map, Nat.succ
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)

Tactic:
exact
      ⟨⟨Sigma.map Nat.succ fun _ => id,
          Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card

Tactic:
_root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)

Premises used: trans, Iff.mp, Cardinal.lift_le, FirstOrder.Language.BoundedFormula.card_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
refine :
  lift.{max u v, max u v} (max ℵ₀ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
    lift.{max u v, max u v} (max ℵ₀ L.card)
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card

Tactic:
refine _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
simp : lift.{max u v, max u v} (max ℵ₀ L.card) ≤ lift.{max u v, max u v} (max ℵ₀ L.card)
⊢ lift.{max u v, max u v} (max ℵ₀ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
    lift.{max u v, max u v} (max ℵ₀ L.card)

Tactic:
simp only [mk_empty, lift_zero, lift_uzero, zero_add]

Premises used: Cardinal.lift_zero, zero_add, Cardinal.lift_uzero, Cardinal.mk_empty
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
⊢ lift.{max u v, max u v} (max ℵ₀ L.card) ≤ lift.{max u v, max u v} (max ℵ₀ L.card)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
apply :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1))
    (x :
      Fin n →
        ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
            L.Substructure M))
    (a : M),
    BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
          (Subtype.val (p := fun (x : M) ↦
              Membership.mem (γ := L.Substructure M)
                ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                  L.Substructure M)
                x) ∘
            x)
          a) →
      ∃ (b :
        ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
            L.Substructure M)),
        BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
            (Subtype.val (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                    L.Substructure M)
                  x) ∘
              x)
            (↑b : M))
⊢ IsElementary.{w, u, v} (L := L) (M := M)
    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S)

Tactic:
apply (LHom.sumInl.substructureReduct S).isElementary_of_exists

Premises used: FirstOrder.Language.LHom.substructureReduct, FirstOrder.Language.Substructure.isElementary_of_exists, DFunLike.coe, FirstOrder.Language.LHom.sumInl
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
h₁ :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x)
            (funMap φ'
              (Subtype.val (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M)
                        S :
                      L.Substructure M)
                    x) ∘
                x))
            ⋯) :
        M))
w :
  Membership.mem (γ := L.Substructure M)
    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
      L.Substructure M)
    (funMap φ'
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x))
⊢ ∃ (b :
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)),
    BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x) ∘
          x)
        (↑b : M))

Tactic:
use ⟨funMap φ' ((↑) ∘ x), ?_⟩
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
⊢ BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x)
            (funMap φ'
              (Subtype.val (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M)
                        S :
                      L.Substructure M)
                    x) ∘
                x))
            ⋯) :
        M))

Tactic:
Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default
          (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩

Premises used: Classical.epsilon, Exists.intro, Classical.epsilon_spec, Sum.elim
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
⊢ BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x)
            (funMap φ'
              (Subtype.val (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M)
                        S :
                      L.Substructure M)
                    x) ∘
                x))
            ⋯) :
        M))

Tactic:
exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default
          (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩

Premises used: Exists.intro, Classical.epsilon_spec
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
⊢ ∀ (i : Fin n),
    (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x) ∘
          x)
        i ∈
      (↑S : Set M)

Tactic:
fun i => (x i).2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
⊢ ∀ (i : Fin n),
    (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x) ∘
          x)
        i ∈
      (↑S : Set M)

Tactic:
exact fun i => (x i).2

Premises used: Subtype.property
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
⊢ Membership.mem (γ := L.Substructure M)
    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
      L.Substructure M)
    (funMap φ'
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x))

Tactic:
exact S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by
      exact fun i => (x i).2)

Premises used: FirstOrder.Language.Substructure.fun_mem, FirstOrder.Language.LHom.sumInr, Function.comp, FirstOrder.Language.LHom.onFunction
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
⊢ ↥S.elementarySkolem₁Reduct = ↥S

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
⊢ Small.{max u v, w} ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : L.Structure M
⊢ ∃ (S : L.ElementarySubstructure M), Small.{max u v, w} ↥S

Tactic:
(isEmpty_or_nonempty M).elim
    (fun _ => ⟨⊤, Countable.toSmall _⟩)
    (fun _ => ⟨Substructure.elementarySkolem₁Reduct ⊥, inferInstance⟩)

Premises used: Membership.mem, inferInstance, isEmpty_or_nonempty, Subtype, Bot.bot, Exists.intro, FirstOrder.Language.Substructure.elementarySkolem₁Reduct, Top.top, Or.elim, Countable.toSmall
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ κ
h2 : lift.{w', w} #(↑s : Type w) ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
obtain :
  ∀ (s' : Set (ULift.{w', w} M)) (hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ),
    ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
obtain ⟨s', hs'⟩ := Cardinal.le_mk_iff_exists_set.1 h4

Premises used: Cardinal.le_mk_iff_exists_set, Iff.mp