awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ t ∈ n.primeFactors.powerset,
      HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i))
    (∑ i ∈ (↑n.primeFactorsList : Multiset ℕ).toFinset.powerset,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) i.val.prod : R) ((g : (a : ℕ) → R) (n / i.val.prod) : R))
⊢ Eq (α := R)
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := R) (β := R) ((f : (a : ℕ) → R) x : R) ((g : (a : ℕ) → R) x : R) : R)
    ((f * g : (a : ℕ) → R) n : R)

Tactic:
rw [prod_add, mul_apply, sum_divisorsAntidiagonal (f · * g ·),
    ← divisors_filter_squarefree_of_squarefree hn, sum_divisors_filter_squarefree hn.ne_zero,
    factors_eq]

Premises used: Nat.divisors_filter_squarefree_of_squarefree, HMul.hMul, Finset.prod_add, Nat.factors_eq, Nat.sum_divisors_filter_squarefree, Squarefree.ne_zero, ArithmeticFunction.mul_apply, DFunLike.coe, Nat.sum_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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
apply :
  ∀ x ∈ n.primeFactors.powerset,
    HMul.hMul (α := R) (∏ i ∈ x, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ x, (g : (a : ℕ) → R) i) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.val.prod : R) ((g : (a : ℕ) → R) (n / x.val.prod) : R)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ t ∈ n.primeFactors.powerset,
      HMul.hMul (α := R) (∏ i ∈ t, (f : (a : ℕ) → R) i) (∏ i ∈ n.primeFactors \ t, (g : (a : ℕ) → R) i))
    (∑ i ∈ (↑n.primeFactorsList : Multiset ℕ).toFinset.powerset,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) i.val.prod : R) ((g : (a : ℕ) → R) (n / i.val.prod) : R))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
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)
rw₄ 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)
⊢ 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)

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]

Premises used: Nat.prod_primeFactors_sdiff_of_squarefree, Function.id_def, ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors, Finset.prod_val, Finset.mem_powerset, SDiff.sdiff, Iff.mp, Finset.sdiff_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
x : ℕ
⊢ (ArithmeticFunction.id : (a : ℕ) → ℕ) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
⊢ ArithmeticFunction.id.IsMultiplicative

Tactic:
⟨rfl, fun _ => rfl⟩

Premises used: ArithmeticFunction.IsMultiplicative, And.intro, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
zero : (pow 0 : (a : ℕ) → ℕ) n = if Eq (α := ℕ) 0 0 ∧ n = 0 then 0 else HPow.hPow (β := ℕ) n 0
succ : ∀ (n_1 : ℕ), (pow (n_1 + 1) : (a : ℕ) → ℕ) n = if n_1 + 1 = 0 ∧ n = 0 then 0 else n ^ (n_1 + 1)
⊢ (pow k : (a : ℕ) → ℕ) n = if k = 0 ∧ n = 0 then 0 else n ^ k

Tactic:
cases k
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ (pow 0 : (a : ℕ) → ℕ) n = if Eq (α := ℕ) 0 0 ∧ n = 0 then 0 else HPow.hPow (β := ℕ) n 0

Tactic:
simp [pow]

Premises used: ArithmeticFunction.pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n n_1 : ℕ
⊢ (pow (n_1 + 1) : (a : ℕ) → ℕ) n = if n_1 + 1 = 0 ∧ n = 0 then 0 else n ^ (n_1 + 1)

Tactic:
simp [pow]

