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

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

Tactic:
obtain ⟨N0, hN0⟩ := (L.elementaryDiagram M).exists_large_model_of_infinite_model κ M

Result:
case intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{w, w'} #M ≤ lift.{w', w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Proof state:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Tactic:
exact ⟨h2, h1⟩

Result:
no goals

Proof state:
case intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
obtain ⟨N, ⟨NN0⟩, hN⟩ :=
  exists_elementaryEmbedding_card_eq_of_le (L[[M]]) N0 κ
    (aleph0_le_lift.1 ((aleph0_le_lift.2 (aleph0_le_mk M)).trans h2))
    (by
      simp only [card_withConstants, lift_add, lift_lift]
      rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]
      rw [← lift_le.{w'}, lift_lift, lift_lift] at h1
      exact ⟨h2, h1⟩)
    (hN0.trans (by rw [← lift_umax, lift_id]))

Result:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Proof state:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max w' w, max u v} L.card + lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ

Tactic:
rw [add_comm, add_eq_max (aleph0_le_lift.2 (infinite_iff.1 iM)), max_le_iff]

Result:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Proof state:
case intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{w, w'} #M ≤ lift.{w', w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
rw [← lift_le.{max u v}, lift_lift, lift_lift] at h2

Result:
case intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Proof state:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ #↑N0 ≤ lift.{w, max (max (max u v) w) w'} #↑N0

Tactic:
rw [← lift_umax, lift_id]

Result:
no goals

Proof state:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Tactic:
rw [← lift_le.{w'}, lift_lift, lift_lift] at h1

Result:
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
⊢ lift.{max (max u v) w, w'} #M ≤ lift.{max (max w' u) v, w} κ ∧
    lift.{max w' w, max u v} L.card ≤ lift.{max (max w' u) v, w} κ

Proof state:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
h : ↑N ⊨ L.elementaryDiagram M
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
refine ⟨Bundled.of N, ⟨?_⟩, hN⟩

Result:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
h : ↑N ⊨ L.elementaryDiagram M
⊢ M ↪ₑ[L] ↑(Bundled.of ↑N)

Proof state:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ

Tactic:
letI := (lhomWithConstants L M).reduct N

Result:
case intro.intro.intro.intro
L : Language
M : Type w'
inst✝ : L.Structure M
iM : Infinite M
κ : Cardinal.{w}
h1 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
h2 : lift.{max w u v, w'} #M ≤ lift.{max w' u v, w} κ
N0 : (L.elementaryDiagram M).ModelType
hN0 : lift.{max (max u w') v w, w} κ ≤ #↑N0
N : Bundled L[[M]].Structure
hN : #↑N = κ
NN0 : ↑N ↪ₑ[L[[M]]] ↑N0
this : L.Structure ↑N := (L.lhomWithConstants M).reduct ↑N
⊢ ∃ N, Nonempty (M ↪ₑ[L] ↑N) ∧ #↑N = κ