[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
⊢ IsSatisfiable (LHom.onTheory φ T) ↔ IsSatisfiable T
[PROOFSTEP]
classical
refine' ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => _⟩
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
exact Model.isSatisfiable (h'.some.defaultExpansion h)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
⊢ IsSatisfiable (LHom.onTheory φ T) ↔ IsSatisfiable T
[PROOFSTEP]
refine' ⟨isSatisfiable_of_isSatisfiable_onTheory φ, fun h' => _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
h' : IsSatisfiable T
⊢ IsSatisfiable (LHom.onTheory φ T)
[PROOFSTEP]
haveI : Inhabited h'.some := Classical.inhabited_of_nonempty'
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
T' : Theory L
L' : Language
φ : L →ᴸ L'
h : LHom.Injective φ
h' : IsSatisfiable T
this : Inhabited ↑(Nonempty.some h')
⊢ IsSatisfiable (LHom.onTheory φ T)
[PROOFSTEP]
exact Model.isSatisfiable (h'.some.defaultExpansion h)
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
⊢ IsSatisfiable T
[PROOFSTEP]
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,
    Subtype.coe_mk, exists_and_right, exists_eq_right]
  exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
exact ⟨ModelType.of T M'⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
⊢ IsSatisfiable T
[PROOFSTEP]
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
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
⊢ IsSatisfiable T
[PROOFSTEP]
let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
⊢ IsSatisfiable T
[PROOFSTEP]
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,
    Subtype.coe_mk, exists_and_right, exists_eq_right]
  exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
⊢ M' ⊨ T
[PROOFSTEP]
refine' ⟨fun φ hφ => _⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
⊢ M' ⊨ φ
[PROOFSTEP]
rw [Ultraproduct.sentence_realize]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
⊢ ∀ᶠ (a : Finset ↑T) in ↑(Ultrafilter.of Filter.atTop), M a ⊨ φ
[PROOFSTEP]
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)) _⟩)
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {{ val := φ, property := hφ }}
⊢ φ ∈ ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) s)
[PROOFSTEP]
simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe, Subtype.exists,
  Subtype.coe_mk, exists_and_right, exists_eq_right]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
φ : Sentence L
hφ : φ ∈ T
s : Finset ↑T
h' : s ≥ {{ val := φ, property := hφ }}
⊢ ∃ x, { val := φ, property := (_ : φ ∈ T) } ∈ s
[PROOFSTEP]
exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
h : IsFinitelySatisfiable T
M : Finset ↑T → Type (max u v) :=
  fun T0 => ↑(Nonempty.some (_ : IsSatisfiable ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ T) T0)))
M' : Type (max u v) := Filter.Product (↑(Ultrafilter.of Filter.atTop)) M
h' : M' ⊨ T
⊢ IsSatisfiable T
[PROOFSTEP]
exact ⟨ModelType.of T M'⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (i : ι), IsSatisfiable (T i)
[PROOFSTEP]
refine' ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => _⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
[PROOFSTEP]
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ ⋃ (i : ι), T i → IsSatisfiable ↑T0
[PROOFSTEP]
intro T0 hT0
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑T0
[PROOFSTEP]
obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
i : ι
hi : ↑T0 ⊆ T i
⊢ IsSatisfiable ↑T0
[PROOFSTEP]
exact (h' i).mono hi
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : lift #↑s ≤ lift #M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : lift #↑s ≤ lift #M
this : Inhabited M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
rw [Cardinal.lift_mk_le'] at h 
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this : Inhabited M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
letI : (constantsOn α).Structure M := constantsOn.structure (Function.extend (↑) h.some default)
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
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⟩)))
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ M ⊨ LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s
[PROOFSTEP]
refine' ((LHom.onTheory_model _ _).2 inferInstance).union _
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ M ⊨ distinctConstantsTheory L s
[PROOFSTEP]
rw [model_distinctConstantsTheory]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
⊢ Set.InjOn (fun i => ↑(Language.con L i)) s
[PROOFSTEP]
refine' fun a as b bs ab => _
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(Language.con L i)) a = (fun i => ↑(Language.con L i)) b
⊢ a = b
[PROOFSTEP]
rw [← Subtype.coe_mk a as, ← Subtype.coe_mk b bs, ← Subtype.ext_iff]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i => ↑(Language.con L i)) a = (fun i => ↑(Language.con L i)) b
⊢ { val := a, property := as } = { val := b, property := bs }
[PROOFSTEP]
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⟩)))
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : Structure L M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝¹ : Inhabited M
this✝ : Structure (constantsOn α) M := constantsOn.structure (Function.extend Subtype.val (↑(Nonempty.some h)) default)
this : M ⊨ LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
exact Model.isSatisfiable M
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
classical
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
·
  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)))
