[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ #((n : ℕ) × Functions (Language.sum L (skolem₁ L)) n) = #((n : ℕ) × BoundedFormula L Empty (n + 1))
[PROOFSTEP]
simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ((sum fun i => lift #(Functions L i)) + sum fun i => lift #(BoundedFormula L Empty (i + 1))) =
    sum fun i => #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
| (sum fun i => lift #(Functions L i)) + sum fun i => lift #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
enter [2, 1, i]; rw [lift_id'.{u, v}]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
| (sum fun i => lift #(Functions L i)) + sum fun i => lift #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
enter [2, 1, i]; rw [lift_id'.{u, v}]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
| (sum fun i => lift #(Functions L i)) + sum fun i => lift #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
enter [2, 1, i]
[GOAL]
case h
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
i : ℕ
| lift #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
rw [lift_id'.{u, v}]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ((sum fun i => lift #(Functions L i)) + sum fun i => #(BoundedFormula L Empty (i + 1))) =
    sum fun i => #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
rw [add_comm, add_eq_max, max_eq_left]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (sum fun i => lift #(Functions L i)) ≤ sum fun i => #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
refine' sum_le_sum _ _ fun n => _
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
⊢ lift #(Functions L n) ≤ #(BoundedFormula L Empty (n + 1))
[PROOFSTEP]
rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
⊢ Nonempty (Functions L n ↪ BoundedFormula L Empty (n + 1))
[PROOFSTEP]
refine' ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => _⟩⟩
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
f g : Functions L n
h : (fun f => func f default =' func f default) f = (fun f => func f default =' func f default) g
⊢ f = g
[PROOFSTEP]
rcases h with ⟨rfl, ⟨rfl⟩⟩
[GOAL]
case refl
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
f : Functions L n
⊢ f = f
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ℵ₀ ≤ sum fun i => #(BoundedFormula L Empty (i + 1))
[PROOFSTEP]
rw [← mk_sigma]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ℵ₀ ≤ #((i : ℕ) × BoundedFormula L Empty (i + 1))
[PROOFSTEP]
exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy => (Sigma.mk.inj_iff.1 xy).1)
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ #((n : ℕ) × Functions (Language.sum L (skolem₁ L)) n) ≤ max ℵ₀ (card L)
[PROOFSTEP]
rw [card_functions_sum_skolem₁]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ #((n : ℕ) × BoundedFormula L Empty (n + 1)) ≤ max ℵ₀ (card L)
[PROOFSTEP]
trans #(Σ n, L.BoundedFormula Empty n)
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ #((n : ℕ) × BoundedFormula L Empty (n + 1)) ≤ #((n : ℕ) × BoundedFormula L Empty n)
[PROOFSTEP]
exact ⟨⟨Sigma.map Nat.succ fun _ => id, Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ #((n : ℕ) × BoundedFormula L Empty n) ≤ max ℵ₀ (card L)
[PROOFSTEP]
refine' _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 _)
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ lift (max ℵ₀ (lift #Empty + lift (card L))) ≤ lift (max ℵ₀ (card L))
[PROOFSTEP]
simp only [mk_empty, lift_zero, lift_uzero, zero_add]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ lift (max ℵ₀ (card L)) ≤ lift (max ℵ₀ (card L))
[PROOFSTEP]
rfl
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
⊢ IsElementary (↑(LHom.substructureReduct LHom.sumInl) S)
[PROOFSTEP]
apply (LHom.sumInl.substructureReduct S).isElementary_of_exists
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
⊢ ∀ (n : ℕ) (φ : BoundedFormula L Empty (n + 1)) (x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S })
    (a : M),
    BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) →
      ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
[PROOFSTEP]
intro n φ x a h
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
⊢ ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
[PROOFSTEP]
let φ' : (L.sum L.skolem₁).Functions n := LHom.sumInr.onFunction φ
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ ∃ b, BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)
[PROOFSTEP]
exact
  ⟨⟨funMap φ' ((↑) ∘ x), S.fun_mem (LHom.sumInr.onFunction φ) ((↑) ∘ x) (by exact fun i => (x i).2)⟩, by
    exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩⟩
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ ∀ (i : Fin n), (Subtype.val ∘ x) i ∈ ↑S
[PROOFSTEP]
exact fun i => (x i).2
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
S : Substructure (Language.sum L (skolem₁ L)) M
n : ℕ
φ : BoundedFormula L Empty (n + 1)
x : Fin n → { x // x ∈ ↑(LHom.substructureReduct LHom.sumInl) S }
a : M
h : BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)
φ' : Functions (Language.sum L (skolem₁ L)) n := LHom.onFunction LHom.sumInr φ
⊢ BoundedFormula.Realize φ default
    (Fin.snoc (Subtype.val ∘ x)
      ↑{ val := funMap φ' (Subtype.val ∘ x),
          property := (_ : funMap (LHom.onFunction LHom.sumInr φ) (Subtype.val ∘ x) ∈ ↑S) })
[PROOFSTEP]
exact Classical.epsilon_spec (p := fun a => BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a)) ⟨a, h⟩
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ Small.{?u.38330, w} { x // x ∈ elementarySkolem₁Reduct ⊥ }
[PROOFSTEP]
rw [coeSort_elementarySkolem₁Reduct]
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ Small.{?u.38330, w} { x // x ∈ ⊥ }
[PROOFSTEP]
infer_instance
[GOAL]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ κ
h2 : lift #↑s ≤ lift κ
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
⊢ ∃ S, s ⊆ ↑S ∧ lift #{ x // x ∈ S } = lift κ
[PROOFSTEP]
obtain ⟨s', hs'⟩ := Cardinal.le_mk_iff_exists_set.1 h4
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ κ
h2 : lift #↑s ≤ lift κ
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
hs' : #↑s' = lift κ
⊢ ∃ S, s ⊆ ↑S ∧ lift #{ x // x ∈ S } = lift κ
[PROOFSTEP]
rw [← aleph0_le_lift.{_, w}] at h1 
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift κ
h2 : lift #↑s ≤ lift κ
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
hs' : #↑s' = lift κ
⊢ ∃ S, s ⊆ ↑S ∧ lift #{ x // x ∈ S } = lift κ
[PROOFSTEP]
rw [← hs'] at h1 h2 ⊢
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
⊢ ∃ S, s ⊆ ↑S ∧ lift #{ x // x ∈ S } = #↑s'
[PROOFSTEP]
refine'
  ⟨elementarySkolem₁Reduct (closure (L.sum L.skolem₁) (s ∪ Equiv.ulift '' s')),
    (s.subset_union_left _).trans subset_closure, _⟩
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
⊢ lift
      #{ x //
          x ∈
            elementarySkolem₁Reduct
              (LowerAdjoint.toFun (closure (Language.sum L (skolem₁ L))) (s ∪ ↑Equiv.ulift '' s')) } =
    #↑s'
[PROOFSTEP]
have h := mk_image_eq_lift _ s' Equiv.ulift.injective
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = lift #↑s'
⊢ lift
      #{ x //
          x ∈
            elementarySkolem₁Reduct
              (LowerAdjoint.toFun (closure (Language.sum L (skolem₁ L))) (s ∪ ↑Equiv.ulift '' s')) } =
    #↑s'
[PROOFSTEP]
rw [lift_umax.{w, w'}, lift_id'.{w, w'}] at h 
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ lift
      #{ x //
          x ∈
            elementarySkolem₁Reduct
              (LowerAdjoint.toFun (closure (Language.sum L (skolem₁ L))) (s ∪ ↑Equiv.ulift '' s')) } =
    #↑s'
[PROOFSTEP]
rw [coeSort_elementarySkolem₁Reduct, ← h, lift_inj]
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ #{ x // x ∈ LowerAdjoint.toFun (closure (Language.sum L (skolem₁ L))) (s ∪ ↑Equiv.ulift '' s') } =
    #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
refine'
  le_antisymm (lift_le.1 (lift_card_closure_le.trans _))
    (mk_le_mk_of_subset ((Set.subset_union_right _ _).trans subset_closure))
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ max ℵ₀ (lift #↑(s ∪ ↑Equiv.ulift '' s') + lift #((i : ℕ) × Functions (Language.sum L (skolem₁ L)) i)) ≤
    lift #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
rw [max_le_iff, aleph0_le_lift, ← aleph0_le_lift.{_, w'}, h, add_eq_max, max_le_iff, lift_le]
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ #↑s' ∧
    #↑(s ∪ ↑Equiv.ulift '' s') ≤ #↑(↑Equiv.ulift '' s') ∧
      lift #((i : ℕ) × Functions (Language.sum L (skolem₁ L)) i) ≤ lift #↑(↑Equiv.ulift '' s')
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift #↑(s ∪ ↑Equiv.ulift '' s')
[PROOFSTEP]
refine' ⟨h1, (mk_union_le _ _).trans _, (lift_le.2 card_functions_sum_skolem₁_le).trans _⟩
[GOAL]
case intro.refine'_1
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ #↑s + #↑(↑Equiv.ulift '' s') ≤ #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
rw [← lift_le, lift_add, h, add_comm, add_eq_max h1]
[GOAL]
case intro.refine'_1
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ max (#↑s') (lift #↑s) ≤ #↑s'
[PROOFSTEP]
exact max_le le_rfl h2
[GOAL]
case intro.refine'_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ lift (max ℵ₀ (card L)) ≤ lift #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
rw [lift_max, lift_aleph0, max_le_iff, aleph0_le_lift, and_comm, ← lift_le.{w'}, lift_lift, lift_lift, ← aleph0_le_lift,
  h]
[GOAL]
case intro.refine'_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ lift (card L) ≤ lift #↑(↑Equiv.ulift '' s') ∧ ℵ₀ ≤ #↑s'
[PROOFSTEP]
refine' ⟨_, h1⟩
[GOAL]
case intro.refine'_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ lift (card L) ≤ lift #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
rw [← lift_lift.{w', w}]
[GOAL]
case intro.refine'_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ lift (lift (card L)) ≤ lift #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
refine' _root_.trans (lift_le.{w}.2 h3) _
[GOAL]
case intro.refine'_2
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ lift (lift κ) ≤ lift #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
rw [lift_lift, ← lift_lift.{w, max u v}, ← hs', ← h, lift_lift]
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift #↑(s ∪ ↑Equiv.ulift '' s')
[PROOFSTEP]
refine' _root_.trans _ (lift_le.2 (mk_le_mk_of_subset (Set.subset_union_right _ _)))
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ lift #↑(↑Equiv.ulift '' s')
[PROOFSTEP]
rw [aleph0_le_lift, ← aleph0_le_lift, h]
[GOAL]
case intro
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
s : Set M
κ : Cardinal.{w'}
h3 : lift (card L) ≤ lift κ
h4 : lift κ ≤ lift #M
s' : Set (ULift M)
h2 : lift #↑s ≤ #↑s'
h1 : ℵ₀ ≤ #↑s'
hs' : #↑s' = lift κ
h : lift #↑(↑Equiv.ulift '' s') = #↑s'
⊢ ℵ₀ ≤ #↑s'
[PROOFSTEP]
exact h1
