case zero
h : ∑ x in properDivisors zero, x ∣ zero
⊢ ∑ x in properDivisors zero, x = 1 ∨ ∑ x in properDivisors zero, x = zero

case succ
n : ℕ
h : ∑ x in properDivisors (succ n), x ∣ succ n
⊢ ∑ x in properDivisors (succ n), x = 1 ∨ ∑ x in properDivisors (succ n), x = succ n
n : ℕ
h : ∑ x in properDivisors n, x ∣ n
⊢ ∑ x in properDivisors n, x = 1 ∨ ∑ x in properDivisors n, x = n
cases' n with n
no goals
case zero
h : ∑ x in properDivisors zero, x ∣ zero
⊢ ∑ x in properDivisors zero, x = 1 ∨ ∑ x in properDivisors zero, x = zero
simp
case succ.zero
h : ∑ x in properDivisors (succ zero), x ∣ succ zero
⊢ ∑ x in properDivisors (succ zero), x = 1 ∨ ∑ x in properDivisors (succ zero), x = succ zero

case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1 ∨ ∑ x in properDivisors (succ (succ n)), x = succ (succ n)
case succ
n : ℕ
h : ∑ x in properDivisors (succ n), x ∣ succ n
⊢ ∑ x in properDivisors (succ n), x = 1 ∨ ∑ x in properDivisors (succ n), x = succ n
cases' n with n
case succ.zero
h : ∑ x in properDivisors (succ zero), x ≠ 1 ∧ ∑ x in properDivisors (succ zero), x ≠ succ zero
⊢ ¬∑ x in properDivisors (succ zero), x ∣ succ zero
case succ.zero
h : ∑ x in properDivisors (succ zero), x ∣ succ zero
⊢ ∑ x in properDivisors (succ zero), x = 1 ∨ ∑ x in properDivisors (succ zero), x = succ zero
contrapose! h
no goals
case succ.zero
h : ∑ x in properDivisors (succ zero), x ≠ 1 ∧ ∑ x in properDivisors (succ zero), x ≠ succ zero
⊢ ¬∑ x in properDivisors (succ zero), x ∣ succ zero
simp
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
⊢ ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n) → ∑ x in properDivisors (succ (succ n)), x = 1
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1 ∨ ∑ x in properDivisors (succ (succ n)), x = succ (succ n)
rw [or_iff_not_imp_right]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
⊢ ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n) → ∑ x in properDivisors (succ (succ n)), x = 1
intro ne_n
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1
have hlt : (∑ x in n.succ.succ.properDivisors, x) < n.succ.succ :=
  lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ 1 = ∑ x in properDivisors (succ (succ n)), x
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1
symm
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ 1 ∣ succ (succ n) ∧ 1 < succ (succ n)
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ 1 = ∑ x in properDivisors (succ (succ n)), x
rw [← mem_singleton,
  eq_properDivisors_of_subset_of_sum_eq_sum
    (singleton_subset_iff.2 (mem_properDivisors.2 ⟨h, hlt⟩)) sum_singleton,
  mem_properDivisors]
no goals
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ 1 ∣ succ (succ n) ∧ 1 < succ (succ n)
refine' ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