· apply Monotone.directed_le
  refine' monotone_const.union (monotone_distinctConstantsTheory.comp _)
  simp only [Finset.coe_map, Function.Embedding.coe_subtype]
  exact
    Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s)) Set.monotone_image fun _ _ =>
      Finset.coe_subset.2
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
[PROOFSTEP]
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∀ (i : Finset ↑s),
    IsSatisfiable
      (LHom.onTheory (lhomWithConstants L α) T ∪
        distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i))
[PROOFSTEP]
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)))
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
apply Monotone.directed_le
[GOAL]
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
refine' monotone_const.union (monotone_distinctConstantsTheory.comp _)
[GOAL]
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
[PROOFSTEP]
simp only [Finset.coe_map, Function.Embedding.coe_subtype]
[GOAL]
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => (fun a => ↑a) '' ↑i
[PROOFSTEP]
exact
  Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s)) Set.monotone_image fun _ _ =>
    Finset.coe_subset.2
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∃ N, lift κ ≤ #↑N
[PROOFSTEP]
obtain ⟨N⟩ := isSatisfiable_union_distinctConstantsTheory_of_infinite T (Set.univ : Set κ.out) M
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ ∃ N, lift κ ≤ #↑N
[PROOFSTEP]
refine' ⟨(N.is_model.mono (Set.subset_union_left _ _)).bundled.reduct _, _⟩
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
⊢ lift κ ≤
    #↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T)))
[PROOFSTEP]
haveI : N ⊨ distinctConstantsTheory _ _ := N.is_model.mono (Set.subset_union_right _ _)
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤
    #↑(ModelType.reduct (lhomWithConstants L (Quotient.out κ))
          (Model.bundled (_ : ↑N ⊨ LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T)))
[PROOFSTEP]
rw [ModelType.reduct_Carrier, coe_of]
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift κ ≤ #↑N
[PROOFSTEP]
refine' _root_.trans (lift_le.2 (le_of_eq (Cardinal.mk_out κ).symm)) _
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift #(Quotient.out κ) ≤ #↑N
[PROOFSTEP]
rw [← mk_univ]
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift #↑Set.univ ≤ #↑N
[PROOFSTEP]
refine' (card_le_of_model_distinctConstantsTheory L Set.univ N).trans (lift_le.{max u v w}.1 _)
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
κ : Cardinal.{w}
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ModelType (LHom.onTheory (lhomWithConstants L (Quotient.out κ)) T ∪ distinctConstantsTheory L Set.univ)
this : ↑N ⊨ distinctConstantsTheory L Set.univ
⊢ lift (lift #↑N) ≤ lift #↑N
[PROOFSTEP]
rw [lift_lift]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
[PROOFSTEP]
classical
refine' ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _), fun h => _⟩
rw [isSatisfiable_iff_isFinitelySatisfiable]
intro s hs
rw [Set.iUnion_eq_iUnion_finset] at hs 
obtain ⟨t, ht⟩ :=
  Directed.exists_mem_subset_of_finset_subset_biUnion
    (by
      exact
        Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
          Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩)
    hs
exact (h t).mono ht
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
[PROOFSTEP]
refine' ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _), fun h => _⟩
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
[PROOFSTEP]
rw [isSatisfiable_iff_isFinitelySatisfiable]
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsFinitelySatisfiable (⋃ (i : ι), T i)
[PROOFSTEP]
intro s hs
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑s
[PROOFSTEP]
rw [Set.iUnion_eq_iUnion_finset] at hs 
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
[PROOFSTEP]
obtain ⟨t, ht⟩ :=
  Directed.exists_mem_subset_of_finset_subset_biUnion
    (by
      exact
        Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
          Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩)
    hs
[GOAL]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), T i_1
[PROOFSTEP]
exact
  Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
    Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩
