awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
x : ℕ × ℕ
rw : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x ∈ n.divisorsAntidiagonal
rw₁ : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal
have rw₂ : x.swap.2 * x.swap.1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
Tactic: rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
x : ℕ × ℕ
rw : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x ∈ n.divisorsAntidiagonal
rw₁ : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
rw₂ : x.swap.2 * x.swap.1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal
have rw₃ : (x.2, x.1).2 * (x.2, x.1).1 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
Tactic: rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.1 ∈ n.divisors
have h₁ : x.1 * x.2 = n ∧ n ≠ 0
Tactic: rw [mem_divisorsAntidiagonal] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.2 ∈ n.divisors
have h₁ : x.1 * x.2 = n ∧ n ≠ 0
Tactic: rw [mem_divisorsAntidiagonal] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal = n.divisorsAntidiagonal
have rw : Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) = (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
Tactic: rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm,
    Set.image_swap_eq_preimage_swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) = (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
have h : ∀ (x : ℕ × ℕ), x ∈ Prod.swap ⁻¹' (↑n.divisorsAntidiagonal : Set (ℕ × ℕ)) ↔ x ∈ (↑n.divisorsAntidiagonal : Set (ℕ × ℕ))
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ image Prod.fst n.divisorsAntidiagonal = n.divisors
have h : ∀ (a : ℕ), a ∈ image Prod.fst n.divisorsAntidiagonal ↔ a ∈ n.divisors
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ image Prod.snd n.divisorsAntidiagonal = n.divisors
have rw : image (Function.comp (β := ℕ × ℕ) Prod.snd (⇑(Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ))
    n.divisorsAntidiagonal =
  n.divisors
Tactic: rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
have h : ∀ (d nd : ℕ),
  Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := sorry } n.divisors) (d, nd) ↔
    (d, nd) ∈ n.divisorsAntidiagonal
Tactic: ext ⟨d, nd⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n d nd : ℕ
⊢ Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := ⋯ } n.divisors) (d, nd) ↔
    (d, nd) ∈ n.divisorsAntidiagonal
have h : (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
Tactic: simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
    Prod.ext_iff, and_left_comm, exists_eq_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
have h : (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n d nd : ℕ
h : (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
have h₁ : d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0
have h : d * k = d * k ∧ d * k ≠ 0
Tactic: rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal
have a : map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := sorry : ℕ ↪ ℕ × ℕ } n.divisors) =
  map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
Tactic: apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ } n.divisors) =
    map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
have a : ∀ (a : ℕ × ℕ),
  a ∈
      map (Equiv.prodComm ℕ ℕ).toEmbedding
        (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := sorry : ℕ ↪ ℕ × ℕ } n.divisors) ↔
    a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
a : ℕ × ℕ
⊢ a ∈
      map (Equiv.prodComm ℕ ℕ).toEmbedding
        (map { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := ⋯ : ℕ ↪ ℕ × ℕ } n.divisors) ↔
    a ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal
