awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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),
  HAdd.hAdd (α := ℕ) 0 (∑ 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)
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)
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have succ₉ : ∀ (h : ((n + 1).properDivisors \ s).Nonempty), LT.lt (α := ℕ) 0 (∑ x ∈ (n + 1).properDivisors \ 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)
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)
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have 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)
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)
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)
⊢ Eq (α := ℕ) (∑ x ∈ s, x) (∑ x ∈ (n + 1).properDivisors, x) → s = (n + 1).properDivisors
have 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)
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:
n : ℕ
h : ∑ x ∈ n.properDivisors, x ∣ n
⊢ Eq (α := ℕ) (∑ x ∈ n.properDivisors, x) 1 ∨ ∑ x ∈ n.properDivisors, x = n
have zero : ∀ (h : Dvd.dvd (α := ℕ) (∑ x ∈ properDivisors 0, x) 0),
  Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ∨ Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 0
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ Eq (α := ℕ) (∑ x ∈ n.properDivisors, x) 1 ∨ ∑ x ∈ n.properDivisors, x = n
have succ : ∀ (n : ℕ) (h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1),
  Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : ∑ x ∈ (n + 1).properDivisors, x ∣ n + 1
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1
have 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
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ∨ ∑ x ∈ (n + 1).properDivisors, x = n + 1
have 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
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
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
have succ : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1 → Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
Tactic: rw [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
h : ∑ x ∈ (n + 1 + 1).properDivisors, x ∣ n + 1 + 1
ne_n : ¬∑ x ∈ (n + 1 + 1).properDivisors, x = n + 1 + 1
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
have hlt : ∑ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
have succ : Eq (α := ℕ) 1 (∑ x ∈ (n + 1 + 1).properDivisors, x)
Tactic: symm
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ Eq (α := ℕ) 1 (∑ x ∈ (n + 1 + 1).properDivisors, x)
have succ : 1 ∣ n + 1 + 1 ∧ 1 < n + 1 + 1
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x ∈ p.divisors, f x = f p * f 1
have rw : ∏ x ∈ cons p p.properDivisors sorry, f x = f p * f 1
Tactic: rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
rw : ∏ x ∈ cons p p.properDivisors ⋯, f x = f p * f 1
⊢ ∏ x ∈ p.divisors, f x = f p * f 1
have rw₁ : f p * ∏ x ∈ p.properDivisors, f x = f p * f 1
Tactic: rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
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
⊢ ∏ x ∈ p.divisors, f x = f p * f 1
have rw₂ : f p * f 1 = f p * f 1
Tactic: rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ n.properDivisors = {1} ↔ Prime n
have refine_1 : n.properDivisors = {1} → Prime n
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
refine_1 : n.properDivisors = {1} → Prime n
⊢ n.properDivisors = {1} ↔ Prime n
have refine_2 : Prime n → n.properDivisors = {1}
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n.properDivisors = {1}
⊢ Prime n
have refine_1 : 2 ≤ n
Tactic: refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n.properDivisors = {1}
refine_1 : 2 ≤ n
⊢ Prime n
have refine_1₁ : ∀ (m : ℕ) (hdvd : m ∣ n), m = 1 ∨ m = n
Tactic: refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ m = 1 ∨ m = n
have refine_1 : m ∣ n ∧ m < n ∨ m = n
Tactic: rw [← mem_singleton, ← h, mem_properDivisors]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ m ∣ n ∧ m < n ∨ m = n
have refine_1 : ∀ (this : m ≤ n), m ∣ n ∧ m < n ∨ m = n
Tactic: have := Nat.le_of_dvd ?_ hdvd
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
refine_1 : ∀ (this : m ≤ n), m ∣ n ∧ m < n ∨ m = n
⊢ m ∣ n ∧ m < n ∨ m = n
have refine_1₁ : 0 < n
Tactic: have := Nat.le_of_dvd ?_ hdvd
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
⊢ 0 < n
have refine_1 : ∀ (this : n ≤ 0), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
h : n.properDivisors = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ False
have h₁ : properDivisors 0 = {1}
Tactic: simp only [nonpos_iff_eq_zero.mp this] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ n.properDivisors, x) 1 ↔ Prime n
have zero : Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ↔ Prime 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
zero : Eq (α := ℕ) (∑ x ∈ properDivisors 0, x) 1 ↔ Prime 0
⊢ Eq (α := ℕ) (∑ x ∈ n.properDivisors, x) 1 ↔ Prime n
have succ : ∀ (n : ℕ), Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ↔ Prime (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ↔ Prime (n + 1)
have succ : Eq (α := ℕ) (∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x) 1 ↔ Prime (HAdd.hAdd (α := ℕ) 0 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
succ : Eq (α := ℕ) (∑ x ∈ (HAdd.hAdd (α := ℕ) 0 1).properDivisors, x) 1 ↔ Prime (HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1).properDivisors, x) 1 ↔ Prime (n + 1)
have succ₁ : ∀ (n : ℕ), Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ Prime (n + 1 + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ Prime (n + 1 + 1)
have succ : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ (n + 1 + 1).properDivisors = {1}
Tactic: rw [← properDivisors_eq_singleton_one_iff_prime]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1 ↔ (n + 1 + 1).properDivisors = {1}
have succ : ∀ (h : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1), (n + 1 + 1).properDivisors = {1}
Tactic: refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : Eq (α := ℕ) (∑ x ∈ (n + 1 + 1).properDivisors, x) 1
⊢ (n + 1 + 1).properDivisors = {1}
have succ : {1} = (n + 1 + 1).properDivisors
Tactic: rw [@eq_comm (Finset ℕ) _ _]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j
have rw : (∃ (x_1 : ℕ), (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j
Tactic: rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ (x_1 : ℕ), (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j
have simp : (∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j
Tactic: simp only [exists_prop, and_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j
have h : ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
have h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k → a < k ∧ x = p ^ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k → a < k ∧ x = p ^ a
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
have h₁ : a < k ∧ x = p ^ a → a ≤ k ∧ x = p ^ a ∧ x < p ^ k
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k
⊢ a < k ∧ x = p ^ a
have h₁ : ∀ (_h_left : a ≤ k) (h_right : p ^ a < p ^ k), a < k ∧ p ^ a = p ^ a
Tactic: rcases h with ⟨_h_left, rfl, h_right⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : p ^ a < p ^ k
⊢ a < k ∧ p ^ a = p ^ a
have h_right₁ : a < k
Tactic: rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right
Cleared hypotheses: h_right
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k x a : ℕ
h : a < k ∧ x = p ^ a
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k
have h₁ : ∀ (h_left : a < k), a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k
Tactic: rcases h with ⟨h_left, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k
have h : a ≤ k ∧ p ^ a = p ^ a ∧ a < k
Tactic: rw [Nat.pow_lt_pow_iff_right pp.one_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k : ℕ
⊢ (p ^ k).properDivisors = map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range k)
have h : ∀ (a : ℕ), a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := sorry : ℕ ↪ ℕ } (range k)
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun (x : ℕ) ↦ p ^ x, inj' := ⋯ : ℕ ↪ ℕ } (range k)
have h : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
Tactic: simp only [mem_properDivisors, mem_map, mem_range, Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
have this : a ∈ (p ^ k).properDivisors ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j
Tactic: have := mem_properDivisors_prime_pow pp k (x := a)
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ (p ^ k).properDivisors ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
have this₁ : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ (j : ℕ) (_ : j < k), a = p ^ j
Tactic: rw [mem_properDivisors] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ Eq.{u_1 + 1} (α := M) (∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2) (∏ i ∈ n.divisors, f i (n / i))
have rw : Eq.{u_1 + 1} (α := M)
  (∏ x ∈ n.divisors,
    f (({ toFun := fun (d : ℕ) ↦ (d, n / d), inj' := sorry } : (a : ℕ) → ℕ × ℕ) x).1
      (({ toFun := fun (d : ℕ) ↦ (d, n / d), inj' := sorry } : (a : ℕ) → ℕ × ℕ) x).2)
  (∏ i ∈ n.divisors, f i (n / i))
Tactic: rw [← map_div_right_divisors, Finset.prod_map]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
M : Type u_1
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ Eq.{u_1 + 1} (α := M) (∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2) (∏ i ∈ n.divisors, f (n / i) i)
have rw : Eq.{u_1 + 1} (α := M)
  (∏ x ∈ n.divisorsAntidiagonal,
    f (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).1
      (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).2)
  (∏ i ∈ n.divisors, f (n / i) i)
Tactic: rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
⊢ {p ∈ n.primeFactors | p ∣ m} = m.primeFactors
have simp_rw : {p ∈ {p ∈ n.divisors | Prime p} | p ∣ m} = {p ∈ m.divisors | Prime p}
Tactic: simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm,
    divisors_filter_dvd_of_dvd hn hmn]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
simp_rw : {p ∈ {p ∈ n.divisors | Prime p} | p ∣ m} = {p ∈ m.divisors | Prime p}
⊢ {p ∈ n.primeFactors | p ∣ m} = m.primeFactors
have simp_rw₁ : {p ∈ {p ∈ n.divisors | p ∣ m} | Prime p} = {p ∈ m.divisors | Prime p}
Tactic: simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm,
    divisors_filter_dvd_of_dvd hn hmn]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
have pos : ∀ (hn : n = 0), image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
pos : ∀ (hn : n = 0), image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
⊢ image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
have neg : ∀ (hn : ¬n = 0), image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
⊢ image (fun (x : ℕ) ↦ n / x) n.divisors = n.divisors
have neg : ∀ (a : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a ↔ a ∈ n.divisors
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a ↔ a ∈ n.divisors
have neg : Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a → a ∈ n.divisors
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
neg : Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a → a ∈ n.divisors
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a ↔ a ∈ n.divisors
have neg₁ : a ∈ n.divisors → Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a → a ∈ n.divisors
have neg : (∃ a_1 ∈ n.divisors, n / a_1 = a) → a ∈ n.divisors
Tactic: rw [mem_image]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ n.divisors
hx2 : n / x = a
⊢ a ∈ n.divisors
have neg : ∀ (hx1 : x ∣ n ∧ n ≠ 0) (hx2 : n / x = a), a ∣ n ∧ n ≠ 0
Tactic: rw [mem_divisors] at *
Cleared hypotheses: hx1, hx2
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0
have neg : a ∣ n
Tactic: refine ⟨?_, hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n
have neg : n / x ∣ n
Tactic: rw [← hx2]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ n.divisors → Membership.mem (γ := Finset ℕ) (image (fun (x : ℕ) ↦ n / x) n.divisors) a
have neg : a ∣ n ∧ n ≠ 0 → ∃ a_2 ∈ n.divisors, n / a_2 = a
Tactic: rw [mem_divisors, mem_image]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
have pos : ∀ (hn : n = 0), ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
Tactic: by_cases hn : n = 0