awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ κ
h2 : lift.{w', w} #(↑s : Type w) ≤ 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' : Type (max w w')) = lift.{w, w'} κ
rw :
  ∀ (h1 : ℵ₀ ≤ lift.{w, w'} κ) (h2 : lift.{w', w} #(↑s : Type w) ≤ 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' : Type (max w w')) = lift.{w, w'} κ),
    ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
rw [← aleph0_le_lift.{_, w}] at h1
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
inst : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift.{w, w'} κ
h2 : lift.{w', w} #(↑s : Type w) ≤ 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' : Type (max w w')) = lift.{w, w'} κ
rw :
  ∀ (h2 : lift.{w', w} #(↑s : Type w) ≤ #(↑s' : Type (max w w'))) (h1 : ℵ₀ ≤ #(↑s' : Type (max w w')))
    (hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ),
    ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = #(↑s' : Type (max w w'))
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
rw [← hs'] at h1 h2 ⊢
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
⊢ Nonempty M

Tactic:
have : Nonempty M := nonempty_ulift.1 (Cardinal.mk_ne_zero_iff.1
    (aleph0_pos.trans_le (h1.trans (Cardinal.mk_subtype_le _))).ne')
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = #(↑s' : Type (max w w'))

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

Premises used: Equiv.ulift, HasSubset.Subset.trans, FirstOrder.Language.skolem₁, Set.subset_union_left, FirstOrder.Language.Substructure.subset_closure, And.intro, Exists.intro, LowerAdjoint.toFun, FirstOrder.Language.Substructure.closure, FirstOrder.Language.sum, Set.image, FirstOrder.Language.Substructure.elementarySkolem₁Reduct, Union.union, DFunLike.coe
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
this₁ :
  lift.{w', w}
      #↥(elementarySkolem₁Reduct
            (LowerAdjoint.toFun (u := SetLike.coe) (closure (L.sum L.skolem₁))
              (s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s'))) =
    #(↑s' : Type (max w w'))
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = #(↑s' : Type (max w w'))

Tactic:
refine
    ⟨elementarySkolem₁Reduct (closure (L.sum L.skolem₁) (s ∪ Equiv.ulift '' s')),
      (s.subset_union_left).trans subset_closure, ?_⟩
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
⊢ lift.{max w w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) =
    lift.{w, max w w'} #(↑s' : Type (max w w'))

Tactic:
have h := mk_image_eq_lift _ s' Equiv.ulift.injective
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h :
  lift.{max w w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) =
    lift.{w, max w w'} #(↑s' : Type (max w w'))
⊢ lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))

Tactic:
rw [lift_umax.{w, w'}, lift_id'.{w, w'}] at h
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
rw :
  #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure (L.sum L.skolem₁))
          (s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s')) =
    #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w', w}
      #↥(elementarySkolem₁Reduct
            (LowerAdjoint.toFun (u := SetLike.coe) (closure (L.sum L.skolem₁))
              (s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s'))) =
    #(↑s' : Type (max w w'))

Tactic:
rw [coeSort_elementarySkolem₁Reduct, ← h, lift_inj]

Premises used: Cardinal.lift_inj, FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure (L.sum L.skolem₁))
          (s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s')) =
    #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
le_antisymm (lift_le.1 (lift_card_closure_le.trans ?_))
      (mk_le_mk_of_subset ((s.subset_union_right).trans subset_closure))

Premises used: Set.subset_union_right, HasSubset.Subset.trans, le_antisymm, Cardinal.mk_le_mk_of_subset, FirstOrder.Language.Substructure.subset_closure, Iff.mp, LE.le.trans, FirstOrder.Language.Substructure.lift_card_closure_le, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
le_antisymm :
  max ℵ₀
      (lift.{max u v, w} #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) +
        lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i)) ≤
    lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ #↥(LowerAdjoint.toFun (u := SetLike.coe) (closure (L.sum L.skolem₁))
          (s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s')) =
    #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
refine
    le_antisymm (lift_le.1 (lift_card_closure_le.trans ?_))
      (mk_le_mk_of_subset ((s.subset_union_right).trans subset_closure))

Premises used: Set.subset_union_right, HasSubset.Subset.trans, le_antisymm, Cardinal.mk_le_mk_of_subset, FirstOrder.Language.Substructure.subset_closure, Iff.mp, LE.le.trans, FirstOrder.Language.Substructure.lift_card_closure_le, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
rw :
  ℵ₀ ≤ #(↑s' : Type (max w w')) ∧
    #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
        #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ∧
      lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤
        lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
rw₁ : ℵ₀ ≤ lift.{max u v, w} #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ max ℵ₀
      (lift.{max u v, w} #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) +
        lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i)) ≤
    lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
rw [max_le_iff, aleph0_le_lift, ← aleph0_le_lift.{_, w'}, h, add_eq_max, max_le_iff, lift_le]

Premises used: max_le_iff, Cardinal.aleph0_le_lift, Cardinal.add_eq_max, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ ℵ₀ ≤ #(↑s' : Type (max w w')) ∧
    #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
        #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ∧
      lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤
        lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
⟨h1, (mk_union_le _ _).trans ?_, (lift_le.2 card_functions_sum_skolem₁_le).trans ?_⟩

Premises used: Iff.mpr, FirstOrder.Language.card_functions_sum_skolem₁_le, And.intro, LE.le.trans, Cardinal.mk_union_le, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_1 :
  #(↑s : Type w) + #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
    #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2 :
  lift.{w, max v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ ℵ₀ ≤ #(↑s' : Type (max w w')) ∧
    #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
        #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ∧
      lift.{w, max u v} #((i : ℕ) × (L.sum L.skolem₁).Functions i) ≤
        lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
refine ⟨h1, (mk_union_le _ _).trans ?_, (lift_le.2 card_functions_sum_skolem₁_le).trans ?_⟩
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_1 : max (#(↑s' : Type (max w w'))) (lift.{w', w} #(↑s : Type w)) ≤ #(↑s' : Type (max w w'))
⊢ #(↑s : Type w) + #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
    #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]

Premises used: add_comm, Cardinal.add_eq_max, Cardinal.lift_add, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ max (#(↑s' : Type (max w w'))) (lift.{w', w} #(↑s : Type w)) ≤ #(↑s' : Type (max w w'))

Tactic:
max_le le_rfl h2

Premises used: le_rfl, max_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ max (#(↑s' : Type (max w w'))) (lift.{w', w} #(↑s : Type w)) ≤ #(↑s' : Type (max w w'))

Tactic:
exact max_le le_rfl h2

Premises used: le_rfl, max_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max w w', max u v} L.card ≤
      lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ∧
    ℵ₀ ≤ #(↑s' : Type (max w w'))
⊢ lift.{w, max v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{w'},
        lift_lift, lift_lift, ← aleph0_le_lift, h]

Premises used: Cardinal.lift_lift, max_le_iff, and_comm, Cardinal.aleph0_le_lift, Cardinal.lift_aleph0, Cardinal.lift_max
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ lift.{max w w', max u v} L.card ≤
      lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ∧
    ℵ₀ ≤ #(↑s' : Type (max w w'))

Tactic:
⟨?_, h1⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max w w', max u v} L.card ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{max w w', max u v} L.card ≤
      lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ∧
    ℵ₀ ≤ #(↑s' : Type (max w w'))

Tactic:
refine ⟨?_, h1⟩
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{w, max w' u v} (lift.{w', max u v} L.card) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{max w w', max u v} L.card ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
rw [← lift_lift.{w', w}]
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ lift.{w, max w' u v} (lift.{w', max u v} L.card) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

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

Premises used: Iff.mpr, trans, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w, max w' u v} (lift.{w', max u v} L.card) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
refine _root_.trans (lift_le.{w}.2 h3) ?_
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine_2 :
  lift.{max (max u v) w, w'} κ ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₁ :
  lift.{max u v, max w w'} (lift.{w, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₂ :
  lift.{max u v, max w w'} #(↑s' : Type (max w w')) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₃ :
  lift.{max u v, max w w'} (lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
refine_2₄ refine_2₅ :
  lift.{max w' u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
    lift.{max w' u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ lift.{w, max (max u v) w'} (lift.{max u v, w'} κ) ≤
    lift.{max (max u v) w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]

Premises used: Cardinal.lift_lift
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ ℵ₀ ≤ lift.{max u v, w} #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

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

Premises used: Iff.mpr, trans, Set.subset_union_right, Cardinal.mk_le_mk_of_subset, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
refine : ℵ₀ ≤ lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
⊢ ℵ₀ ≤ lift.{max u v, w} #(↑(s ∪ (⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

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

Premises used: Iff.mpr, trans, Set.subset_union_right, Cardinal.mk_le_mk_of_subset, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
rw : ℵ₀ ≤ #(↑s' : Type (max w w'))
⊢ ℵ₀ ≤ lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)

Tactic:
rw [aleph0_le_lift, ← aleph0_le_lift, h]

Premises used: Cardinal.aleph0_le_lift
-- Module: Mathlib.ModelTheory.Skolem
Goal:
L : Language
M : Type w
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 : Type w) ≤ #(↑s' : Type (max w w'))
h1 : ℵ₀ ≤ #(↑s' : Type (max w w'))
hs' : #(↑s' : Type (max w w')) = lift.{w, w'} κ
this : Nonempty M
h : lift.{w', w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) = #(↑s' : Type (max w w'))
⊢ ℵ₀ ≤ #(↑s' : Type (max w w'))

Tactic:
h1