case intro.intro
α β : Type u
c : Cardinal
h' : c < (#ℕ)
h : lift c < ℵ₀
⊢ ∃ n, lift c = ↑n
α β : Type u
c : Cardinal
h : c < ℵ₀
⊢ ∃ n, c = ↑n
rcases lt_lift_iff.1 h with ⟨c, rfl, h'⟩
case intro.intro.intro
α β : Type u
S : Set ℕ
h' : (#↑S) < (#ℕ)
h : lift (#↑S) < ℵ₀
⊢ ∃ n, lift (#↑S) = ↑n
case intro.intro
α β : Type u
c : Cardinal
h' : c < (#ℕ)
h : lift c < ℵ₀
⊢ ∃ n, lift c = ↑n
rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩
case intro.intro.intro
α β : Type u
S : Set ℕ
h' : (#↑S) < (#ℕ)
h : lift (#↑S) < ℵ₀
⊢ Set.Finite S
case intro.intro.intro
α β : Type u
S : Set ℕ
h' : (#↑S) < (#ℕ)
h : lift (#↑S) < ℵ₀
⊢ ∃ n, lift (#↑S) = ↑n
suffices S.Finite by
  lift S to Finset ℕ using this
  simp
case intro.intro.intro
α β : Type u
S : Set ℕ
h : lift (#↑S) < ℵ₀
h' : ¬Set.Finite S
⊢ (#ℕ) ≤ (#↑S)
case intro.intro.intro
α β : Type u
S : Set ℕ
h' : (#↑S) < (#ℕ)
h : lift (#↑S) < ℵ₀
⊢ Set.Finite S
contrapose! h'
case intro.intro.intro
α β : Type u
S : Set ℕ
h : lift (#↑S) < ℵ₀
h' : ¬Set.Finite S
this : Infinite ↑S
⊢ (#ℕ) ≤ (#↑S)
case intro.intro.intro
α β : Type u
S : Set ℕ
h : lift (#↑S) < ℵ₀
h' : ¬Set.Finite S
⊢ (#ℕ) ≤ (#↑S)
haveI := Infinite.to_subtype h'
no goals
case intro.intro.intro
α β : Type u
S : Set ℕ
h : lift (#↑S) < ℵ₀
h' : ¬Set.Finite S
this : Infinite ↑S
⊢ (#ℕ) ≤ (#↑S)
exact ⟨Infinite.natEmbedding S⟩
case intro
α β : Type u
S : Finset ℕ
h' : (#↑↑S) < (#ℕ)
h : lift (#↑↑S) < ℵ₀
⊢ ∃ n, lift (#↑↑S) = ↑n
α β : Type u
S : Set ℕ
h' : (#↑S) < (#ℕ)
h : lift (#↑S) < ℵ₀
this : Set.Finite S
⊢ ∃ n, lift (#↑S) = ↑n
lift S to Finset ℕ using this
no goals
case intro
α β : Type u
S : Finset ℕ
h' : (#↑↑S) < (#ℕ)
h : lift (#↑↑S) < ℵ₀
⊢ ∃ n, lift (#↑↑S) = ↑n
simp