n : ℕ
h : 0 < n
⊢ ∑ i in properDivisors n, i = n ↔ ∑ i in properDivisors n, i + n = n + n
n : ℕ
h : 0 < n
⊢ Perfect n ↔ ∑ i in divisors n, i = 2 * n
rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i in properDivisors n, i = n
⊢ ∑ i in properDivisors n, i + n = n + n

case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i in properDivisors n, i + n = n + n
⊢ ∑ i in properDivisors n, i = n
n : ℕ
h : 0 < n
⊢ ∑ i in properDivisors n, i = n ↔ ∑ i in properDivisors n, i + n = n + n
constructor <;> intro h
no goals
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i in properDivisors n, i = n
⊢ ∑ i in properDivisors n, i + n = n + n
rw [h]
no goals
case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i in properDivisors n, i + n = n + n
⊢ ∑ i in properDivisors n, i = n
apply add_right_cancel h