awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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)
rwa : ⊤ ≤ F.dom
⊢ F.dom = ⊤
have rwa₁ : LowerAdjoint.toFun (u := SetLike.coe) (closure L) X ≤ F.dom
Tactic: rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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)
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have dom_top : F.dom = ⊤
Tactic: have dom_top : F.dom = ⊤ := by rwa [← top_le_iff, ← X_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 = ⊤
⊢ F.cod = ⊤
have rwa : ⊤ ≤ F.cod
Tactic: rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 = ⊤
rwa : ⊤ ≤ F.cod
⊢ F.cod = ⊤
have rwa₁ : LowerAdjoint.toFun (u := SetLike.coe) (closure L) Y ≤ F.cod
Tactic: rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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 = ⊤
⊢ ∃ (f : M ≃[L] N), (↑g : M ≃ₚ[L] N) ≤ f.toEmbedding.toPartialEquiv
have cod_top : F.cod = ⊤
Tactic: have cod_top : F.cod = ⊤ := by rwa [← top_le_iff, ← Y_gen, Substructure.closure_le]
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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
have refine : (↑g : M ≃ₚ[L] N) ≤ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv
Tactic: refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 = ⊤
⊢ (↑g : M ≃ₚ[L] N) ≤ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv
have h : (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv = partialEquivLimit S
Tactic: convert! le_partialEquivLimit S 0
-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
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 = ⊤
⊢ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv = partialEquivLimit S
have h : (toEmbeddingOfEqTop dom_top).toPartialEquiv = partialEquivLimit S
Tactic: rw [toEquivOfEqTop_toEmbedding]
-- Lean 4 proof step from Mathlib.ModelTheory.Quotients (goal)
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice (α := fun (a : Fin n) ↦ M) fun (i : Fin n) ↦ ⟦x i⟧) = ⟦funMap f x⟧
have rw : Quotient.map (funMap f) sorry ⟦x⟧ = ⟦funMap f x⟧
Tactic: rw [Quotient.finChoice_eq, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.ModelTheory.Quotients (goal)
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⟧
⊢ Quotient.map (funMap f) ⋯ (Quotient.finChoice (α := fun (a : Fin n) ↦ M) fun (i : Fin n) ↦ ⟦x i⟧) = ⟦funMap f x⟧
have rw₁ : ⟦funMap f x⟧ = ⟦funMap f x⟧
Tactic: rw [Quotient.finChoice_eq, Quotient.map_mk]
-- Lean 4 proof step from Mathlib.ModelTheory.Quotients (goal)
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
n : ℕ
r : L.Relations n
x : Fin n → M
⊢ 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
have rw : Quotient.lift (s := piSetoid (α := fun (a : Fin n) ↦ M)) (RelMap r) sorry ⟦x⟧ ↔ RelMap r x
Tactic: rw [Quotient.finChoice_eq, Quotient.lift_mk]
-- Lean 4 proof step from Mathlib.ModelTheory.Quotients (goal)
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
⊢ 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
have rw₁ : RelMap r x ↔ RelMap r x
Tactic: rw [Quotient.finChoice_eq, Quotient.lift_mk]
-- Lean 4 proof step from Mathlib.ModelTheory.Quotients (goal)
Goal:
L : Language
M : Type u_1
s : Setoid M
ps : L.Prestructure s
β : Type u_2
t : L.Term β
x : β → M
⊢ realize (fun (i : β) ↦ ⟦x i⟧) t = ⟦realize x t⟧
have var : ∀ (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: induction t with
  | var => rfl
  | func _ _ ih => simp only [ih, funMap_quotient_mk', Term.realize]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Quotients (goal)
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)⟧
⊢ realize (fun (i : β) ↦ ⟦x i⟧) t = ⟦realize x t⟧
have 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⟧) (func _f _ts) = ⟦realize x (func _f _ts)⟧
Tactic: induction t with
  | var => rfl
  | func _ _ ih => simp only [ih, funMap_quotient_mk', Term.realize]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable
have refine : ∀ (h' : T.IsSatisfiable), (φ.onTheory T).IsSatisfiable
Tactic: refine ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
h' : T.IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable
have haveI : ∀ (this : Inhabited (↑(Nonempty.some h') : Type (max u v))), (φ.onTheory T).IsSatisfiable
Tactic: haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable
have refine : ∀ (h' : T.IsSatisfiable), (φ.onTheory 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)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
L' : Language
φ : L →ᴸ L'
h : φ.Injective
refine : ∀ (h' : T.IsSatisfiable), (φ.onTheory T).IsSatisfiable
⊢ (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable
have refine₁ : ∀ (h' : T.IsSatisfiable) (this : Inhabited (↑(Nonempty.some h') : Type (max u v))), (φ.onTheory 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)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
have refine : ∀ (φ : L.Sentence) (hφ : φ ∈ T), M' ⊨ φ
Tactic: refine ⟨fun φ hφ => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ M' ⊨ φ
have rw : ∀ᶠ (a : Finset (↑T : Type (max u v))) in (↑(Ultrafilter.of Filter.atTop) : Filter (Finset (↑T : Type (max u v)))),
  M a ⊨ φ
Tactic: rw [Ultraproduct.sentence_realize]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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 ⊨ φ
have 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)
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))
                  ?_⟩)
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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φ}
⊢ φ ∈ (↑(Finset.map (Function.Embedding.subtype fun (x : L.Sentence) ↦ x ∈ T) s) : Set L.Sentence)
have simp : ∃ (x : φ ∈ T), Subtype.mk (p := fun (a : L.Sentence) ↦ a ∈ T) φ sorry ∈ s
Tactic: simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe,
          Subtype.exists, exists_and_right, exists_eq_right]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (hypothesis)
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
⊢ T.IsSatisfiable
have h' : 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 _)⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
Goal:
L : Language
T : L.Theory
h : T.IsFinitelySatisfiable
set set₁ : T.IsSatisfiable
set₂ : T.IsSatisfiable
⊢ T.IsSatisfiable
have set₃ : let M : Finset (↑T : Type (max u v)) → Type (max u v) := fun (T0 : Finset (↑T : Type (max u v))) ↦
  (↑(Nonempty.some sorry) : 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
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'⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
have refine : ∀ (h' : ∀ (i : ι), (T i).IsSatisfiable), IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
Tactic: refine ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ IsSatisfiable.{u, v} (L := L) (⋃ (i : ι), T i)
have rw : ∀ (T0 : Finset L.Sentence), (↑T0 : Set L.Sentence) ⊆ ⋃ (i : ι), T i → IsSatisfiable (↑T0 : Set L.Sentence)
Tactic: rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ IsSatisfiable (↑T0 : Set L.Sentence)
have obtain : ∀ (i : ι) (hi : (↑T0 : Set L.Sentence) ⊆ T i), IsSatisfiable (↑T0 : Set L.Sentence)
Tactic: obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have haveI : ∀ (this : Inhabited M), ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
Tactic: haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
-- Lean 4 proof step from Mathlib.ModelTheory.Satisfiability (goal)
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
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
have rw : ∀ (h : Nonempty (Function.Embedding.{w + 1, w' + 1} (↑s : Type w) M)) (this : Inhabited M),
  ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable
Tactic: rw [Cardinal.lift_mk_le'] at h
Cleared hypotheses: h, this