case zero

⊢ ∑ x in properDivisors zero, x = 1 ↔ Prime zero

case succ
n : ℕ
⊢ ∑ x in properDivisors (succ n), x = 1 ↔ Prime (succ n)
n : ℕ
⊢ ∑ x in properDivisors n, x = 1 ↔ Prime n
cases' n with n
no goals
case zero

⊢ ∑ x in properDivisors zero, x = 1 ↔ Prime zero
simp [Nat.not_prime_zero]
case succ.zero

⊢ ∑ x in properDivisors (succ zero), x = 1 ↔ Prime (succ zero)

case succ.succ
n✝ : ℕ
⊢ ∑ x in properDivisors (succ (succ n✝)), x = 1 ↔ Prime (succ (succ n✝))
case succ
n : ℕ
⊢ ∑ x in properDivisors (succ n), x = 1 ↔ Prime (succ n)
cases n
no goals
case succ.zero

⊢ ∑ x in properDivisors (succ zero), x = 1 ↔ Prime (succ zero)
simp [Nat.not_prime_one]
case succ.succ
n✝ : ℕ
⊢ ∑ x in properDivisors (succ (succ n✝)), x = 1 ↔ properDivisors (succ (succ n✝)) = {1}
case succ.succ
n✝ : ℕ
⊢ ∑ x in properDivisors (succ (succ n✝)), x = 1 ↔ Prime (succ (succ n✝))
rw [← properDivisors_eq_singleton_one_iff_prime]
case succ.succ
n✝ : ℕ
h : ∑ x in properDivisors (succ (succ n✝)), x = 1
⊢ properDivisors (succ (succ n✝)) = {1}
case succ.succ
n✝ : ℕ
⊢ ∑ x in properDivisors (succ (succ n✝)), x = 1 ↔ properDivisors (succ (succ n✝)) = {1}
refine' ⟨fun h => _, fun h => h.symm ▸ sum_singleton⟩
case succ.succ
n✝ : ℕ
h : ∑ x in properDivisors (succ (succ n✝)), x = 1
⊢ {1} = properDivisors (succ (succ n✝))
case succ.succ
n✝ : ℕ
h : ∑ x in properDivisors (succ (succ n✝)), x = 1
⊢ properDivisors (succ (succ n✝)) = {1}
rw [@eq_comm (Finset ℕ) _ _]
no goals
case succ.succ
n✝ : ℕ
h : ∑ x in properDivisors (succ (succ n✝)), x = 1
⊢ {1} = properDivisors (succ (succ n✝))
apply
  eq_properDivisors_of_subset_of_sum_eq_sum
    (singleton_subset_iff.2
      (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
    (Eq.trans sum_singleton h.symm)