α β : Type u
ι : Type u_1
f g : ι → Cardinal
this :
  (#(i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    (#(i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g
α β : Type u
ι : Type u_1
f g : ι → Cardinal
⊢ sum (f + g) = sum f + sum g
have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
α β : Type u
ι : Type u_1
f g : ι → Cardinal
this : (sum fun i => f i + g i) = (sum fun i => f i) + sum fun i => g i
⊢ sum (f + g) = sum f + sum g
α β : Type u
ι : Type u_1
f g : ι → Cardinal
this :
  (#(i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    (#(i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g
simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this
no goals
α β : Type u
ι : Type u_1
f g : ι → Cardinal
this : (sum fun i => f i + g i) = (sum fun i => f i) + sum fun i => g i
⊢ sum (f + g) = sum f + sum g
exact this