case intro
L : Language
κ : Cardinal
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 φ
L : Language
κ : Cardinal
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 φ
obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2
case intro
L : Language
κ : Cardinal
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 φ
case intro
L : Language
κ : Cardinal
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 φ
rw [Theory.models_sentence_iff, Theory.models_sentence_iff]
case intro
L : Language
κ : Cardinal
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
case intro
L : Language
κ : Cardinal
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 φ
by_contra con
case intro
L : Language
κ : Cardinal
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
case intro
L : Language
κ : Cardinal
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
push_neg  at con
case intro.intro.intro.intro
L : Language
κ : Cardinal
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
case intro
L : Language
κ : Cardinal
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
obtain ⟨⟨MF, hMF⟩, MT, hMT⟩ := con
case intro.intro.intro.intro
L : Language
κ : Cardinal
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
case intro.intro.intro.intro
L : Language
κ : Cardinal
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
rw [Sentence.realize_not, Classical.not_not] at hMT
case intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
case intro.intro.intro.intro
L : Language
κ : Cardinal
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
refine' hMF _
case intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
case intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
haveI := hT MT
case intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
case intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
haveI := hT MF
case intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
case intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
obtain ⟨NT, MNT, hNT⟩ := exists_elementarilyEquivalent_card_eq L MT κ h1 h2
case intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
case intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
obtain ⟨NF, MNF, hNF⟩ := exists_elementarilyEquivalent_card_eq L MF κ h1 h2
case intro.intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
case intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
obtain ⟨TF⟩ := h (MNT.toModel T) (MNF.toModel T) hNT hNF
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro
L : Language
κ : Cardinal
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 ⊨ φ
exact
  ((MNT.realize_sentence φ).trans
    ((TF.realize_sentence φ).trans (MNF.realize_sentence φ).symm)).1 hMT