-- Mathlib/ModelTheory/Satisfiability.lean
theorem exists_elementaryEmbedding_card_eq_of_le (M : Type w') [L.Structure M] [Nonempty M]
    (κ : Cardinal.{w}) (h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ)
    (h3 : lift.{w'} κ ≤ Cardinal.lift.{w} #M) :
    ∃ N : Bundled L.Structure, Nonempty (N ↪ₑ[L] M) ∧ #N = κ

Proof state:
case intro.intro
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Tactic:
refine
  ⟨(equivShrink S).bundledInduced L,
    ⟨S.subtype.comp (Equiv.bundledInducedEquiv L _).symm.toElementaryEmbedding⟩,
    lift_inj.1 (_root_.trans ?_ hS)⟩

Result:
case intro.intro
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ lift.{w', w} #↑(Equiv.bundledInduced L (equivShrink ↥S)) = lift.{w, w'} #↥S

Proof state:
case intro.intro
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ lift.{w', w} #↑(Equiv.bundledInduced L (equivShrink ↥S)) = lift.{w, w'} #↥S

Tactic:
simp only [Equiv.bundledInduced_α, lift_mk_shrink']

Result:
no goals

Proof state:
case intro.intro
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Tactic:
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')

Result:
case intro.intro
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
this : Small.{w, w'} ↥S
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Proof state:
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ lift.{w, w'} #↑∅ ≤ lift.{w', w} κ

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ Small.{w, w'} ↥S

Tactic:
rw [← lift_inj.{_, w + 1}, lift_lift, lift_lift] at hS

Result:
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w + 1, w'} #↥S = lift.{max w' (w + 1), w} κ
⊢ Small.{w, w'} ↥S

Proof state:
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Tactic:
obtain ⟨S, _, hS⟩ := exists_elementarySubstructure_card_eq L ∅ κ h1 (by simp) h2 h3

Result:
case intro.intro
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w, w'} #↥S = lift.{w', w} κ
⊢ ∃ N, Nonempty (↑N ↪ₑ[L] M) ∧ #↑N = κ

Proof state:
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Nonempty M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h3 : lift.{w', w} κ ≤ lift.{w, w'} #M
S : L.ElementarySubstructure M
left✝ : ∅ ⊆ ↑S
hS : lift.{w + 1, w'} #↥S = lift.{max w' (w + 1), w} κ
⊢ Small.{w, w'} ↥S

Tactic:
exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ')

Result:
no goals