case inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
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
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift (#M)
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
cases le_or_gt (lift.{w'} κ) (Cardinal.lift.{w} (#M))
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift (#M)
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
case inl
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
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
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift (#M)
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
case inl h =>
  obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
  exact ⟨N, Or.inl hN1, hN2⟩
no goals
case inr
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h✝ : lift κ > lift (#M)
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
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⟩
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
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) = κ
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ ≤ lift (#M)
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_le L M κ h1 h2 h
no goals
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
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) = κ
exact ⟨N, Or.inl hN1, hN2⟩
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
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) = κ
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h : lift κ > lift (#M)
⊢ ∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ (#↑N) = κ
obtain ⟨N, hN1, hN2⟩ := exists_elementaryEmbedding_card_eq_of_ge L M κ h2 (le_of_lt h)
no goals
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝ : Structure L M
iM : Infinite M
κ : Cardinal
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) = κ
exact ⟨N, Or.inr hN1, hN2⟩