case inl

⊢ ∑ i in divisors 0, i = ∑ i in properDivisors 0, i + 0

case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i in divisors n, i = ∑ i in properDivisors n, i + n
n : ℕ
⊢ ∑ i in divisors n, i = ∑ i in properDivisors n, i + n
rcases Decidable.eq_or_ne n 0 with (rfl | hn)
no goals
case inl

⊢ ∑ i in divisors 0, i = ∑ i in properDivisors 0, i + 0
simp
no goals
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i in divisors n, i = ∑ i in properDivisors n, i + n
rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]