awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ image (Function.comp (β := ℕ × ℕ) Prod.snd (⇑(Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ))
      n.divisorsAntidiagonal =
    n.divisors

Tactic:
image_fst_divisorsAntidiagonal

Premises used: Nat.image_fst_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ image (Function.comp (β := ℕ × ℕ) Prod.snd (⇑(Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ))
      n.divisorsAntidiagonal =
    n.divisors

Tactic:
exact image_fst_divisorsAntidiagonal

Premises used: Nat.image_fst_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h :
  ∀ (d nd : ℕ),
    Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors) (d, nd) ↔
      (d, nd) ∈ n.divisorsAntidiagonal
⊢ map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
ext ⟨d, nd⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n d nd : ℕ
h : (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
⊢ Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors) (d, nd) ↔
    (d, nd) ∈ n.divisorsAntidiagonal

Tactic:
simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
    Prod.ext_iff, and_left_comm, exists_eq_left]

Premises used: Nat.mem_divisors, Nat.mem_divisorsAntidiagonal, Prod.ext_iff, and_left_comm, exists_eq_left, Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n d nd : ℕ
h : (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0
h₁ : d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Divisors
Goal:
d k : ℕ
hn : d * k ≠ 0
h : d * k = d * k ∧ d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0

Tactic:
rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]

Premises used: Nat.mul_div_cancel_left, left_ne_zero_of_mul, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0

Tactic:
⟨rfl, hn⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0

Tactic:
exact ⟨rfl, hn⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd

Tactic:
⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩

Premises used: Nat.mul_div_cancel_left, And.intro, left_ne_zero_of_mul, dvd_mul_right, Ne.bot_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd

Tactic:
exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a :
  map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ } n.divisors) =
    map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
⊢ map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding

Premises used: Equiv.prodComm, Finset.map_injective, Equiv.toEmbedding
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a :
  ∀ (a : ℕ × ℕ),
    a ∈
        map (Equiv.prodComm ℕ ℕ).toEmbedding
          (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ } n.divisors) ↔
      a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ } n.divisors) =
    map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a_1 : ℕ × ℕ
a :
  a_1 ∈
      map
        (Function.Embedding.trans { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ }
          (Equiv.prodComm ℕ ℕ).toEmbedding)
        n.divisors ↔
    Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors) a_1
⊢ a_1 ∈
      map (Equiv.prodComm ℕ ℕ).toEmbedding
        (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ } n.divisors) ↔
    a_1 ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal

Tactic:
rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]

Premises used: Nat.map_swap_divisorsAntidiagonal, Nat.map_div_right_divisors, Finset.map_map
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
a : ℕ × ℕ
⊢ a ∈
      map
        (Function.Embedding.trans { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ }
          (Equiv.prodComm ℕ ℕ).toEmbedding)
        n.divisors ↔
    Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors) a

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
inl : ∑ i ∈ divisors 0, i = HAdd.hAdd (α := ℕ) (∑ i ∈ properDivisors 0, i) 0
inr : ∀ (hn : n ≠ 0), ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ ∑ i ∈ divisors 0, i = HAdd.hAdd (α := ℕ) (∑ i ∈ properDivisors 0, i) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
hn : n ≠ 0
inr : ∑ i ∈ cons n n.properDivisors ⋯, i = ∑ i ∈ n.properDivisors, i + n
inr₁ : n + ∑ x ∈ n.properDivisors, x = ∑ i ∈ n.properDivisors, i + n
inr₂ inr₃ : ∑ x ∈ n.properDivisors, x + n = ∑ i ∈ n.properDivisors, i + n
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

Premises used: Finset.sum_cons, add_comm, Nat.cons_self_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : 0 < n
⊢ n.Perfect ↔ ∑ i ∈ n.properDivisors, i = n

Tactic:
and_iff_left h

Premises used: and_iff_left, Nat.Perfect
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : 0 < n
rw : ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n
⊢ n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n

Tactic:
rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]

Premises used: Nat.perfect_iff_sum_properDivisors, two_mul, Nat.sum_divisors_eq_sum_properDivisors_add_self
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : 0 < n
mp : ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n
mpr : ∑ i ∈ n.properDivisors, i + n = n + n → ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h_1 : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
mp mp₁ : n + n = n + n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h_1 : 0 < n
h : ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n