Premises used: ArithmeticFunction.pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
h : ∀ (n : ℕ), Eq (α := ℕ) ((pow 0 : (a : ℕ) → ℕ) n : ℕ) ((ζ : (a : ℕ) → ℕ) n : ℕ)
⊢ pow 0 = ζ

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((pow 0 : (a : ℕ) → ℕ) n : ℕ) ((ζ : (a : ℕ) → ℕ) n : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
h : ∀ (n : ℕ), Eq (α := ℕ) ((pow 1 : (a : ℕ) → ℕ) n : ℕ) ((ArithmeticFunction.id : (a : ℕ) → ℕ) n : ℕ)
⊢ pow 1 = ArithmeticFunction.id

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((pow 1 : (a : ℕ) → ℕ) n : ℕ) ((ArithmeticFunction.id : (a : ℕ) → ℕ) n : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k : ℕ
⊢ (pow k).IsMultiplicative

Tactic:
isMultiplicative_id.ppow

Premises used: ArithmeticFunction.IsMultiplicative.ppow, ArithmeticFunction.pow, ArithmeticFunction.isMultiplicative_id
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
k : ℕ
⊢ Eq (α := ℕ) ((fun (n : ℕ) ↦ (∑ d ∈ n.divisors, d ^ k : ℕ)) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (∑ d ∈ n.divisors, d ^ k : ℕ)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finset.sum, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
inl : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ) ↔ Eq (α := ℕ) 0 0
inr : ∀ (hn : n ≠ 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k : ℕ
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ) ↔ Eq (α := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn : n ≠ 0
inr : Eq (α := ℕ) (∑ d ∈ n.divisors, d ^ k) 0 ↔ n = 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0

Tactic:
simp only [ArithmeticFunction.sigma_apply]

Premises used: ArithmeticFunction.sigma_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (∑ d ∈ n.divisors, d ^ k) 0 ↔ n = 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
⊢ LT.lt (α := ℕ) (0 : ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k p i : ℕ
hp : Nat.Prime p
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) (p ^ i) : ℕ) (∑ j ∈ range (i + 1), p ^ (j * k) : ℕ)

Tactic:
simp [sigma_apply, divisors_prime_pow hp, pow_mul]

Premises used: Nat.divisors_prime_pow, ArithmeticFunction.sigma_apply, pow_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((σ 1 : (a : ℕ) → ℕ) n : ℕ) (∑ d ∈ n.divisors, d : ℕ)

Tactic:
simp [sigma_apply]

Premises used: ArithmeticFunction.sigma_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
p i : ℕ
hp : Nat.Prime p
⊢ Eq (α := ℕ) ((σ 1 : (a : ℕ) → ℕ) (p ^ i) : ℕ) (∑ k ∈ range (i + 1), p ^ k : ℕ)

Tactic:
simp [sigma_apply_prime_pow hp]

Premises used: ArithmeticFunction.sigma_apply_prime_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
rw : Eq (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, (n / d) ^ k)
rw₁ rw₂ : Eq (α := ℕ) (∑ d ∈ n.divisors, (n / d) ^ k) (∑ d ∈ n.divisors, (n / d) ^ k)
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (∑ d ∈ n.divisors, (n / d) ^ k : ℕ)

Tactic:
rw [sigma_apply, ← sum_div_divisors]

Premises used: ArithmeticFunction.sigma_apply, Nat.sum_div_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ (σ 0 : (a : ℕ) → ℕ) n = #n.divisors

Tactic:
simp [sigma_apply]

Premises used: ArithmeticFunction.sigma_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
p i : ℕ
hp : Nat.Prime p
⊢ (σ 0 : (a : ℕ) → ℕ) (p ^ i) = i + 1

Tactic:
simp [sigma_apply_prime_pow hp]

Premises used: ArithmeticFunction.sigma_apply_prime_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k : ℕ
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) 1 : ℕ) (1 : ℕ)

Tactic:
simp only [sigma_apply, divisors_one, sum_singleton, one_pow]

Premises used: one_pow, ArithmeticFunction.sigma_apply, Finset.sum_singleton, Nat.divisors_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : n ≠ 0
rwa : 0 < n
rwa₁ rwa₂ rwa₃ rwa₄ : n ≠ 0
⊢ LT.lt (α := ℕ) (0 : ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)

Tactic:
rwa [sigma_pos_iff, pos_iff_ne_zero]

