case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
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) = κ
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ (#↑N) = κ
obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
this : Small { x // x ∈ S }
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ (#↑N) = κ
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
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) = κ
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')
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
this : Small { x // x ∈ S }
⊢ lift (#↑(Equiv.bundledInduced L (equivShrink { x // x ∈ S }))) = lift (#{ x // x ∈ S })
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
this : Small { x // x ∈ S }
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ (#↑N) = κ
refine'
  ⟨(equivShrink S).bundledInduced L,
    ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
    lift_inj.1 (_root_.trans _ hS)⟩
no goals
case intro.intro
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
this : Small { x // x ∈ S }
⊢ lift (#↑(Equiv.bundledInduced L (equivShrink { x // x ∈ S }))) = lift (#{ x // x ∈ S })
simp only [Equiv.bundledInduced_α, lift_mk_shrink']
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
⊢ lift (#↑∅) ≤ lift κ
simp
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
⊢ Small { x // x ∈ S }
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
⊢ Small { x // x ∈ S }
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
M : Type w'
inst✝¹ : Structure L M
inst✝ : Nonempty M
κ : Cardinal
h1 : ℵ₀ ≤ κ
h2 : lift (card L) ≤ lift κ
h3 : lift κ ≤ lift (#M)
S : ElementarySubstructure L M
left✝ : ∅ ⊆ ↑S
hS : lift (#{ x // x ∈ S }) = lift κ
⊢ Small { x // x ∈ S }
exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')