Tactic:
apply add_right_cancel h

Premises used: add_right_cancel
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k x : ℕ
rw : x ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j ≤ k, x = p ^ j
rw₁ : (∃ k_1 ≤ k, x = p ^ k_1) ∧ p ^ k ≠ 0 ↔ ∃ j ≤ k, x = p ^ j
rw₂ rw₃ : (∃ k_1 ≤ k, x = p ^ k_1) ↔ ∃ j ≤ k, x = p ^ j
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j

Tactic:
rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]

Premises used: pow_pos, Nat.mem_divisors, and_iff_left, Nat.Prime.pos, Nat.dvd_prime_pow, Nat.ne_of_gt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
h : ∀ (a : ℕ), a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
⊢ p.divisors = {1, p}

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
a : ℕ
h : a ∣ p ∧ p ≠ 0 ↔ Membership.mem (γ := Finset ℕ) {1, p} a
h₁ : (a = 1 ∨ a = p) ∧ p ≠ 0 ↔ Membership.mem (γ := Finset ℕ) {1, p} a
h₂ : a = 1 ∨ a = p ↔ Membership.mem (γ := Finset ℕ) {1, p} a
h₃ : a = 1 ∨ a = p ↔ a = 1 ∨ Membership.mem (γ := Finset ℕ) {p} a
h₄ h₅ : a = 1 ∨ a = p ↔ a = 1 ∨ a = p
⊢ a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a

Tactic:
rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]

Premises used: Finset.mem_singleton, Nat.mem_divisors, and_iff_left, Finset.mem_insert, Nat.dvd_prime, Nat.Prime.ne_zero
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
rw : (insert p p.properDivisors).erase p = {1}
rw₁ : p.divisors.erase p = {1}
rw₂ : erase {1, p} p = {1}
rw₃ : erase {p, 1} p = {1}
rw₄ rw₅ : Eq (α := Finset ℕ) {1} {1}
⊢ p.properDivisors = {1}

Tactic:
rw [← erase_insert self_notMem_properDivisors, insert_self_properDivisors pp.ne_zero,
    pp.divisors, pair_comm, erase_insert fun con => pp.ne_one (mem_singleton.1 con)]

Premises used: Finset.pair_comm, Finset.mem_singleton, Finset.erase_insert, Nat.Prime.ne_one, Nat.Prime.divisors, Nat.Prime.ne_zero, Nat.self_notMem_properDivisors, Iff.mp, Nat.insert_self_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k : ℕ
h : ∀ (a : ℕ), a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))
⊢ (p ^ k).divisors = map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))

Tactic:
ext a
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
h : (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))
⊢ a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))

Tactic:
rw [mem_divisors_prime_pow pp]

Premises used: Nat.mem_divisors_prime_pow
-- Module: Mathlib.NumberTheory.Divisors
Goal:
p : ℕ
pp : Prime p
k a : ℕ
⊢ (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ Function.Injective divisors

Tactic:
Function.LeftInverse.injective sup_divisors_id

Premises used: Function.LeftInverse.injective, Nat.sup_divisors_id
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℕ
⊢ a.divisors = b.divisors ↔ a = b

Tactic:
divisors_injective.eq_iff

Premises used: Function.Injective.eq_iff, Nat.divisors_injective
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
zero : ∀ (hsub : s ⊆ properDivisors 0), Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ properDivisors 0, x) → s = properDivisors 0
succ :
  ∀ (n : ℕ) (hsub : s ⊆ (n + 1).properDivisors),
    Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ n.properDivisors, x) → s = n.properDivisors

Tactic:
cases n
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ s = ∅

Tactic:
rw [properDivisors_zero, subset_empty] at hsub

Premises used: Nat.properDivisors_zero, Finset.subset_empty
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
hsub : s = ∅
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ properDivisors 0, x) → s = properDivisors 0

Tactic:
simp [hsub]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
succ : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x) → s = (n + 1).properDivisors
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors

Tactic:
rw [← sum_sdiff hsub]

