case zero
s : Finset ℕ
hsub : s ⊆ properDivisors zero
⊢ ∑ x in s, x = ∑ x in properDivisors zero, x → s = properDivisors zero

case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝), x → s = properDivisors (succ n✝)
n : ℕ
s : Finset ℕ
hsub : s ⊆ properDivisors n
⊢ ∑ x in s, x = ∑ x in properDivisors n, x → s = properDivisors n
cases n
no goals
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝), x → s = properDivisors (succ n✝)
classical
  rw [← sum_sdiff hsub]
  intro h
  apply Subset.antisymm hsub
  rw [← sdiff_eq_empty_iff_subset]
  contrapose h
  rw [← Ne.def, ← nonempty_iff_ne_empty] at h
  apply ne_of_lt
  rw [← zero_add (∑ x in 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
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x in s, x = ∑ x in properDivisors zero, x → s = properDivisors zero
case zero
s : Finset ℕ
hsub : s ⊆ properDivisors zero
⊢ ∑ x in s, x = ∑ x in properDivisors zero, x → s = properDivisors zero
rw [properDivisors_zero, subset_empty] at hsub
no goals
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x in s, x = ∑ x in properDivisors zero, x → s = properDivisors zero
simp [hsub]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x → s = properDivisors (succ n✝)
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝), x → s = properDivisors (succ n✝)
rw [← sum_sdiff hsub]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ s = properDivisors (succ n✝)
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x → s = properDivisors (succ n✝)
intro h
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ properDivisors (succ n✝) ⊆ s
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ s = properDivisors (succ n✝)
apply Subset.antisymm hsub
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ properDivisors (succ n✝) \ s = ∅
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ properDivisors (succ n✝) ⊆ s
rw [← sdiff_eq_empty_iff_subset]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ¬properDivisors (succ n✝) \ s = ∅
⊢ ¬∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ properDivisors (succ n✝) \ s = ∅
contrapose h
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ ¬∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ¬properDivisors (succ n✝) \ s = ∅
⊢ ¬∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
rw [← Ne.def, ← nonempty_iff_ne_empty] at h
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ ∑ x in s, x < ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ ¬∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
apply ne_of_lt
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ 0 + ∑ x in s, x < ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ ∑ x in s, x < ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
rw [← zero_add (∑ x in s, x), ← add_assoc, add_zero]
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ 0 + ∑ x in s, x < ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
apply add_lt_add_right
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
hlt : ∑ i in properDivisors (succ n✝) \ s, 0 < ∑ i in properDivisors (succ n✝) \ s, i
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
have hlt :=
  sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset _ _ hx)
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
hlt : 0 < ∑ i in properDivisors (succ n✝) \ s, i
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
hlt : ∑ i in properDivisors (succ n✝) \ s, 0 < ∑ i in properDivisors (succ n✝) \ s, i
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
simp only [sum_const_zero] at hlt
no goals
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
hlt : 0 < ∑ i in properDivisors (succ n✝) \ s, i
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
apply hlt