Theorem: power_nat_nat_card_eq_power_nat (meetings/ex5.lean)

State before:
⊢ Cardinal.mk ↑(𝒫 Set.univ) = Cardinal.mk ↑(𝒫 Set.univ)
Tactic:
simp only [Cardinal.mk_powerset,
           Cardinal.mk_univ,
           Cardinal.mk_eq_aleph0,
           Cardinal.two_power_aleph0]
State after:
no goals