awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
set set₁ : T.IsSatisfiable
set₂ : T.IsSatisfiable
set₃ :
  let M : Finset (↑T : Type (max u v)) → Type (max u v) := fun (T0 : Finset (↑T : Type (max u v))) ↦
    (↑(Nonempty.some ⋯) : Type (max u v));
  let M' := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M;
  ∀ (h' : M' ⊨ T), T.IsSatisfiable
⊢ T.IsSatisfiable

Tactic:
classical
      set M : Finset T → Type max u v := fun T0 : Finset T =>
        (h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
      let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
      have h' : M' ⊨ T := by
        refine ⟨fun φ hφ => ?_⟩
        rw [Ultraproduct.sentence_realize]
        refine
          Filter.Eventually.filter_mono (Ultrafilter.of_le _)
            (Filter.eventually_atTop.2
              ⟨{⟨φ, hφ⟩}, fun s h' =>
                Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T))
                  ?_⟩)
        simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
          Subtype.exists, exists_and_right, exists_eq_right]
        exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
      exact ⟨ModelType.of T M'⟩

Premises used: Finset.map_subtype_subset, Finset.map, Membership.mem, Nonempty.some, FirstOrder.Language.Theory.ModelType.Carrier, Function.Embedding.subtype
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
inst : Nonempty ι
T : ι → L.Theory
h : Directed (fun (x1 x2 : L.Theory) ↦ x1 ⊆ x2) T
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (i : ι), (T i).IsSatisfiable

Tactic:
⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => ?_⟩