Premises used: Finset.sum_sdiff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
succ : (n + 1).properDivisors ⊆ s
⊢ s = (n + 1).properDivisors

Tactic:
apply Subset.antisymm hsub

Premises used: Finset.Subset.antisymm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
succ : (n + 1).properDivisors \ s = ∅
⊢ (n + 1).properDivisors ⊆ s

Tactic:
rw [← sdiff_eq_empty_iff_subset]

Premises used: Finset.sdiff_eq_empty_iff_subset
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
succ :
  ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
    ∑ x ∈ s, x ≠ HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
⊢ (n + 1).properDivisors \ s = ∅

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
succ : ∑ x ∈ s, x < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
⊢ ∑ x ∈ s, x ≠ HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)

Tactic:
apply ne_of_lt

Premises used: Nat.ne_of_lt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
succ : HAdd.hAdd (α := ℕ) 0 (∑ x ∈ s, x) < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
⊢ ∑ x ∈ s, x < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)

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

Premises used: add_assoc, zero_add, add_zero, Finset.sum
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
succ : LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)
⊢ HAdd.hAdd (α := ℕ) 0 (∑ x ∈ s, x) < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
⊢ LT.lt (α := ℕ) (∑ i ∈ (n + 1).properDivisors \ s, 0) (∑ i ∈ (n + 1).properDivisors \ s, i)

Tactic:
have hlt :=
      sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset hx)
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
hlt : LT.lt (α := ℕ) (∑ i ∈ (n + 1).properDivisors \ s, 0) (∑ i ∈ (n + 1).properDivisors \ s, i)
⊢ LT.lt (α := ℕ) 0 (∑ i ∈ (n + 1).properDivisors \ s, i)

Tactic:
simp only [sum_const_zero] at hlt

Premises used: Finset.sum_const_zero
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
hlt : LT.lt (α := ℕ) 0 (∑ i ∈ (n + 1).properDivisors \ s, i)
⊢ LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)

Tactic:
apply hlt
-- Module: Mathlib.NumberTheory.Divisors
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
succ succ₁ succ₂ succ₃ :
  ∀ (h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)), s = (n + 1).properDivisors
succ₄ :
  ∀ (h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)), (n + 1).properDivisors ⊆ s
succ₅ :
  ∀ (h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)),
    (n + 1).properDivisors \ s = ∅
succ₆ :
  ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
    ∑ x ∈ s, x ≠ HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
succ₇ :
  ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
    ∑ x ∈ s, x < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
succ₈ :
  ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
    HAdd.hAdd (α := ℕ) 0 (∑ x ∈ s, x) < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
succ₉ : ∀ (h : ((n + 1).properDivisors \ s).Nonempty), LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)
succ₁₀ :
  ∀ (h : ((n + 1).properDivisors \ s).Nonempty)
    (hlt : LT.lt (α := ℕ) (∑ i ∈ (n + 1).properDivisors \ s, 0) (∑ i ∈ (n + 1).properDivisors \ s, i)),
    LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)
succ₁₁ :
  ∀ (h : ((n + 1).properDivisors \ s).Nonempty) (hlt : LT.lt (α := ℕ) 0 (∑ i ∈ (n + 1).properDivisors \ s, i)),
    LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)
⊢ Eq (α := ℕ) (∑ 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
    apply ne_of_lt
    rw [← zero_add (∑ x ∈ s, x), ← add_assoc, add_zero]
    gcongr
    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

Premises used: add_assoc, zero_add, Finset.sum_const_zero, Finset.sdiff_eq_empty_iff_subset, add_zero, Finset.Subset.antisymm, Finset.sum, Nat.ne_of_lt, Finset.sum_sdiff
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : ∑ x ∈ n.properDivisors, x ∣ n
zero :
  ∀ (h : Dvd.dvd (α := ℕ) (∑ x ∈ properDivisors 0, x) 0),
    Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ∨ Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 0
succ :
  ∀ (n : ℕ) (h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1),
    Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1
⊢ Eq (α := ℕ) (∑ x ∈ n.properDivisors, x) 1 ∨ ∑ x ∈ n.properDivisors, x = n

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : Dvd.dvd (α := ℕ) (∑ x ∈ properDivisors 0, x) 0
⊢ Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ∨ Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
succ :
  ∀ (h : ∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x ∣ HAdd.hAdd (α := ℕ) 0 1),
    Eq (α := ℕ) (∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x) 1 ∨
      ∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x = HAdd.hAdd (α := ℕ) 0 1
succ₁ :
  ∀ (n : ℕ) (h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1),
    Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1

Tactic:
rcases n with - | n
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x ∣ HAdd.hAdd (α := ℕ) 0 1
⊢ Eq (α := ℕ) (∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x) 1 ∨
    ∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x = HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp at h
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
succ : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
⊢ ∑ x ∈ n.succ.succ.properDivisors, x < n.succ.succ

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
-- Module: Mathlib.NumberTheory.Divisors
Goal:
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
succ : Eq (α := ℕ) 1 (∑ x ∈ (n + 1 + 1).properDivisors, x)
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1

Tactic:
symm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
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
succ : 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1
⊢ Eq (α := ℕ) 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]