Premises used: ArithmeticFunction.sigma_pos_iff, pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k k' n : ℕ
hk : k ≤ k'
simp_rw : LE.le (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, d ^ k')
⊢ LE.le (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) ((σ k' : (a : ℕ) → ℕ) n : ℕ)

Tactic:
simp_rw [sigma_apply]

Premises used: ArithmeticFunction.sigma_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k k' n : ℕ
hk : k ≤ k'
h : ∀ (d : ℕ) (hd : d ∈ n.divisors), 1 ≤ d
⊢ LE.le (α := ℕ) (∑ d ∈ n.divisors, d ^ k) (∑ d ∈ n.divisors, d ^ k')

Tactic:
gcongr with d hd
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k k' n : ℕ
hk : k ≤ k'
d : ℕ
hd : d ∈ n.divisors
⊢ 1 ≤ d

Tactic:
pos_of_mem_divisors hd

Premises used: Nat.pos_of_mem_divisors, Nat.lt
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k k' n : ℕ
hk : k ≤ k'
d : ℕ
hd : d ∈ n.divisors
⊢ 1 ≤ d

Tactic:
exact pos_of_mem_divisors hd

Premises used: Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k : ℕ
h : ∀ (x : ℕ), Eq (α := ℕ) ((ζ * pow k : (a : ℕ) → ℕ) x : ℕ) ((σ k : (a : ℕ) → ℕ) x : ℕ)
⊢ ζ * pow k = σ k

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k x : ℕ
h :
  Eq (α := ℕ) (∑ i ∈ x.divisors, (pow k : (a : ℕ) → ℕ) i : ℕ)
    (({ toFun := fun (n : ℕ) ↦ ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } : (a : ℕ) → ℕ) x : ℕ)
⊢ Eq (α := ℕ) ((ζ * pow k : (a : ℕ) → ℕ) x : ℕ) ((σ k : (a : ℕ) → ℕ) x : ℕ)

Tactic:
rw [sigma, zeta_mul_apply]

Premises used: ArithmeticFunction.sigma, ArithmeticFunction.zeta_mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k x : ℕ
h : ∀ x_1 ∈ x.divisors, (pow k : (a : ℕ) → ℕ) x_1 = x_1 ^ k
⊢ Eq (α := ℕ) (∑ i ∈ x.divisors, (pow k : (a : ℕ) → ℕ) i : ℕ)
    (({ toFun := fun (n : ℕ) ↦ ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } : (a : ℕ) → ℕ) x : ℕ)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k x : ℕ
⊢ ∀ x_1 ∈ x.divisors, (pow k : (a : ℕ) → ℕ) x_1 = x_1 ^ k

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k : ℕ
rw : (ζ * pow k).IsMultiplicative
⊢ (σ k).IsMultiplicative

Tactic:
rw [← zeta_mul_pow_eq_sigma]

Premises used: ArithmeticFunction.zeta_mul_pow_eq_sigma
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k : ℕ
⊢ (ζ * pow k).IsMultiplicative

Tactic:
apply isMultiplicative_zeta.mul isMultiplicative_pow

Premises used: ArithmeticFunction.isMultiplicative_zeta, ArithmeticFunction.isMultiplicative_pow, ArithmeticFunction.IsMultiplicative.mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn : n ≠ 0
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))
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)
    (∏ p ∈ n.primeFactors,
        ∑ i ∈ range (HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)), p ^ (i * k) :
      ℕ)

Tactic:
rw [isMultiplicative_sigma.multiplicative_factorization _ hn]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, ArithmeticFunction.isMultiplicative_sigma
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn : n ≠ 0
⊢ 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:
prod_congr n.support_factorization fun _ h ↦
    sigma_apply_prime_pow <| prime_of_mem_primeFactors h

Premises used: ArithmeticFunction.sigma_apply_prime_pow, Nat.support_factorization, Finset.prod_congr, Nat.prime_of_mem_primeFactors, Finsupp.prod
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn : n ≠ 0
⊢ 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:
exact prod_congr n.support_factorization fun _ h ↦
    sigma_apply_prime_pow <| prime_of_mem_primeFactors h

Premises used: ArithmeticFunction.sigma_apply_prime_pow, Nat.support_factorization, Finset.prod_congr, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
simp : ∑ d ∈ n.divisors, d ^ k ≤ n * n ^ k
⊢ (σ k : (a : ℕ) → ℕ) n ≤ n ^ (k + 1)

