awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
rw :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (t.prod id) : R) ((g : (a : ℕ) → R) (n / t.prod id) : R)
rw₁ :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (∏ x ∈ t, x) : R) ((g : (a : ℕ) → R) (n / ∏ x ∈ t, x) : R)
⊢ HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) t.val.prod : R) ((g : (a : ℕ) → R) (n / t.val.prod) : R)
have rw₂ : HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (∏ x ∈ t, x) : R) ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R)
Tactic: rw [t.prod_val, Function.id_def,
    ← prod_primeFactors_sdiff_of_squarefree hn (mem_powerset.mp ht),
    hf.map_prod_of_subset_primeFactors n t (mem_powerset.mp ht),
    ← hg.map_prod_of_subset_primeFactors n (_ \ t) sdiff_subset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
rw :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (t.prod id) : R) ((g : (a : ℕ) → R) (n / t.prod id) : R)
rw₁ :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (∏ x ∈ t, x) : R) ((g : (a : ℕ) → R) (n / ∏ x ∈ t, x) : R)
rw₂ :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (∏ x ∈ t, x) : R)
      ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R)
⊢ HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) t.val.prod : R) ((g : (a : ℕ) → R) (n / t.val.prod) : R)
have rw₃ : HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
  HMul.hMul (α := R) (β := R) (∏ a ∈ t, (f : (a : ℕ) → R) a : R) ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R)
Tactic: rw [t.prod_val, Function.id_def,
    ← prod_primeFactors_sdiff_of_squarefree hn (mem_powerset.mp ht),
    hf.map_prod_of_subset_primeFactors n t (mem_powerset.mp ht),
    ← hg.map_prod_of_subset_primeFactors n (_ \ t) sdiff_subset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ∈ n.primeFactors.powerset
rw :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (t.prod id) : R) ((g : (a : ℕ) → R) (n / t.prod id) : R)
rw₁ :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (∏ x ∈ t, x) : R) ((g : (a : ℕ) → R) (n / ∏ x ∈ t, x) : R)
rw₂ :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (∏ x ∈ t, x) : R)
      ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R)
rw₃ :
  HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) (∏ a ∈ t, (f : (a : ℕ) → R) a : R) ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R)
⊢ HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) t.val.prod : R) ((g : (a : ℕ) → R) (n / t.val.prod) : R)
have rw₄ : HMul.hMul (α := R) (β := R) (∏ i ∈ t, (f : (a : ℕ) → R) i : R) ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R) =
  HMul.hMul (α := R) (β := R) (∏ a ∈ t, (f : (a : ℕ) → R) a : R) ((g : (a : ℕ) → R) (∏ a ∈ n.primeFactors \ t, a) : R)
Tactic: rw [t.prod_val, Function.id_def,
    ← prod_primeFactors_sdiff_of_squarefree hn (mem_powerset.mp ht),
    hf.map_prod_of_subset_primeFactors n t (mem_powerset.mp ht),
    ← hg.map_prod_of_subset_primeFactors n (_ \ t) sdiff_subset]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