[GOAL]
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
[PROOFSTEP]
exact (h t).mono ht
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
⊢ lift #↑∅ ≤ lift κ
[PROOFSTEP]
simp
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
[PROOFSTEP]
have : Small.{w} S := by
  rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS 
  exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
⊢ Small.{w, w'} { x // x ∈ S }
[PROOFSTEP]
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS 
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
⊢ Small.{w, w'} { x // x ∈ S }
[PROOFSTEP]
exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
this : Small.{w, w'} { x // x ∈ S }
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ
[PROOFSTEP]
refine'
  ⟨(equivShrink S).bundledInduced L, ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
    lift_inj.1 (_root_.trans _ hS)⟩
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift #M
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift #{ x // x ∈ S } = lift κ
this : Small.{w, w'} { x // x ∈ S }
⊢ lift #↑(Equiv.bundledInduced L (equivShrink { x // x ∈ S })) = lift #{ x // x ∈ S }
[PROOFSTEP]
simp only [Equiv.bundledInduced_α, lift_mk_shrink']
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N0, hN0⟩ := (L.elementaryDiagram M).exists_large_model_of_infinite_model κ M
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2 
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, ⟨NN0⟩, hN⟩ :=
  exists_elementaryEmbedding_card_eq_of_le (L[[M]]) N0 κ
    (aleph0_le_lift.1 ((aleph0_le_lift.2 (aleph0_le_mk M)).trans h2))
    (by
      simp only [card_withConstants, lift_add, lift_lift]
      rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
      rw [← lift_le.{w'}, lift_lift, lift_lift] at h1 
      exact ⟨h2, h1⟩)
    (hN0.trans (by rw [← lift_umax', lift_id]))
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift (card (L[[M]])) ≤ lift κ
[PROOFSTEP]
simp only [card_withConstants, lift_add, lift_lift]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift (card L) + lift #M ≤ lift κ
[PROOFSTEP]
rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift #M ≤ lift κ ∧ lift (card L) ≤ lift κ
[PROOFSTEP]
rw [← lift_le.{w'}, lift_lift, lift_lift] at h1 
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ lift #M ≤ lift κ ∧ lift (card L) ≤ lift κ
[PROOFSTEP]
exact ⟨h2, h1⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
⊢ #↑N0 ≤ lift #↑N0
[PROOFSTEP]
rw [← lift_umax', lift_id]
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
letI := (lhomWithConstants L M).reduct N
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : Structure L ↑N := LHom.reduct (lhomWithConstants L M) ↑N
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
haveI h : N ⊨ L.elementaryDiagram M := (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : Structure L ↑N := LHom.reduct (lhomWithConstants L M) ↑N
h : ↑N ⊨ elementaryDiagram L M
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
refine' ⟨Bundled.of N, ⟨_⟩, hN⟩
[GOAL]
case intro.intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift (card L) ≤ lift κ
h2 : lift #M ≤ lift κ
N0 : Theory.ModelType (elementaryDiagram L M)
hN0 : lift κ ≤ #↑N0
N : Bundled (Structure (L[[M]]))
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : Structure L ↑N := LHom.reduct (lhomWithConstants L M) ↑N
h : ↑N ⊨ elementaryDiagram L M
⊢ M ↪ₑ[L] ↑(Bundled.of ↑N)
[PROOFSTEP]
apply ElementaryEmbedding.ofModelsElementaryDiagram L M N
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} #M)
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ ≤ lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inl h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
  exact ⟨N, Or.inl hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inl h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
  exact ⟨N, Or.inl hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift #M
N : Bundled (Structure L)
hN1 : Nonempty (↑N ↪ₑ[L] M)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, Or.inl hN1, hN2⟩
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inr h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
  exact ⟨N, Or.inr hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
case inr h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
  exact ⟨N, Or.inr hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift #M
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
[GOAL]
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift #M
N : Bundled (Structure L)
hN1 : Nonempty (M ↪ₑ[L] ↑N)
hN2 : #↑N = κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, Or.inr hN1, hN2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2
[GOAL]
case intro.intro.inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : #↑N = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩
[GOAL]
case intro.intro.inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ
[PROOFSTEP]
exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
cases h with
| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : ∃ M, Infinite ↑M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
cases h with
| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ
[PROOFSTEP]

| intro M MI =>
  haveI := MI
  obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
  haveI : Nonempty N := hN.nonempty
  exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI : Infinite ↑M
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
haveI := MI
[GOAL]
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI this : Infinite ↑M
⊢ ∃ N, #↑N = κ
[PROOFSTEP]
obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
[GOAL]
case intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : ModelType T
MI this : Infinite ↑M
N : Bundled (Structure L)
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift (card L) ≤ lift #↑N
⊢ ∃ N_1, #↑N_1 = #↑N
[PROOFSTEP]
haveI : Nonempty N := hN.nonempty
[GOAL]
case intro.intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : ModelType T
MI this✝ : Infinite ↑M
N : Bundled (Structure L)
hN : ↑M ≅[L] ↑N
h1 : ℵ₀ ≤ #↑N
h2 : lift (card L) ≤ lift #↑N
this : Nonempty ↑N
⊢ ∃ N_1, #↑N_1 = #↑N
[PROOFSTEP]
exact ⟨hN.theory_model.bundled, rfl⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ T ⊨ᵇ φ ↔ ¬IsSatisfiable (T ∪ {Formula.not φ})
[PROOFSTEP]
rw [models_sentence_iff, IsSatisfiable]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (M : ModelType T), ↑M ⊨ φ) ↔ ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
[PROOFSTEP]
refine'
  ⟨fun h1 h2 =>
    (Sentence.realize_not _).1
      (realize_sentence_of_mem (T ∪ {Formula.not φ}) (Set.subset_union_right _ _ (Set.mem_singleton _)))
      (h1 (h2.some.subtheoryModel (Set.subset_union_left _ _))),
    fun h M => _⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬Nonempty (ModelType (T ∪ {Formula.not φ}))
M : ModelType T
⊢ ↑M ⊨ φ
[PROOFSTEP]
contrapose! h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ¬↑M ⊨ φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
[PROOFSTEP]
rw [← Sentence.realize_not] at h 
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (ModelType (T ∪ {Formula.not φ}))
[PROOFSTEP]
refine'
  ⟨{  Carrier := M
      is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => _⟩ }⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ
[PROOFSTEP]
rw [Set.mem_singleton_iff.1 h']
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : ModelType T
h : ↑M ⊨ Formula.not φ
ψ : Sentence L
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ
[PROOFSTEP]
exact h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
[PROOFSTEP]
rw [models_iff_not_satisfiable] at h 
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
h : ¬IsSatisfiable (T ∪ {Formula.not φ})
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ
[PROOFSTEP]
contrapose! h
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ IsSatisfiable (T ∪ {Formula.not φ})
[PROOFSTEP]
have : M ⊨ T ∪ {Formula.not φ} :=
  by
  simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp, Sentence.realize_not]
  rw [← model_iff]
  exact ⟨h, inferInstance⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}
[PROOFSTEP]
simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp, Sentence.realize_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ (a : Sentence L), a ∈ T → M ⊨ a
[PROOFSTEP]
rw [← model_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T
[PROOFSTEP]
exact ⟨h, inferInstance⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ IsSatisfiable (T ∪ {Formula.not φ})
[PROOFSTEP]
exact Model.isSatisfiable M
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ T ⊨ᵇ φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ
[PROOFSTEP]
simp only [models_iff_not_satisfiable]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ ¬IsSatisfiable (T ∪ {Formula.not φ}) ↔ ∃ T0, ↑T0 ⊆ T ∧ ¬IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
rw [← not_iff_not, not_not, isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ¬∃ T0, ↑T0 ⊆ T ∧ ¬IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
push_neg
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
letI := Classical.decEq (Sentence L)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) ↔
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
constructor
[GOAL]
case mp
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0) →
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
intro h T0 hT0
[GOAL]
case mp
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T
⊢ IsSatisfiable (↑T0 ∪ {Formula.not φ})
[PROOFSTEP]
simpa using
  h (T0 ∪ {Formula.not φ})
    (by
      simp only [Finset.coe_union, Finset.coe_singleton]
      exact Set.union_subset_union hT0 (Set.Subset.refl _))
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T
⊢ ↑(T0 ∪ {Formula.not φ}) ⊆ T ∪ {Formula.not φ}
[PROOFSTEP]
simp only [Finset.coe_union, Finset.coe_singleton]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T
⊢ ↑T0 ∪ {Formula.not φ} ⊆ T ∪ {Formula.not φ}
[PROOFSTEP]
exact Set.union_subset_union hT0 (Set.Subset.refl _)
[GOAL]
case mpr
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
⊢ (∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})) →
    ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T ∪ {Formula.not φ} → IsSatisfiable ↑T0
[PROOFSTEP]
intro h T0 hT0
[GOAL]
case mpr
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ IsSatisfiable ↑T0
[PROOFSTEP]
exact IsSatisfiable.mono (h (T0.erase (Formula.not φ)) (by simpa using hT0)) (by simp)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑(Finset.erase T0 (Formula.not φ)) ⊆ T
[PROOFSTEP]
simpa using hT0
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : Sentence L
this : DecidableEq (Sentence L) := Classical.decEq (Sentence L)
h : ∀ (T0 : Finset (Sentence L)), ↑T0 ⊆ T → IsSatisfiable (↑T0 ∪ {Formula.not φ})
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ T ∪ {Formula.not φ}
⊢ ↑T0 ⊆ ↑(Finset.erase T0 (Formula.not φ)) ∪ {Formula.not φ}
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
[PROOFSTEP]
cases' h.2 φ with hφ hφn
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
[PROOFSTEP]
simp only [hφ, not_true, iff_false_iff]
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ
[PROOFSTEP]
rw [models_sentence_iff, not_forall]
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ∃ x, ¬↑x ⊨ Formula.not φ
[PROOFSTEP]
refine' ⟨h.1.some, _⟩
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ¬↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ Formula.not φ
[PROOFSTEP]
simp only [Sentence.realize_not, Classical.not_not]
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ ↑(Nonempty.some (_ : IsSatisfiable T)) ⊨ φ
[PROOFSTEP]
exact models_sentence_iff.1 hφ _
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ T ⊨ᵇ Formula.not φ ↔ ¬T ⊨ᵇ φ
[PROOFSTEP]
simp only [hφn, true_iff_iff]
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
⊢ ¬T ⊨ᵇ φ
[PROOFSTEP]
intro hφ
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : T ⊨ᵇ Formula.not φ
hφ : T ⊨ᵇ φ
⊢ False
[PROOFSTEP]
rw [models_sentence_iff] at *
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
hφn : ∀ (M : ModelType T), ↑M ⊨ Formula.not φ
hφ : ∀ (M : ModelType T), ↑M ⊨ φ
⊢ False
[PROOFSTEP]
exact hφn h.1.some (hφ _)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
[PROOFSTEP]
cases' h.2 φ with hφ hφn
[GOAL]
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφ : T ⊨ᵇ φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
[PROOFSTEP]
exact iff_of_true (hφ.realize_sentence M) hφ
[GOAL]
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsComplete T
φ : Sentence L
M : Type u_1
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
hφn : T ⊨ᵇ Formula.not φ
⊢ M ⊨ φ ↔ T ⊨ᵇ φ
[PROOFSTEP]
exact iff_of_false ((Sentence.realize_not M).1 (hφn.realize_sentence M)) ((h.models_not_iff φ).1 hφn)
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ φ ∈ T
[PROOFSTEP]
refine' (h.mem_or_not_mem φ).resolve_right fun con => _
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False
[PROOFSTEP]
rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ 
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : ¬IsSatisfiable T
con : Formula.not φ ∈ T
⊢ False
[PROOFSTEP]
exact hφ h.1
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : BoundedFormula L α n
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ φ) v xs
[PROOFSTEP]
rw [BoundedFormula.realize_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (ψ ⇔ φ) v xs
[PROOFSTEP]
rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ ψ) v xs
[PROOFSTEP]
exact h M v xs
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
[PROOFSTEP]
have h1' := h1 M v xs
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
[PROOFSTEP]
have h2' := h2 M v xs
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
h2' : BoundedFormula.Realize (ψ ⇔ θ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
[PROOFSTEP]
rw [BoundedFormula.realize_iff] at *
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize ψ v xs
h2' : BoundedFormula.Realize ψ v xs ↔ BoundedFormula.Realize θ v xs
⊢ BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize θ v xs
[PROOFSTEP]
exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ SemanticallyEquivalent T (∀'φ) (∀'ψ)
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_all]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    (∀ (a : ↑M), BoundedFormula.Realize φ v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), BoundedFormula.Realize ψ v (Fin.snoc xs a)
[PROOFSTEP]
exact fun M v xs => forall_congr' fun a => h.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ SemanticallyEquivalent T (∃'φ) (∃'ψ)
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_ex]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α (n + 1)
h : SemanticallyEquivalent T φ ψ
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    (∃ a, BoundedFormula.Realize φ v (Fin.snoc xs a)) ↔ ∃ a, BoundedFormula.Realize ψ v (Fin.snoc xs a)
[PROOFSTEP]
exact fun M v xs => exists_congr fun a => h.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
⊢ SemanticallyEquivalent T (∼φ) ∼ψ
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M), ¬BoundedFormula.Realize φ v xs ↔ ¬BoundedFormula.Realize ψ v xs
[PROOFSTEP]
exact fun M v xs => not_congr h.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ SemanticallyEquivalent T (φ ⟹ φ') (ψ ⟹ ψ')
[PROOFSTEP]
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_imp]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    BoundedFormula.Realize φ v xs → BoundedFormula.Realize φ' v xs ↔
      BoundedFormula.Realize ψ v xs → BoundedFormula.Realize ψ' v xs
[PROOFSTEP]
exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w
inst✝ : Structure L M
φ : Sentence L
⊢ φ ∈ completeTheory L M ∨ Formula.not φ ∈ completeTheory L M
[PROOFSTEP]
simp_rw [completeTheory, Set.mem_setOf_eq, Sentence.Realize, Formula.realize_not, or_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ ∼∼φ) v xs
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⟹ ψ ⇔ ∼φ ⊔ ψ) v xs
[PROOFSTEP]
simp [imp_iff_not_or]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⊔ ψ ⇔ ∼(∼φ ⊓ ∼ψ)) v xs
[PROOFSTEP]
simp [imp_iff_not_or]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⊓ ψ ⇔ ∼(∼φ ⊔ ∼ψ)) v xs
[PROOFSTEP]
simp [and_iff_not_or_not]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ✝ ψ : BoundedFormula L α n
φ : BoundedFormula L α (n + 1)
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (∀'φ ⇔ ∼(∃'∼φ)) v xs
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ✝ ψ : BoundedFormula L α n
φ : BoundedFormula L α (n + 1)
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (∃'φ ⇔ ∼(∀'∼φ)) v xs
[PROOFSTEP]
simp
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ ∀'liftAt 1 n φ) v xs
[PROOFSTEP]
skip
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
M : Theory.ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ ∀'liftAt 1 n φ) v xs
[PROOFSTEP]
rw [realize_iff, realize_all_liftAt_one_self]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
φ : BoundedFormula L α n
M : Theory.ModelType ∅
v : α → ↑M
xs : Fin n → ↑M
⊢ Realize (φ ⇔ toPrenex φ) v xs
[PROOFSTEP]
rw [realize_iff, realize_toPrenex]
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ P φ
[PROOFSTEP]
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
[GOAL]
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
h' : ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
⊢ P φ
[PROOFSTEP]
exact (hse φ.semanticallyEquivalent_toPrenex).2 (h' φ.toPrenex_isPrenex)
[GOAL]
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
[PROOFSTEP]
intro m φ hφ
[GOAL]
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
hφ : IsPrenex φ
⊢ P φ
[PROOFSTEP]
induction' hφ with _ _ hφ _ _ _ hφ _ _ _ hφ
[GOAL]
case h'.of_isQF
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
⊢ P φ✝
[PROOFSTEP]
exact hqf hφ
[GOAL]
case h'.all
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∀'φ✝)
[PROOFSTEP]
exact hall hφ
[GOAL]
case h'.ex
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∃'φ✝)
[PROOFSTEP]
exact hex hφ
[GOAL]
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
[PROOFSTEP]
obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
⊢ T ⊨ᵇ φ ∨ T ⊨ᵇ Formula.not φ
[PROOFSTEP]
rw [Theory.models_sentence_iff, Theory.models_sentence_iff]
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
⊢ (∀ (M : Theory.ModelType T), ↑M ⊨ φ) ∨ ∀ (M : Theory.ModelType T), ↑M ⊨ Formula.not φ
[PROOFSTEP]
by_contra con
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
con : ¬((∀ (M : Theory.ModelType T), ↑M ⊨ φ) ∨ ∀ (M : Theory.ModelType T), ↑M ⊨ Formula.not φ)
⊢ False
[PROOFSTEP]
push_neg at con 
[GOAL]
case intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
con : (∃ M, ¬↑M ⊨ φ) ∧ ∃ M, ¬↑M ⊨ Formula.not φ
⊢ False
[PROOFSTEP]
obtain ⟨⟨MF, hMF⟩, MT, hMT⟩ := con
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ¬↑MT ⊨ Formula.not φ
⊢ False
[PROOFSTEP]
rw [Sentence.realize_not, Classical.not_not] at hMT 
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
⊢ False
[PROOFSTEP]
refine' hMF _
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
⊢ ↑MF ⊨ φ
[PROOFSTEP]
haveI := hT MT
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this : Infinite ↑MT
⊢ ↑MF ⊨ φ
[PROOFSTEP]
haveI := hT MF
[GOAL]
case intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
⊢ ↑MF ⊨ φ
[PROOFSTEP]
obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2
[GOAL]
case intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled (Structure L)
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
⊢ ↑MF ⊨ φ
[PROOFSTEP]
obtain ⟨NF, MNF, hNF⟩ := exists_elementarilyEquivalent_card_eq L MF κ h1 h2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled (Structure L)
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
NF : Bundled (Structure L)
MNF : ↑MF ≅[L] ↑NF
hNF : #↑NF = κ
⊢ ↑MF ⊨ φ
[PROOFSTEP]
obtain ⟨TF⟩ := h (MNT.toModel T) (MNF.toModel T) hNT hNF
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal.{w}
T : Theory L
h : Categorical κ T
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
hS : Theory.IsSatisfiable T
hT : ∀ (M : Theory.ModelType T), Infinite ↑M
φ : Sentence L
w✝ : Theory.ModelType T
h✝ : #↑w✝ = κ
MF : Theory.ModelType T
hMF : ¬↑MF ⊨ φ
MT : Theory.ModelType T
hMT : ↑MT ⊨ φ
this✝ : Infinite ↑MT
this : Infinite ↑MF
NT : Bundled (Structure L)
MNT : ↑MT ≅[L] ↑NT
hNT : #↑NT = κ
NF : Bundled (Structure L)
MNF : ↑MF ≅[L] ↑NF
hNF : #↑NF = κ
TF : ↑(ElementarilyEquivalent.toModel T MNT) ≃[L] ↑(ElementarilyEquivalent.toModel T MNF)
⊢ ↑MF ⊨ φ
[PROOFSTEP]
exact ((MNT.realize_sentence φ).trans ((TF.realize_sentence φ).trans (MNF.realize_sentence φ).symm)).1 hMT
[GOAL]
L : Language
κ : Cardinal.{w}
T✝ : Theory L
T : Theory Language.empty
M N : Theory.ModelType T
hM : #↑M = κ
hN : #↑N = κ
⊢ Nonempty (↑M ≃[Language.empty] ↑N)
[PROOFSTEP]
rw [empty.nonempty_equiv_iff, hM, hN]
[GOAL]
L : Language
κ : Cardinal.{w}
T : Theory L
⊢ lift (card Language.empty) ≤ lift ℵ₀
[PROOFSTEP]
simp