Tactic:
simp only [sigma_apply, pow_succ']

Premises used: Nat.pow_succ', ArithmeticFunction.sigma_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
⊢ ∑ d ∈ n.divisors, d ^ k ≤ n * n ^ k

Tactic:
(Finset.sum_le_sum fun d hd ↦ Nat.pow_le_pow_left (Nat.divisor_le hd) k).trans ?_

Premises used: Finset.sum_le_sum, LE.le.trans, Nat.divisor_le, Nat.pow_le_pow_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
refine : ∑ i ∈ n.divisors, n ^ k ≤ n * n ^ k
⊢ ∑ d ∈ n.divisors, d ^ k ≤ n * n ^ k

Tactic:
refine (Finset.sum_le_sum fun d hd ↦ Nat.pow_le_pow_left (Nat.divisor_le hd) k).trans ?_

Premises used: Finset.sum_le_sum, LE.le.trans, Nat.divisor_le, Nat.pow_le_pow_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
⊢ ∑ i ∈ n.divisors, n ^ k ≤ n * n ^ k

Tactic:
simpa [Finset.sum_const] using Nat.mul_le_mul_right (n ^ k) (Nat.card_divisors_le_self n)

Premises used: Nat.mul_le_mul_right, HPow.hPow, Nat.card_divisors_le_self, Finset.sum_const
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
rw :
  Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ (σ 0 : (a : ℕ) → ℕ) (p ^ k))
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ))
⊢ #n.divisors = ∏ x ∈ n.primeFactors, HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ)

Tactic:
rw [← sigma_zero_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]

Premises used: ArithmeticFunction.sigma_zero_apply, ArithmeticFunction.IsMultiplicative.multiplicative_factorization, ArithmeticFunction.isMultiplicative_sigma
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ (σ 0 : (a : ℕ) → ℕ) (p ^ k))
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ))

Tactic:
prod_congr n.support_factorization fun _ h =>
    sigma_zero_apply_prime_pow <| prime_of_mem_primeFactors h

Premises used: Nat.support_factorization, Finset.prod_congr, ArithmeticFunction.sigma_zero_apply_prime_pow, Nat.prime_of_mem_primeFactors, Finsupp.prod
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ (σ 0 : (a : ℕ) → ℕ) (p ^ k))
    (∏ x ∈ n.primeFactors, HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ))

Tactic:
exact prod_congr n.support_factorization fun _ h =>
    sigma_zero_apply_prime_pow <| prime_of_mem_primeFactors h