⊢ (pow k : (a : ℕ) → ℕ) n = if k = 0 ∧ n = 0 then 0 else n ^ k
have zero : (pow 0 : (a : ℕ) → ℕ) n = if Eq (α := ℕ) 0 0 ∧ n = 0 then 0 else HPow.hPow (β := ℕ) n 0
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
zero : (pow 0 : (a : ℕ) → ℕ) n = if Eq (α := ℕ) 0 0 ∧ n = 0 then 0 else HPow.hPow (β := ℕ) n 0
⊢ (pow k : (a : ℕ) → ℕ) n = if k = 0 ∧ n = 0 then 0 else n ^ k
have succ : ∀ (n_1 : ℕ), (pow (n_1 + 1) : (a : ℕ) → ℕ) n = if n_1 + 1 = 0 ∧ n = 0 then 0 else n ^ (n_1 + 1)
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
⊢ pow 0 = ζ
have h : ∀ (n : ℕ), Eq (α := ℕ) ((pow 0 : (a : ℕ) → ℕ) n : ℕ) ((ζ : (a : ℕ) → ℕ) n : ℕ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
⊢ pow 1 = ArithmeticFunction.id
have h : ∀ (n : ℕ), Eq (α := ℕ) ((pow 1 : (a : ℕ) → ℕ) n : ℕ) ((ArithmeticFunction.id : (a : ℕ) → ℕ) n : ℕ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0
have inl : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ) ↔ Eq (α := ℕ) 0 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
inl : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ) ↔ Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0
have inr : ∀ (hn : n ≠ 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0
have inr : Eq (α := ℕ) (∑ d ∈ n.divisors, d ^ k) 0 ↔ n = 0
Tactic: simp only [ArithmeticFunction.sigma_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (∑ d ∈ n.divisors, (n / d) ^ k : ℕ)
have rw : Eq (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, (n / d) ^ k)
Tactic: rw [sigma_apply, ← sum_div_divisors]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
rw : Eq (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, (n / d) ^ k)
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (∑ d ∈ n.divisors, (n / d) ^ k : ℕ)
have rw₁ : Eq (α := ℕ) (∑ d ∈ n.divisors, (n / d) ^ k) (∑ d ∈ n.divisors, (n / d) ^ k)
Tactic: rw [sigma_apply, ← sum_div_divisors]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
hn0 : n ≠ 0
⊢ LT.lt (α := ℕ) (0 : ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)
have rwa : 0 < n
Tactic: rwa [sigma_pos_iff, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k k' n : ℕ
hk : k ≤ k'
⊢ LE.le (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) ((σ k' : (a : ℕ) → ℕ) n : ℕ)
have simp_rw : LE.le (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, d ^ k')
Tactic: simp_rw [sigma_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k k' n : ℕ
hk : k ≤ k'
⊢ LE.le (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, d ^ k')
have h : ∀ (d : ℕ) (hd : d ∈ n.divisors), 1 ≤ d
Tactic: gcongr with d hd
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k : ℕ
⊢ ζ * pow k = σ k
have h : ∀ (x : ℕ), Eq (α := ℕ) ((ζ * pow k : (a : ℕ) → ℕ) x : ℕ) ((σ k : (a : ℕ) → ℕ) x : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k x : ℕ
⊢ Eq (α := ℕ) ((ζ * pow k : (a : ℕ) → ℕ) x : ℕ) ((σ k : (a : ℕ) → ℕ) x : ℕ)
have h : Eq (α := ℕ) (∑ i ∈ x.divisors, (pow k : (a : ℕ) → ℕ) i : ℕ)
  (({ toFun := fun (n : ℕ) ↦ ∑ d ∈ n.divisors, d ^ k, map_zero' := sorry } : (a : ℕ) → ℕ) x : ℕ)
Tactic: rw [sigma, zeta_mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k x : ℕ
⊢ Eq (α := ℕ) (∑ i ∈ x.divisors, (pow k : (a : ℕ) → ℕ) i : ℕ)
    (({ toFun := fun (n : ℕ) ↦ ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } : (a : ℕ) → ℕ) x : ℕ)
have h : ∀ x_1 ∈ x.divisors, (pow k : (a : ℕ) → ℕ) x_1 = x_1 ^ k
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k : ℕ
⊢ (σ k).IsMultiplicative
have rw : (ζ * pow k).IsMultiplicative
Tactic: rw [← zeta_mul_pow_eq_sigma]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)
    (∏ p ∈ n.primeFactors,
        ∑ i ∈ range (HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)), p ^ (i * k) :
      ℕ)
have rw : Eq (α := ℕ) (n.factorization.prod fun (p k_1 : ℕ) ↦ (σ k : (a : ℕ) → ℕ) (p ^ k_1))
  (∏ p ∈ n.primeFactors,
    ∑ i ∈ range (HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)), p ^ (i * k))
Tactic: rw [isMultiplicative_sigma.multiplicative_factorization _ hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
⊢ (σ k : (a : ℕ) → ℕ) n ≤ n ^ (k + 1)
have simp : ∑ d ∈ n.divisors, d ^ k ≤ n * n ^ k
Tactic: simp only [sigma_apply, pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
⊢ ∑ d ∈ n.divisors, d ^ k ≤ n * n ^ k
have refine : ∑ i ∈ n.divisors, n ^ k ≤ n * n ^ k
Tactic: refine (Finset.sum_le_sum fun d hd ↦ Nat.pow_le_pow_left (Nat.divisor_le hd) k).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ #n.divisors = ∏ x ∈ n.primeFactors, HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ)
have rw : Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ (σ 0 : (a : ℕ) → ℕ) (p ^ k))
  (∏ x ∈ n.primeFactors, HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ))
Tactic: rw [← sigma_zero_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
⊢ #n.divisors = 1 ↔ n = 1
have inl : #(divisors 0) = 1 ↔ Eq (α := ℕ) 0 1
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
inl : #(divisors 0) = 1 ↔ Eq (α := ℕ) 0 1
⊢ #n.divisors = 1 ↔ n = 1
have inr : ∀ (hn : n ≠ 0), #n.divisors = 1 ↔ n = 1
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ #n.divisors = 1 ↔ n = 1
have inr : ∀ (h : #n.divisors = 1), n = 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
have pos : ∀ (hn0 : n = 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
pos : ∀ (hn0 : n = 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
have neg : ∀ (hn0 : ¬n = 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
hn0 : ¬n = 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
have neg : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) → n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
hn0 : ¬n = 0
neg : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) → n = 1
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
have neg₁ : n = 1 → Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
⊢ n = 1
have neg : Eq (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
Tactic: rw [← sigma_zero_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (hypothesis)
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
⊢ Eq (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
have zero_lt_sigma : LT.lt (α := ℕ) (0 : ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ)
Tactic: have zero_lt_sigma := sigma_pos 0 n hn0
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (hypothesis)
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
zero_lt_sigma : LT.lt (α := ℕ) (0 : ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ)
⊢ Eq (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
have sigma_zero_le_sigma : LE.le (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)
Tactic: have sigma_zero_le_sigma := sigma_mono 0 k n k.zero_le
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (∑ d ∈ n.divisors, d)
    (∏ p ∈ n.primeFactors,
      ∑ k ∈ range (HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)), p ^ k)
have rw : Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ (σ 1 : (a : ℕ) → ℕ) (p ^ k))
  (∏ p ∈ n.primeFactors,
    ∑ k ∈ range (HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)), p ^ k)
Tactic: rw [← sigma_one_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0 ∨ n = 1
have rw : n.primeFactorsList.length = 0 ↔ n = 0 ∨ n = 1
Tactic: rw [cardFactors_apply, List.length_eq_zero_iff, primeFactorsList_eq_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : n.primeFactorsList.length = 0 ↔ n = 0 ∨ n = 1
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0 ∨ n = 1
have rw₁ : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
Tactic: rw [cardFactors_apply, List.length_eq_zero_iff, primeFactorsList_eq_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : n.primeFactorsList.length = 0 ↔ n = 0 ∨ n = 1
rw₁ : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0 ∨ n = 1
have rw₂ : n = 0 ∨ n = 1 ↔ n = 0 ∨ n = 1
Tactic: rw [cardFactors_apply, List.length_eq_zero_iff, primeFactorsList_eq_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) ↔ 1 < n
have rw : 0 < n.primeFactorsList.length ↔ 1 < n
Tactic: rw [cardFactors_apply, List.length_pos_iff, primeFactorsList_ne_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : 0 < n.primeFactorsList.length ↔ 1 < n
⊢ LT.lt (α := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) ↔ 1 < n
have rw₁ : n.primeFactorsList ≠ [] ↔ 1 < n
Tactic: rw [cardFactors_apply, List.length_pos_iff, primeFactorsList_ne_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
rw : 0 < n.primeFactorsList.length ↔ 1 < n
rw₁ : n.primeFactorsList ≠ [] ↔ 1 < n
⊢ LT.lt (α := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) ↔ 1 < n
have rw₂ : 1 < n ↔ 1 < n
Tactic: rw [cardFactors_apply, List.length_pos_iff, primeFactorsList_ne_nil]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ Nat.Prime n
have refine : ∀ (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)), Nat.Prime n
Tactic: refine ⟨fun h => ?_, fun h => List.length_eq_one_iff.2 ⟨n, primeFactorsList_prime h⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)
⊢ Nat.Prime (n + 1)
have succ : ∀ (x : ℕ) (hx : (n + 1).primeFactorsList = [x]), Nat.Prime (n + 1)
Tactic: rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime (n + 1)
have succ : Nat.Prime x
Tactic: rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)
x : ℕ
hx : (n + 1).primeFactorsList = [x]
⊢ Nat.Prime x
have succ : x ∈ (n + 1).primeFactorsList
Tactic: apply prime_of_mem_primeFactorsList
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
⊢ Nat.Prime n
have zero : ∀ (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)), Nat.Prime 0
Tactic: cases n with | zero => simp at h | succ n =>
  rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
  rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
  apply prime_of_mem_primeFactorsList
  rw [hx, List.mem_singleton]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
n : ℕ
h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
zero : ∀ (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) 0 : ℕ) (1 : ℕ)), Nat.Prime 0
⊢ Nat.Prime n
have succ : ∀ (n : ℕ) (h : Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) (n + 1) : ℕ) (1 : ℕ)), Nat.Prime (n + 1)
Tactic: cases n with | zero => simp at h | succ n =>
  rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
  rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
  apply prime_of_mem_primeFactorsList
  rw [hx, List.mem_singleton]
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
rw : (m * n).primeFactorsList.length = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : (m * n).primeFactorsList.length = HAdd.hAdd (β := ℕ) m.primeFactorsList.length ((Ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : (m * n).primeFactorsList.length = m.primeFactorsList.length + n.primeFactorsList.length
rw₃ : (↑(m * n).primeFactorsList : Multiset ℕ).card = m.primeFactorsList.length + n.primeFactorsList.length
rw₄ : (UniqueFactorizationMonoid.normalizedFactors (m * n)).card = m.primeFactorsList.length + n.primeFactorsList.length
⊢ (Ω : (a : ℕ) → ℕ) (m * n) = HAdd.hAdd (α := ℕ) (β := ℕ) ((Ω : (a : ℕ) → ℕ) m : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ)
have rw₅ : (UniqueFactorizationMonoid.normalizedFactors m + UniqueFactorizationMonoid.normalizedFactors n).card =
  m.primeFactorsList.length + n.primeFactorsList.length
Tactic: rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
    Multiset.card_add, Multiset.coe_card, Multiset.coe_card]