no goals
L : Language
T : Theory L
α : Type w
n : ℕ
h : ∃ M, Infinite ↑M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (#↑N) = κ
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⟩
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI this : Infinite ↑M
⊢ ∃ N, (#↑N) = κ
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI : Infinite ↑M
⊢ ∃ N, (#↑N) = κ
haveI := MI
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)
case intro
L : Language
T : Theory L
α : Type w
n : ℕ
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
M : ModelType T
MI this : Infinite ↑M
⊢ ∃ N, (#↑N) = κ
obtain ⟨N, hN, rfl⟩ := exists_elementarilyEquivalent_card_eq L M κ h1 h2
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)
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)
haveI : Nonempty N := hN.nonempty
no goals
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)
exact ⟨hN.theory_model.bundled, rfl⟩