Premises used: Set.subset_iUnion, FirstOrder.Language.Theory.IsSatisfiable.mono, Iff.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
inst : Nonempty ι
T : ι → L.Theory
h : Directed (fun (x1 x2 : L.Theory) ↦ x1 ⊆ x2) T
refine : ∀ (h' : ∀ (i : ι), (T i).IsSatisfiable), IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i) ↔ ∀ (i : ι), (T i).IsSatisfiable

Tactic:
refine ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
inst : Nonempty ι
T : ι → L.Theory
h : Directed (fun (x1 x2 : L.Theory) ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
rw : ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ ⋃ (i : ι), T i → IsSatisfiable (↑T0 : Set L.Sentence)
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]

Premises used: FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, FirstOrder.Language.Theory.IsFinitelySatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
inst : Nonempty ι
T : ι → L.Theory
h : Directed (fun (x1 x2 : L.Theory) ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ ⋃ (i : ι), T i
obtain : ∀ (i : ι) (hi : (↑T0 : Set L.Sentence) ⊆ T i), IsSatisfiable (↑T0 : Set L.Sentence)
⊢ IsSatisfiable (↑T0 : Set L.Sentence)

Tactic:
obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0

Premises used: Directed.exists_mem_subset_of_finset_subset_biUnion
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
inst : Nonempty ι
T : ι → L.Theory
h : Directed (fun (x1 x2 : L.Theory) ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ ⋃ (i : ι), T i
i : ι
hi : (↑T0 : Set L.Sentence) ⊆ T i
⊢ IsSatisfiable (↑T0 : Set L.Sentence)

Tactic:
(h' i).mono hi

Premises used: FirstOrder.Language.Theory.IsSatisfiable.mono
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
ι : Type u_1
inst : Nonempty ι
T : ι → L.Theory
h : Directed (fun (x1 x2 : L.Theory) ↦ x1 ⊆ x2) T
h' : ∀ (i : ι), (T i).IsSatisfiable
T0 : Finset L.Sentence
hT0 : (↑T0 : Set L.Sentence) ⊆ ⋃ (i : ι), T i
i : ι
hi : (↑T0 : Set L.Sentence) ⊆ T i
⊢ IsSatisfiable (↑T0 : Set L.Sentence)

Tactic:
exact (h' i).mono hi

Premises used: FirstOrder.Language.Theory.IsSatisfiable.mono
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : lift.{w', w} #(↑s : Type w) ≤ lift.{w, w'} #M
haveI : ∀ (this : Inhabited M), ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : lift.{w', w} #(↑s : Type w) ≤ lift.{w, w'} #M
this : Inhabited M
rw :
  ∀ (h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)) (this : Inhabited M),
    ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
rw [Cardinal.lift_mk_le'] at h

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s

Tactic:
((LHom.onTheory_model _ _).2 inferInstance).union ?_

Premises used: Iff.mpr, inferInstance, FirstOrder.Language.LHom.onTheory_model, FirstOrder.Language.Theory.Model.union
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
refine : M ⊨ L.distinctConstantsTheory s
⊢ M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s

Tactic:
refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_

Premises used: Iff.mpr, inferInstance, FirstOrder.Language.LHom.onTheory_model, FirstOrder.Language.Theory.Model.union
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
rw : Set.InjOn.{w, w'} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
⊢ M ⊨ L.distinctConstantsTheory s

Tactic:
rw [model_distinctConstantsTheory]

Premises used: FirstOrder.Language.model_distinctConstantsTheory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ Set.InjOn.{w, w'} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s

Tactic:
fun a as b bs ab => ?_

Premises used: Set.InjOn
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
refine :
  ∀ (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
⊢ Set.InjOn.{w, w'} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s

Tactic:
refine fun a as b bs ab => ?_
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
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)
rw : Subtype.mk (p := Membership.mem s) a as = Subtype.mk (p := Membership.mem s) b bs
⊢ a = b

Tactic:
rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]

Premises used: Subtype.coe_mk, Subtype.ext_iff
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
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)
⊢ Subtype.mk (p := Membership.mem s) a as = Subtype.mk (p := Membership.mem s) b bs

Tactic:
h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))

Premises used: Inhabited.default, Nonempty.some, Function.Injective.extend_apply, Subtype.coe_injective, Subtype.mk, Function.Embedding.injective, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
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)
⊢ Subtype.mk (p := Membership.mem s) a as = Subtype.mk (p := Membership.mem s) b bs

Tactic:
exact
      h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))

Premises used: Inhabited.default, Nonempty.some, Function.Injective.extend_apply, Subtype.coe_injective, Subtype.mk, Function.Embedding.injective, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
⊢ M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s := by
    refine ((LHom.onTheory_model _ _).2 inferInstance).union ?_
    rw [model_distinctConstantsTheory]
    refine fun a as b bs ab => ?_
    rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
    exact
      h.some.injective
        ((Subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
          (ab.trans (Subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩)))
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this_2 : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
this : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
Model.isSatisfiable M

Premises used: FirstOrder.Language.Theory.Model.isSatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)
this_1 : Inhabited M
this_2 : Structure.{w, 0, w'} (constantsOn α) M :=
  constantsOn.structure
    (Function.extend (α := (↑s : Type w)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (⇑h.some : (a : (↑s : Type w)) → M)
      default)
this : M ⊨ (L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
exact Model.isSatisfiable M

Premises used: FirstOrder.Language.Theory.Model.isSatisfiable
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
rw :
  ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
rw₁ :
  Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]

Premises used: FirstOrder.Language.Theory.isSatisfiable_directed_union_iff, Set.union_iUnion, FirstOrder.Language.distinctConstantsTheory_eq_iUnion
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))

Tactic:
fun t =>
        isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
          ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
            (aleph0_le_lift.2 (aleph0_le_mk M)))

Premises used: Iff.mpr, Cardinal.lift_le_aleph0, Finset.map, Membership.mem, LT.lt.le, Cardinal.aleph0_le_lift, SetLike.coe, Function.Embedding.subtype, LE.le.trans, FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le, Cardinal.finset_card_lt_aleph0, Cardinal.aleph0_le_mk
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))

Tactic:
exact fun t =>
        isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
          ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
            (aleph0_le_lift.2 (aleph0_le_mk M)))

