-- Mathlib/ModelTheory/Skolem.lean
theorem exists_elementarySubstructure_card_eq (s : Set M) (κ : Cardinal.{w'}) (h1 : ℵ₀ ≤ κ)
    (h2 : Cardinal.lift.{w'} #s ≤ Cardinal.lift.{w} κ)
    (h3 : Cardinal.lift.{w'} L.card ≤ Cardinal.lift.{max u v} κ)
    (h4 : Cardinal.lift.{w} κ ≤ Cardinal.lift.{w'} #M) :
    ∃ S : L.ElementarySubstructure M, s ⊆ S ∧ Cardinal.lift.{w'} #S = Cardinal.lift.{w} κ

Proof state:
case intro.refine_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w, max w' u v} (lift.{w', max u v} L.card) ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')

Tactic:
refine _root_.trans (lift_le.{w}.2 h3) ?_

Result:
case intro.refine_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')

Proof state:
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
rw [← aleph0_le_lift.{_, w}] at h1

Result:
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift.{w, w'} κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Proof state:
case intro.refine_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s') ∧ ℵ₀ ≤ #↑s'

Tactic:
refine ⟨?_, h1⟩

Result:
case intro.refine_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ lift.{max w w', max u v} L.card ≤ lift.{max (max u v) w', w} #↑(⇑Equiv.ulift '' s')

Proof state:
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = #↑s'

Tactic:
refine
  ⟨elementarySkolem₁Reduct (closure (L.sum L.skolem₁) (s ∪ Equiv.ulift '' s')),
    (s.subset_union_left).trans subset_closure, ?_⟩

Result:
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
⊢ lift.{w', w} #↥((closure (L.sum L.skolem₁)).toFun (s ∪ ⇑Equiv.ulift '' s')).elementarySkolem₁Reduct = #↑s'

Proof state:
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift.{max u v, w} #↑(s ∪ ⇑Equiv.ulift '' s')

Tactic:
refine _root_.trans ?_ (lift_le.2 (mk_le_mk_of_subset Set.subset_union_right))

Result:
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
h2 : lift.{w', w} #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift.{w, w'} κ
h : lift.{w', w} #↑(⇑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift.{max u v, w} #↑(⇑Equiv.ulift '' s')