Premises used: Nat.support_factorization, Finset.prod_congr, ArithmeticFunction.sigma_zero_apply_prime_pow, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
inl : #(divisors 0) = 1 ↔ Eq (α := ℕ) 0 1
inr : ∀ (hn : n ≠ 0), #n.divisors = 1 ↔ n = 1
⊢ #n.divisors = 1 ↔ n = 1

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
⊢ #(divisors 0) = 1 ↔ Eq (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
h : n = 1
⊢ #n.divisors = 1

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
inr : ∀ (h : #n.divisors = 1), n = 1
⊢ #n.divisors = 1 ↔ n = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
h : #n.divisors = 1
⊢ n = 1

Tactic:
(card_le_one.mp h.le 1 (one_mem_divisors.mpr hn) n (n.mem_divisors_self hn)).symm

Premises used: Iff.mpr, Nat.one_mem_divisors, Eq.le, Finset.card_le_one, Iff.mp, OfNat.ofNat, Eq.symm, Nat.mem_divisors_self
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
h : #n.divisors = 1
⊢ n = 1

Tactic:
exact (card_le_one.mp h.le 1 (one_mem_divisors.mpr hn) n (n.mem_divisors_self hn)).symm

Premises used: Iff.mpr, Nat.one_mem_divisors, Eq.le, Finset.card_le_one, Iff.mp, OfNat.ofNat, Eq.symm, Nat.mem_divisors_self
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ Eq (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1

Tactic:
simp [sigma_zero_apply]

Premises used: ArithmeticFunction.sigma_zero_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
pos : ∀ (hn0 : n = 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
neg : ∀ (hn0 : ¬n = 0), Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : n = 0
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : ¬n = 0
neg : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) → n = 1
neg₁ : n = 1 → Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
⊢ Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ) ↔ n = 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
neg : Eq (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
⊢ n = 1

Tactic:
rw [← sigma_zero_eq_one_iff]

Premises used: _private.0.ArithmeticFunction.sigma_zero_eq_one_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
⊢ LT.lt (α := ℕ) (0 : ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ)

Tactic:
have zero_lt_sigma := sigma_pos 0 n hn0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
zero_lt_sigma : LT.lt (α := ℕ) (0 : ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ)
⊢ LE.le (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)

Tactic:
have sigma_zero_le_sigma := sigma_mono 0 k n k.zero_le
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : ¬n = 0
h : Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)
zero_lt_sigma : LT.lt (α := ℕ) (0 : ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ)
sigma_zero_le_sigma : LE.le (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ)
⊢ Eq (α := ℕ) ((σ 0 : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
k n : ℕ
hn0 : ¬n = 0
⊢ n = 1 → Eq (α := ℕ) ((σ k : (a : ℕ) → ℕ) n : ℕ) (1 : ℕ)

Tactic:
simp +contextual
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
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)
⊢ Eq (α := ℕ) (∑ d ∈ n.divisors, d)
    (∏ p ∈ n.primeFactors,
      ∑ k ∈ range (HAdd.hAdd (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)), p ^ k)

Tactic:
rw [← sigma_one_apply, isMultiplicative_sigma.multiplicative_factorization _ hn]

Premises used: ArithmeticFunction.IsMultiplicative.multiplicative_factorization, ArithmeticFunction.sigma_one_apply, ArithmeticFunction.isMultiplicative_sigma
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
⊢ 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:
prod_congr n.support_factorization fun _ h =>
    sigma_one_apply_prime_pow <| prime_of_mem_primeFactors h

Premises used: ArithmeticFunction.sigma_one_apply_prime_pow, Nat.support_factorization, Finset.prod_congr, Nat.prime_of_mem_primeFactors, Finsupp.prod
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
hn : n ≠ 0
⊢ 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:
exact prod_congr n.support_factorization fun _ h =>
    sigma_one_apply_prime_pow <| prime_of_mem_primeFactors h

Premises used: ArithmeticFunction.sigma_one_apply_prime_pow, Nat.support_factorization, Finset.prod_congr, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_1
⊢ Eq (α := ℕ) ((fun (n : ℕ) ↦ n.primeFactorsList.length) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
⊢ (Ω : (a : ℕ) → ℕ) n = n.primeFactorsList.length

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) 1 : ℕ) (0 : ℕ)

Tactic:
simp [cardFactors_apply]

Premises used: ArithmeticFunction.cardFactors_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
rw : n.primeFactorsList.length = 0 ↔ n = 0 ∨ n = 1
rw₁ : n.primeFactorsList = [] ↔ n = 0 ∨ n = 1
rw₂ rw₃ : n = 0 ∨ n = 1 ↔ n = 0 ∨ n = 1
⊢ Eq (α := ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) (0 : ℕ) ↔ n = 0 ∨ n = 1

Tactic:
rw [cardFactors_apply, List.length_eq_zero_iff, primeFactorsList_eq_nil]

Premises used: ArithmeticFunction.cardFactors_apply, Nat.primeFactorsList_eq_nil, List.length_eq_zero_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
n : ℕ
rw : 0 < n.primeFactorsList.length ↔ 1 < n
rw₁ : n.primeFactorsList ≠ [] ↔ 1 < n
rw₂ rw₃ : 1 < n ↔ 1 < n
⊢ LT.lt (α := ℕ) (0 : ℕ) ((Ω : (a : ℕ) → ℕ) n : ℕ) ↔ 1 < n

Tactic:
rw [cardFactors_apply, List.length_pos_iff, primeFactorsList_ne_nil]

Premises used: ArithmeticFunction.cardFactors_apply, List.length_pos_iff, Nat.primeFactorsList_ne_nil