Premises used: Iff.mpr, Finset.mem_singleton, Finset.singleton_subset_iff, Nat.eq_properDivisors_of_subset_of_sum_eq_sum, Finset.sum_singleton, And.intro, Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
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:
⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩

Premises used: Nat.succ_lt_succ, one_dvd, Nat.succ_pos, And.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
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 _)⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.properDivisors, f x = f 1

Tactic:
simp [h.properDivisors]

Premises used: Nat.Prime.properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
α : Type u_1
inst : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
rw : ∏ x ∈ cons p p.properDivisors ⋯, f x = f p * f 1
rw₁ : f p * ∏ x ∈ p.properDivisors, f x = f p * f 1
rw₂ rw₃ : f p * f 1 = f p * f 1
⊢ ∏ x ∈ p.divisors, f x = f p * f 1

Tactic:
rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]

Premises used: Nat.cons_self_properDivisors, Nat.Prime.prod_properDivisors, Nat.Prime.ne_zero, Finset.prod_cons
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ n.properDivisors = {1} ↔ Prime n

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
refine_1 : n.properDivisors = {1} → Prime n
refine_2 : Prime n → n.properDivisors = {1}
⊢ n.properDivisors = {1} ↔ Prime n

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
⊢ Prime n

Tactic:
Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩

Premises used: Iff.mpr, Nat.prime_def, And.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
refine_1 : 2 ≤ n
refine_1₁ : ∀ (m : ℕ) (hdvd : m ∣ n), m = 1 ∨ m = n
⊢ Prime n

Tactic:
refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩

Premises used: Iff.mpr, Nat.prime_def, And.intro
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : properDivisors 0 = {1}
⊢ LE.le (α := ℕ) 2 0

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : properDivisors 1 = {1}
⊢ LE.le (α := ℕ) 2 1

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n_1 n : ℕ
h : n.succ.succ.properDivisors = {1}
⊢ 2 ≤ n.succ.succ

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
⊢ 2 ≤ n

Tactic:
match n with
      | 0 => contradiction
      | 1 => contradiction
      | Nat.succ (Nat.succ n) => simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
refine_1 : m ∣ n ∧ m < n ∨ m = n
⊢ m = 1 ∨ m = n

Tactic:
rw [← mem_singleton, ← h, mem_properDivisors]

Premises used: Finset.mem_singleton, Nat.mem_properDivisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
refine_1 : ∀ (this : m ≤ n), m ∣ n ∧ m < n ∨ m = n
refine_1₁ : 0 < n
⊢ m ∣ n ∧ m < n ∨ m = n

Tactic:
have := Nat.le_of_dvd ?_ hdvd
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m ∣ n ∧ m < n ∨ m = n

Tactic:
simpa [hdvd, this] using (le_iff_eq_or_lt.mp this).symm

Premises used: le_iff_eq_or_lt, Or.symm, Iff.mp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
refine_1 : ∀ (this : n ≤ 0), False
⊢ 0 < n

Tactic:
by_contra!
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ properDivisors 0 = {1}

Tactic:
simp only [nonpos_iff_eq_zero.mp this] at h

Premises used: Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n m : ℕ
hdvd : m ∣ n
this : n ≤ 0
h : properDivisors 0 = {1}
⊢ False

Tactic:
contradiction