Premises used: Iff.mpr, Cardinal.lift_le_aleph0, LT.lt.le, Cardinal.aleph0_le_lift, SetLike.coe, LE.le.trans, FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le, Cardinal.finset_card_lt_aleph0, Cardinal.aleph0_le_mk
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
a :
  Monotone (β := L[[α]].Theory) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
⊢ Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)

Tactic:
apply Monotone.directed_le

Premises used: Monotone.directed_le
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ Monotone (β := L[[α]].Theory) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)

Tactic:
monotone_const.union (monotone_distinctConstantsTheory.comp ?_)

Premises used: monotone_const, Monotone.union, Monotone.comp, FirstOrder.Language.monotone_distinctConstantsTheory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
a :
  Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
    (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
⊢ Monotone (β := L[[α]].Theory) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)

Tactic:
refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)

Premises used: monotone_const, Monotone.union, Monotone.comp, FirstOrder.Language.monotone_distinctConstantsTheory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
a :
  Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
    (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' (↑i : Set { x : α // x ∈ s })
⊢ Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
    (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)

Tactic:
simp only [Finset.coe_map, Function.Embedding.coe_subtype]

Premises used: Function.Embedding.coe_subtype, Finset.coe_map
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
    (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' (↑i : Set { x : α // x ∈ s })

Tactic:
Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2

Premises used: Iff.mpr, Set.Mem, setOf, Monotone.comp, Set.image, Set.monotone_image, Finset.coe_subset
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
⊢ Monotone (β := Set α) fun (i : Finset (↑s : Type w)) ↦
    (fun (a : { x : α // x ∈ s }) ↦ (↑a : α)) '' (↑i : Set { x : α // x ∈ s })

Tactic:
exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2

Premises used: Iff.mpr, Monotone.comp, Set.monotone_image, Finset.coe_subset
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
obtain :
  ∀
    (N :
      ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
        (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)),
    ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))
⊢ ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))

Tactic:
obtain ⟨N⟩ :=
    isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M

Premises used: Set.univ, FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
⊢ ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))

Tactic:
⟨(N.is_model.mono Set.subset_union_left).bundled.reduct _, ?_⟩

Premises used: FirstOrder.Language.Theory.ModelType.is_model, FirstOrder.Language.Theory.ModelType.reduct, Set.subset_union_left, Exists.intro, FirstOrder.Language.Theory.Model.mono, FirstOrder.Language.Theory.Model.bundled
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
refine :
  lift.{max u v w, w} κ ≤
    #(↑(ModelType.reduct (T := T) (L.lhomWithConstants (Quotient.out κ))
            (⋯.bundled (T := LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T))) :
        Type (max (max u v) w))
⊢ ∃ (N : T.ModelType), lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))

Tactic:
refine ⟨(N.is_model.mono Set.subset_union_left).bundled.reduct _, ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
⊢ Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)

Tactic:
haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono Set.subset_union_right
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
N :
  ModelType (L := withConstants.{u, v, w} L (Quotient.out κ))
    (LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T ∪ L.distinctConstantsTheory Set.univ)
this :
  Model (L := withConstants.{u, v, w} L (Quotient.out κ)) (↑N : Type (max (max u v) w))
    (L.distinctConstantsTheory Set.univ)
rw : lift.{max u v w, w} κ ≤ #(↑N : Type (max (max u v) w))
⊢ lift.{max u v w, w} κ ≤
    #(↑(ModelType.reduct (T := T) (L.lhomWithConstants (Quotient.out κ))
            (⋯.bundled (T := LHom.onTheory (L.lhomWithConstants (Quotient.out κ)) T))) :
        Type (max (max u v) w))

Tactic:
rw [ModelType.reduct_Carrier, coe_of]

Premises used: FirstOrder.Language.Theory.coe_of, FirstOrder.Language.Theory.ModelType.reduct_Carrier