α β : Type u
f : ℕ → Cardinal
⊢ (#Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i => f (i + 1)
α β : Type u
f : ℕ → Cardinal
⊢ sum f = f 0 + sum fun i => f (i + 1)
refine' (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans _
no goals
α β : Type u
f : ℕ → Cardinal
⊢ (#Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i => f (i + 1)
simp only [mk_sum, mk_out, lift_id, mk_sigma]