-- Mathlib/NumberTheory/Divisors.lean
theorem sum_properDivisors_dvd (h : (∑ x ∈ n.properDivisors, x) ∣ n) :
    ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

Proof state:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 = ∑ x ∈ (n + 1 + 1).properDivisors, x

Tactic:
rw [← mem_singleton, eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2
  (mem_properDivisors.2 ⟨h, hlt⟩)) (sum_singleton _ _), mem_properDivisors]

Result:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1

Proof state:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1

Tactic:
exact ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

Result:
no goals

Proof state:
n : ℕ
h : ∑ x ∈ n.properDivisors, x ∣ n
⊢ ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n

Tactic:
rcases n with - | n

Result:
case zero
h : ∑ x ∈ properDivisors 0, x ∣ 0
⊢ ∑ x ∈ properDivisors 0, x = 1 ∨ ∑ x ∈ properDivisors 0, x = 0

case succ
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1

Proof state:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Tactic:
have hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ :=
  lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n

Result:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Proof state:
case succ.zero
h : ∑ x ∈ (0 + 1).properDivisors, x ∣ 0 + 1
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (0 + 1).properDivisors, x = 0 + 1

Tactic:
simp at h

Result:
no goals

Proof state:
case zero
h : ∑ x ∈ properDivisors 0, x ∣ 0
⊢ ∑ x ∈ properDivisors 0, x = 1 ∨ ∑ x ∈ properDivisors 0, x = 0

Tactic:
simp

Result:
no goals

Proof state:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1

Tactic:
rw [or_iff_not_imp_right]

Result:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Proof state:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Tactic:
intro ne_n

Result:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Proof state:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1

Tactic:
symm

Result:
case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
hlt : ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ
⊢ 1 = ∑ x ∈ (n + 1 + 1).properDivisors, x

Proof state:
case succ
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1

Tactic:
rcases n with - | n

Result:
case succ.zero
h : ∑ x ∈ (0 + 1).properDivisors, x ∣ 0 + 1
⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (0 + 1).properDivisors, x = 0 + 1

case succ.succ
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
⊢ ∑ x ∈ (n + 1 + 1).properDivisors, x = 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1