case h
α✝ β α : Type u
⊢ (#α) < 2 ^ (#α)
α β : Type u
a : Cardinal
⊢ a < 2 ^ a
induction' a using Cardinal.inductionOn with α
case h
α✝ β α : Type u
⊢ (#α) < (#Set α)
case h
α✝ β α : Type u
⊢ (#α) < 2 ^ (#α)
rw [← mk_set]
case h
α✝ β α : Type u
⊢ ¬Quotient.liftOn₂ (#Set α) (#α) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
case h
α✝ β α : Type u
⊢ (#α) < (#Set α)
refine' ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, _⟩
case h.intro.mk
α✝ β α : Type u
f : Set α → α
hf : Injective f
⊢ False
case h
α✝ β α : Type u
⊢ ¬Quotient.liftOn₂ (#Set α) (#α) (fun α β => Nonempty (α ↪ β)) instLECardinal.proof_1
rintro ⟨⟨f, hf⟩⟩
no goals
case h.intro.mk
α✝ β α : Type u
f : Set α → α
hf : Injective f
⊢ False
exact cantor_injective f hf