case intro.intro.inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : (#↑N) = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ (#↑N) = κ

case intro.intro.inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : (#↑N) = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ (#↑N) = κ
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (M ≅[L] ↑N) ∧ (#↑N) = κ
obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2
no goals
case intro.intro.inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : (#↑N) = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ (#↑N) = κ
exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩
no goals
case intro.intro.inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
N : Bundled (Structure L)
hNκ : (#↑N) = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ (#↑N) = κ
exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