have a : a ∈
    map
      (Function.Embedding.trans { toFun := fun (d : ℕ) ↦ (n / d, d), inj' := sorry : ℕ ↪ ℕ × ℕ }
        (Equiv.prodComm ℕ ℕ).toEmbedding)
      n.divisors ↔
  Membership.mem (γ := Finset (ℕ × ℕ)) (map { toFun := fun (d : ℕ) ↦ (d, n / d), inj' := sorry } n.divisors) a
Tactic: rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
have inl : ∑ i ∈ divisors 0, i = HAdd.hAdd (α := ℕ) (∑ i ∈ properDivisors 0, i) 0
Tactic: rcases Decidable.eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
inl : ∑ i ∈ divisors 0, i = HAdd.hAdd (α := ℕ) (∑ i ∈ properDivisors 0, i) 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
have inr : ∀ (hn : n ≠ 0), ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
Tactic: rcases Decidable.eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
have inr : ∑ i ∈ cons n n.properDivisors sorry, i = ∑ i ∈ n.properDivisors, i + n
Tactic: rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
inr : ∑ i ∈ cons n n.properDivisors ⋯, i = ∑ i ∈ n.properDivisors, i + n
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
have inr₁ : n + ∑ x ∈ n.properDivisors, x = ∑ i ∈ n.properDivisors, i + n
Tactic: rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n
have inr₂ : ∑ x ∈ n.properDivisors, x + n = ∑ i ∈ n.properDivisors, i + n
Tactic: rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : 0 < n
⊢ n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n
have rw : ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n
Tactic: rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : 0 < n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n
have mp : ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : 0 < n
mp : ∑ i ∈ n.properDivisors, i = n → ∑ i ∈ n.properDivisors, i + n = n + n
⊢ ∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n
have mpr : ∑ i ∈ n.properDivisors, i + n = n + n → ∑ i ∈ n.properDivisors, i = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h_1 : 0 < n
h : ∑ i ∈ n.properDivisors, i = n
⊢ ∑ i ∈ n.properDivisors, i + n = n + n
have mp : n + n = n + n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
have rw : x ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ 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))]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x : ℕ
rw : x ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j ≤ k, x = p ^ j
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
have rw₁ : (∃ k_1 ≤ k, x = p ^ k_1) ∧ p ^ k ≠ 0 ↔ ∃ 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))]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ x ∈ (p ^ k).divisors ↔ ∃ j ≤ k, x = p ^ j
have rw₂ : (∃ k_1 ≤ k, x = p ^ k_1) ↔ ∃ 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))]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
⊢ p.divisors = {1, p}
have h : ∀ (a : ℕ), a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
a : ℕ
⊢ a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
have h : a ∣ p ∧ p ≠ 0 ↔ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
a : ℕ
h : a ∣ p ∧ p ≠ 0 ↔ Membership.mem (γ := Finset ℕ) {1, p} a
⊢ a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
have h₁ : (a = 1 ∨ a = p) ∧ p ≠ 0 ↔ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
have h₂ : a = 1 ∨ a = p ↔ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
have h₃ : a = 1 ∨ a = p ↔ a = 1 ∨ Membership.mem (γ := Finset ℕ) {p} a
Tactic: rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ a ∈ p.divisors ↔ Membership.mem (γ := Finset ℕ) {1, p} a
have h₄ : a = 1 ∨ a = p ↔ a = 1 ∨ a = p
Tactic: rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
⊢ p.properDivisors = {1}
have rw : (insert p p.properDivisors).erase p = {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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
rw : (insert p p.properDivisors).erase p = {1}
⊢ p.properDivisors = {1}
have rw₁ : p.divisors.erase p = {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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
rw : (insert p p.properDivisors).erase p = {1}
rw₁ : p.divisors.erase p = {1}
⊢ p.properDivisors = {1}
have rw₂ : erase {1, p} p = {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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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}
⊢ p.properDivisors = {1}
have rw₃ : erase {p, 1} p = {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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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}
⊢ p.properDivisors = {1}
have rw₄ : Eq (α := Finset ℕ) {1} {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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).divisors = map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))
have h : ∀ (a : ℕ), a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := sorry : ℕ ↪ ℕ } (range (k + 1))
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).divisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range (k + 1))
have h : (∃ j ≤ k, a = p ^ j) ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := sorry : ℕ ↪ ℕ } (range (k + 1))
Tactic: rw [mem_divisors_prime_pow pp]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ n.properDivisors, x) → s = n.properDivisors
have zero : ∀ (hsub : s ⊆ properDivisors 0), Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ properDivisors 0, x) → s = properDivisors 0
Tactic: cases n
Cleared hypotheses: n, hsub
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
s : Finset ℕ
hsub : s ⊆ n.properDivisors
zero : ∀ (hsub : s ⊆ properDivisors 0), Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ properDivisors 0, x) → s = properDivisors 0
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ n.properDivisors, x) → s = n.properDivisors
have succ : ∀ (n : ℕ) (hsub : s ⊆ (n + 1).properDivisors),
  Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
Tactic: cases n
Cleared hypotheses: n, hsub
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ properDivisors 0, x) → s = properDivisors 0
have hsub₁ : s = ∅
Tactic: rw [properDivisors_zero, subset_empty] at hsub
Cleared hypotheses: hsub
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x) → s = (n + 1).properDivisors
Tactic: rw [← sum_sdiff hsub]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
⊢ s = (n + 1).properDivisors
have succ : (n + 1).properDivisors ⊆ s
Tactic: apply Subset.antisymm hsub
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
⊢ (n + 1).properDivisors ⊆ s
have succ : (n + 1).properDivisors \ s = ∅
Tactic: rw [← sdiff_eq_empty_iff_subset]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
⊢ (n + 1).properDivisors \ s = ∅
have succ : ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
  ∑ x ∈ s, x ≠ HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x ≠ HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
have succ : ∑ x ∈ s, x < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
⊢ ∑ x ∈ s, x < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
have succ : HAdd.hAdd (α := ℕ) 0 (∑ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
⊢ HAdd.hAdd (α := ℕ) 0 (∑ x ∈ s, x) < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
have succ : LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
h : ((n + 1).properDivisors \ s).Nonempty
⊢ LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ s, x)
have hlt : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
s : Finset ℕ
n : ℕ
hsub : s ⊆ (n + 1).properDivisors
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, 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
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ₄ : ∀ (h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)), (n + 1).properDivisors ⊆ s
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
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ₅ : ∀ (h : ∑ x ∈ s, x = HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)),
  (n + 1).properDivisors \ s = ∅
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
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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 = ∅
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ₆ : ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
  ∑ x ∈ s, x ≠ HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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)
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ₇ : ∀ (h : ((n + 1).properDivisors \ s).Nonempty),
  ∑ x ∈ s, x < HAdd.hAdd (α := ℕ) (∑ x ∈ (n + 1).properDivisors \ s, x) (∑ x ∈ s, x)
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