awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
⊢ IsElementary.{w, u, v} (L := L) (M := M)
    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S)
have apply : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1))
  (x :
    Fin n →
      ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
          L.Substructure M))
  (a : M),
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x) ∘
          x)
        a) →
    ∃ (b :
      ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
          L.Substructure M)),
      BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
          (Subtype.val (p := fun (x : M) ↦
              Membership.mem (γ := L.Substructure M)
                ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                  L.Substructure M)
                x) ∘
            x)
          (↑b : M))
Tactic: apply (LHom.sumInl.substructureReduct S).isElementary_of_exists
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
⊢ ∃ (b :
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)),
    BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x) ∘
          x)
        (↑b : M))
have h₁ : BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
  (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
    (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := L.Substructure M)
          ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
            L.Substructure M)
          x) ∘
      x)
    (↑(Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x)
          (funMap φ'
            (Subtype.val (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                    L.Substructure M)
                  x) ∘
              x))
          sorry) :
      M))
Tactic: use ⟨funMap φ' ((↑) ∘ x), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
M : Type w
inst : Nonempty M
inst_1 : L.Structure M
S : (L.sum L.skolem₁).Substructure M
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
x :
  Fin n →
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)
a : M
h :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      a)
φ' : (L.sum L.skolem₁).Functions n := LHom.onFunction LHom.sumInr φ
h₁ :
  BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
    (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
      (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M)
            ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
              L.Substructure M)
            x) ∘
        x)
      (↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x)
            (funMap φ'
              (Subtype.val (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M)
                        S :
                      L.Substructure M)
                    x) ∘
                x))
            ⋯) :
        M))
⊢ ∃ (b :
    ↥((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
        L.Substructure M)),
    BoundedFormula.Realize.{u, v, w, 0} (M := M) φ default
      (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ M)
        (Subtype.val (p := fun (x : M) ↦
            Membership.mem (γ := L.Substructure M)
              ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
                L.Substructure M)
              x) ∘
          x)
        (↑b : M))
have w : Membership.mem (γ := L.Substructure M)
  ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
    L.Substructure M)
  (funMap φ'
    (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := L.Substructure M)
          ((LHom.substructureReduct LHom.sumInl : (a : (L.sum L.skolem₁).Substructure M) → L.Substructure M) S :
            L.Substructure M)
          x) ∘
      x))
Tactic: use ⟨funMap φ' ((↑) ∘ x), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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 : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ
have obtain : ∀ (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'} κ
Tactic: obtain ⟨s', hs'⟩ := Cardinal.le_mk_iff_exists_set.1 h4
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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'} κ
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ
have 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'} κ
Tactic: rw [← aleph0_le_lift.{_, w}] at h1
Cleared hypotheses: h1, h2, h3, h4, s', hs'
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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'} κ
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = lift.{w, w'} κ
have 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'))
Tactic: rw [← hs'] at h1 h2 ⊢
Cleared hypotheses: h1, h2, hs'
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (hypothesis)
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'} κ
⊢ ∃ (S : L.ElementarySubstructure M), s ⊆ (↑S : Set M) ∧ lift.{w', w} #↥S = #(↑s' : Type (max w w'))
have this : 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')
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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'))
have 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'))
Tactic: refine
    ⟨elementarySkolem₁Reduct (closure (L.sum L.skolem₁) (s ∪ Equiv.ulift '' s')),
      (s.subset_union_left).trans subset_closure, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (hypothesis)
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.{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'))
have 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'))
Tactic: have h := mk_image_eq_lift _ s' Equiv.ulift.injective
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (hypothesis)
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}
      #↥(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'))
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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', 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'))
have 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)
Tactic: rw [coeSort_elementarySkolem₁Reduct, ← h, lift_inj]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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)
have 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)
Tactic: refine
    le_antisymm (lift_le.1 (lift_card_closure_le.trans ?_))
      (mk_le_mk_of_subset ((s.subset_union_right).trans subset_closure))
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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 ℵ₀
      (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)
have 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)
Tactic: rw [max_le_iff, aleph0_le_lift, ← aleph0_le_lift.{_, w'}, h, add_eq_max, max_le_iff, lift_le]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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)
⊢ 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)
have rw₁ : ℵ₀ ≤ lift.{max u v, w} #(↑(s ∪ (⇑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]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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)
have 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)
Tactic: refine ⟨h1, (mk_union_le _ _).trans ?_, (lift_le.2 card_functions_sum_skolem₁_le).trans ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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)
⊢ ℵ₀ ≤ #(↑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)
have 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)
Tactic: refine ⟨h1, (mk_union_le _ _).trans ?_, (lift_le.2 card_functions_sum_skolem₁_le).trans ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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 w) + #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w) ≤
    #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have refine_1 : max (#(↑s' : Type (max w w'))) (lift.{w', w} #(↑s : Type w)) ≤ #(↑s' : Type (max w w'))
Tactic: rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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 v u} (max ℵ₀ L.card) ≤ lift.{max u v, w} #(↑((⇑Equiv.ulift : (a : ULift.{w', w} M) → M) '' s') : Type w)
have 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'))
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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'))
have 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)
Tactic: refine ⟨?_, h1⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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)
have 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)
Tactic: rw [← lift_lift.{w', w}]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
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)
have 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)
Tactic: refine _root_.trans (lift_le.{w}.2 h3) ?_