awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
h_3 : Y ⊆ (↑F.cod : Set N)
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv

Tactic:
⟨toEquivOfEqTop dom_top cod_top, ?_⟩

Premises used: FirstOrder.Language.PartialEquiv.toEquivOfEqTop, Exists.intro
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
h_3 : Y ⊆ (↑F.cod : Set N)
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
refine : (↑g : M ≃ₚ[L] N) ≤ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv

Tactic:
refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
h_3 : Y ⊆ (↑F.cod : Set N)
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ (S : (a : ℕ) → M ≃ₚ[L] N) 0 ≤ partialEquivLimit S

Tactic:
le_partialEquivLimit S 0

Premises used: OfNat.ofNat, FirstOrder.Language.DirectLimit.le_partialEquivLimit
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h_1 : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_2 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_3 : X ⊆ (↑F.dom : Set M)
h_4 : Y ⊆ (↑F.cod : Set N)
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
h : (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv = partialEquivLimit S
⊢ (↑g : M ≃ₚ[L] N) ≤ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv

Tactic:
convert! le_partialEquivLimit S 0

Premises used: OfNat.ofNat, FirstOrder.Language.DirectLimit.le_partialEquivLimit
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h_1 : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_2 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_3 : X ⊆ (↑F.dom : Set M)
h_4 : Y ⊆ (↑F.cod : Set N)
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
h : (toEmbeddingOfEqTop dom_top).toPartialEquiv = partialEquivLimit S
⊢ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv = partialEquivLimit S

Tactic:
rw [toEquivOfEqTop_toEmbedding]

Premises used: FirstOrder.Language.PartialEquiv.toEquivOfEqTop_toEmbedding
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : Eq (α := L.Substructure M) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) X) ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : Eq (α := L.Substructure N) (LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y) ⊤
h : Countable.{w + 1} (↑X : Type w)
x : Encodable (↑X : Type w)
h_1 : Countable.{w' + 1} (↑Y : Type w')
x_1 : Encodable (↑Y : Type w')
D : Sum.{w, w'} (↑X : Type w) (↑Y : Type w') → Order.Cofinal (L.FGEquiv M N) :=
  fun (p : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦
    Sum.recOn (motive := fun (x : Sum.{w, w'} (↑X : Type w) (↑Y : Type w')) ↦ Order.Cofinal (L.FGEquiv M N)) p
      (fun (x : (↑X : Type w)) ↦ ext_dom.definedAtLeft (↑x : M)) fun (y : (↑Y : Type w')) ↦
      ext_cod.definedAtRight (↑y : N)
S : ℕ →o M ≃ₚ[L] N :=
  { toFun := Subtype.val (p := fun (f : M ≃ₚ[L] N) ↦ f.dom.FG) ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
h_2 : X ⊆ (↑F.dom : Set M)
h_3 : Y ⊆ (↑F.cod : Set N)
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ (toEmbeddingOfEqTop dom_top).toPartialEquiv = partialEquivLimit S

Tactic:
apply Embedding.toPartialEquiv_toEmbedding

Premises used: FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding
-- Module: Mathlib.ModelTheory.Quotients
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
rw : Quotient.map (funMap f) ⋯ ⟦x⟧ = ⟦funMap f x⟧
rw₁ rw₂ : ⟦funMap f x⟧ = ⟦funMap f x⟧
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice (α := fun (a : Fin n) ↦ M) fun (i : Fin n) ↦ ⟦x i⟧) = ⟦funMap f x⟧

Tactic:
rw [Quotient.finChoice_eq, Quotient.map_mk]

Premises used: Quotient.map_mk, Quotient.finChoice_eq
-- Module: Mathlib.ModelTheory.Quotients
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
rw : Quotient.lift (s := piSetoid (α := fun (a : Fin n) ↦ M)) (RelMap r) ⋯ ⟦x⟧ ↔ RelMap r x
rw₁ rw₂ : RelMap r x ↔ RelMap r x
⊢ Quotient.lift.{u_1 + 1, 1} (α := Fin n → M) (s := piSetoid (α := fun (a : Fin n) ↦ M)) (RelMap r) ⋯
      (Quotient.finChoice (α := fun (a : Fin n) ↦ M) fun (i : Fin n) ↦ ⟦x i⟧) ↔
    RelMap r x

Tactic:
rw [Quotient.finChoice_eq, Quotient.lift_mk]

Premises used: Quotient.lift_mk, Quotient.finChoice_eq
-- Module: Mathlib.ModelTheory.Quotients
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
a : β
⊢ realize.{u_3, u_4, u_1, u_2} (L := L) (fun (i : β) ↦ ⟦x i⟧) (var a) =
    ⟦realize.{u_3, u_4, u_1, u_2} (L := L) x (var a)⟧

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Quotients
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
x : β → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term β
ih : ∀ (a : Fin l), realize (fun (i : β) ↦ ⟦x i⟧) (_ts a) = ⟦realize x (_ts a)⟧
⊢ realize (fun (i : β) ↦ ⟦x i⟧) (func _f _ts) = ⟦realize x (func _f _ts)⟧

Tactic:
simp only [ih, funMap_quotient_mk', Term.realize]

Premises used: FirstOrder.Language.funMap_quotient_mk', FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Quotients
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
t : L.Term β
x : β → M
var :
  ∀ (a : β),
    realize.{u_3, u_4, u_1, u_2} (L := L) (fun (i : β) ↦ ⟦x i⟧) (Language.var a) =
      ⟦realize.{u_3, u_4, u_1, u_2} (L := L) x (Language.var a)⟧
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term β)
    (ih : ∀ (a : Fin l), realize (fun (i : β) ↦ ⟦x i⟧) (_ts a) = ⟦realize x (_ts a)⟧),
    realize (fun (i : β) ↦ ⟦x i⟧) (Language.func _f _ts) = ⟦realize x (Language.func _f _ts)⟧
⊢ realize (fun (i : β) ↦ ⟦x i⟧) t = ⟦realize x t⟧

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp only [ih, funMap_quotient_mk', Term.realize]

Premises used: FirstOrder.Language.funMap_quotient_mk', FirstOrder.Language.Term.func, FirstOrder.Language.Term.var, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
⊢ T.IsSatisfiable

Tactic:
⟨((⊥ : Substructure _ (ModelType.of T M)).elementarySkolem₁Reduct.toModel T).shrink⟩

Premises used: FirstOrder.Language.ElementarySubstructure.toModel, FirstOrder.Language.Theory.IsSatisfiable, Bot.bot, Nonempty.intro, FirstOrder.Language.Theory.ModelType.shrink, FirstOrder.Language.Substructure.elementarySkolem₁Reduct
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T T' : L.Theory
h : T'.IsSatisfiable
hs : T ⊆ T'
⊢ T.IsSatisfiable

Tactic:
⟨(Theory.Model.mono (ModelType.is_model h.some) hs).bundled⟩

Premises used: FirstOrder.Language.Theory.IsSatisfiable, FirstOrder.Language.Theory.ModelType.is_model, Nonempty.some, Nonempty.intro, FirstOrder.Language.Theory.Model.mono, FirstOrder.Language.Theory.Model.bundled
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
⊢ IsSatisfiable.{u, v} (L := L) ∅

Tactic:
⟨default⟩

Premises used: Inhabited.default, FirstOrder.Language.Theory.IsSatisfiable, Nonempty.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : (φ.onTheory T).IsSatisfiable
⊢ T.IsSatisfiable

Tactic:
Model.isSatisfiable (h.some.reduct φ)

Premises used: Nonempty.some, FirstOrder.Language.Theory.ModelType.reduct, FirstOrder.Language.Theory.Model.isSatisfiable, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Tactic:
⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩

Premises used: Iff.intro, FirstOrder.Language.Theory.isSatisfiable_of_isSatisfiable_onTheory
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
refine : ∀ (h' : T.IsSatisfiable), (φ.onTheory T).IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Tactic:
refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
haveI : ∀ (this : Inhabited (↑(Nonempty.some h') : Type (max u v))), (φ.onTheory T).IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable

Tactic:
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
this : Inhabited (↑(Nonempty.some h') : Type (max u v))
⊢ (φ.onTheory T).IsSatisfiable

Tactic:
Model.isSatisfiable (h'.some.defaultExpansion h)

Premises used: FirstOrder.Language.Theory.ModelType.defaultExpansion, Nonempty.some, FirstOrder.Language.Theory.Model.isSatisfiable, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
this : Inhabited (↑(Nonempty.some h') : Type (max u v))
⊢ (φ.onTheory T).IsSatisfiable

Tactic:
exact Model.isSatisfiable (h'.some.defaultExpansion h)

Premises used: FirstOrder.Language.Theory.ModelType.defaultExpansion, Nonempty.some, FirstOrder.Language.Theory.Model.isSatisfiable, FirstOrder.Language.Theory.ModelType.Carrier
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
refine : ∀ (h' : T.IsSatisfiable), (φ.onTheory T).IsSatisfiable
refine₁ :
  ∀ (h' : T.IsSatisfiable) (this : Inhabited (↑(Nonempty.some h') : Type (max u v))), (φ.onTheory T).IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

Tactic:
classical
    refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩
    haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
    exact Model.isSatisfiable (h'.some.defaultExpansion h)
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsSatisfiable
⊢ T.IsFinitelySatisfiable

Tactic:
fun _ => h.mono

Premises used: FirstOrder.Language.Theory.IsFinitelySatisfiable, FirstOrder.Language.Theory.IsSatisfiable.mono
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
⊢ M' ⊨ T

Tactic:
⟨fun φ hφ => ?_⟩

Premises used: FirstOrder.Language.Theory.Model.mk
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
refine : ∀ (φ : L.Sentence) (hφ : φ ∈ T), M' ⊨ φ
⊢ M' ⊨ T

Tactic:
refine ⟨fun φ hφ => ?_⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
φ : L.Sentence
hφ : φ ∈ T
rw :
  ∀ᶠ (a : Finset (↑T : Type (max u v))) in (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))),
    M a ⊨ φ
⊢ M' ⊨ φ

Tactic:
rw [Ultraproduct.sentence_realize]

Premises used: FirstOrder.Language.Ultraproduct.sentence_realize
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
φ : L.Sentence
hφ : φ ∈ T
⊢ ∀ᶠ (a : Finset (↑T : Type (max u v))) in (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))),
    M a ⊨ φ

Tactic:
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))
                  ?_⟩)

Premises used: Iff.mpr, Filter.Eventually.filter_mono, Ultrafilter.of_le, Exists.intro, Filter.eventually_atTop, Singleton.singleton, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
φ : L.Sentence
hφ : φ ∈ T
fun :
  ∀ (s : Finset (↑T : Type (max u v))) (h' : s ≥ {Subtype.mk (p := fun (x : L.Sentence) ↦ x ∈ T) φ hφ}),
    φ ∈ (↑(Finset.map (Function.Embedding.subtype fun (x : L.Sentence) ↦ x ∈ T) s) : Set L.Sentence)
⊢ ∀ᶠ (a : Finset (↑T : Type (max u v))) in (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))),
    M a ⊨ φ

Tactic:
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))
                  ?_⟩)

Premises used: Iff.mpr, Filter.Eventually.filter_mono, Ultrafilter.of_le, Exists.intro, Filter.eventually_atTop, Singleton.singleton, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
φ : L.Sentence
hφ : φ ∈ T
s : Finset (↑T : Type (max u v))
h' : s ≥ {Subtype.mk (p := fun (x : L.Sentence) ↦ x ∈ T) φ hφ}
simp : ∃ (x : φ ∈ T), Subtype.mk (p := fun (a : L.Sentence) ↦ a ∈ T) φ ⋯ ∈ s
⊢ φ ∈ (↑(Finset.map (Function.Embedding.subtype fun (x : L.Sentence) ↦ x ∈ T) s) : Set L.Sentence)

Tactic:
simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
          Subtype.exists, exists_and_right, exists_eq_right]

Premises used: Set.mem_image, Function.Embedding.coe_subtype, Subtype.exists, exists_eq_right, exists_and_right, Finset.coe_map, Finset.mem_coe
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
φ : L.Sentence
hφ : φ ∈ T
s : Finset (↑T : Type (max u v))
h' : s ≥ {Subtype.mk (p := fun (x : L.Sentence) ↦ x ∈ T) φ hφ}
⊢ ∃ (x : φ ∈ T), Subtype.mk (p := fun (a : L.Sentence) ↦ a ∈ T) φ ⋯ ∈ s

Tactic:
⟨hφ, h' (Finset.mem_singleton_self _)⟩

Premises used: Finset.mem_singleton_self, Exists.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
φ : L.Sentence
hφ : φ ∈ T
s : Finset (↑T : Type (max u v))
h' : s ≥ {Subtype.mk (p := fun (x : L.Sentence) ↦ x ∈ T) φ hφ}
⊢ ∃ (x : φ ∈ T), Subtype.mk (p := fun (a : L.Sentence) ↦ a ∈ T) φ ⋯ ∈ s

Tactic:
exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
⊢ M' ⊨ T

Tactic:
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 _)⟩
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
h' : M' ⊨ T
⊢ T.IsSatisfiable

Tactic:
⟨ModelType.of T M'⟩

Premises used: FirstOrder.Language.Theory.IsSatisfiable, FirstOrder.Language.Theory.ModelType.of, Nonempty.intro
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
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))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))) M
h' : M' ⊨ T
⊢ T.IsSatisfiable

Tactic:
exact ⟨ModelType.of T M'⟩