-- Mathlib/NumberTheory/Divisors.lean
theorem eq_properDivisors_of_subset_of_sum_eq_sum {s : Finset ℕ} (hsub : s ⊆ n.properDivisors) :
    ((∑ x ∈ s, x) = ∑ x ∈ n.properDivisors, x) → s = n.properDivisors

Proof state:
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 + ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
apply add_lt_add_right

Result:
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ s = (n✝ + 1).properDivisors

Tactic:
apply Subset.antisymm hsub

Result:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors ⊆ s

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Tactic:
rw [← sum_sdiff hsub]

Result:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x → s = (n✝ + 1).properDivisors

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors \ s = ∅

Tactic:
contrapose h

Result:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ¬(n✝ + 1).properDivisors \ s = ∅
⊢ ¬∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Proof state:
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]

Result:
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 + ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x → s = (n✝ + 1).properDivisors

Tactic:
intro h

Result:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ s = (n✝ + 1).properDivisors

Proof state:
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Tactic:
apply hlt

Result:
no goals

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ¬∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
apply ne_of_lt

Result:
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x < ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors ⊆ s

Tactic:
rw [← sdiff_eq_empty_iff_subset]

Result:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x
⊢ (n✝ + 1).properDivisors \ s = ∅

Proof state:
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
simp [hsub]

Result:
no goals

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ¬(n✝ + 1).properDivisors \ s = ∅
⊢ ¬∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Tactic:
rw [← Ne, ← nonempty_iff_ne_empty] at h

Result:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ ¬∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors \ s, x + ∑ x ∈ s, x

Proof state:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Tactic:
classical
  rw [← sum_sdiff hsub]
  intro h
  apply Subset.antisymm hsub
  rw [← sdiff_eq_empty_iff_subset]
  contrapose h
  rw [← Ne, ← nonempty_iff_ne_empty] at h
  apply ne_of_lt
  rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]
  apply add_lt_add_right
  have hlt :=
    sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)
  simp only [sum_const_zero] at hlt
  apply hlt

Result:
no goals

Proof state:
n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors

Tactic:
cases n

Result:
case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Proof state:
case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Tactic:
rw [properDivisors_zero, subset_empty] at hsub

Result:
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

Proof state:
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : ∑ i ∈ (n✝ + 1).properDivisors \ s, 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Tactic:
simp only [sum_const_zero] at hlt

Result:
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Proof state:
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x

Tactic:
have hlt :=
  sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)

Result:
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
h : ((n✝ + 1).properDivisors \ s).Nonempty
hlt : ∑ i ∈ (n✝ + 1).properDivisors \ s, 0 < ∑ i ∈ (n✝ + 1).properDivisors \ s, i
⊢ 0 < ∑ x ∈ (n✝ + 1).properDivisors \ s, x