α : Type u
β : α → Type u
⊢ (#WType β) = (#(i : α) × (β i → WType β))
α : Type u
β : α → Type u
⊢ (#WType β) = sum fun a => (#WType β) ^ (#β a)
simp only [Cardinal.power_def, ← Cardinal.mk_sigma]
no goals
α : Type u
β : α → Type u
⊢ (#WType β) = (#(i : α) × (β i → WType β))
exact mk_congr (equivSigma β)