awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
rw :
  ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R : (a : Rˣ) → R)
        (HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
      HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
⊢ n ∈ s →
      Eq.{u_1 + 1} (α := Rˣ)
        (∏ x ∈ n.divisorsAntidiagonal,
          HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
        (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]

Premises used: dif_pos, Finset.prod_congr, map_prod, Units.val_inj, Units.coeHom_apply, Units.val_mk0, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ n.divisorsAntidiagonal
rw :
  (Units.coeHom R : (a : Rˣ) → R) (HPow.hPow (β := ℤ) (Units.mk0 (g x.2) ⋯) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
rw₁ :
  (↑(HPow.hPow (β := ℤ) (Units.mk0 (g x.2) ⋯) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) : R) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
rw₂ :
  HPow.hPow (β := ℤ) (↑(Units.mk0 (g x.2) ⋯) : R) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
rw₃ rw₄ :
  HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
⊢ (Units.coeHom R : (a : Rˣ) → R)
      (HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)

Tactic:
rw [dif_pos (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)),
      Units.coeHom_apply, Units.val_zpow_eq_zpow_val, Units.val_mk0]

Premises used: Nat.snd_mem_divisors_of_mem_antidiagonal, dif_pos, Units.val_zpow_eq_zpow_val, Units.coeHom_apply, Units.val_mk0, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
⊢ Eq (α := ℝ) ((fun (n : ℕ) ↦ Real.log (↑n : ℝ)) 0) 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ (log : (a : ℕ) → ℝ) n = Real.log (↑n : ℝ)

Tactic:
rfl

Premises used: Real.log, dite, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ (Λ : (a : ℕ) → ℝ) n = if IsPrimePow n then Real.log (↑n.minFac : ℝ) else 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) 1 : ℝ) (0 : ℝ)

Tactic:
simp [vonMangoldt_apply]

Premises used: ArithmeticFunction.vonMangoldt_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
rw : 0 ≤ if IsPrimePow n then Real.log (↑n.minFac : ℝ) else 0
⊢ LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ)

Tactic:
rw [vonMangoldt_apply]

Premises used: ArithmeticFunction.vonMangoldt_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
pos : IsPrimePow n → 0 ≤ Real.log (↑n.minFac : ℝ)
neg : ¬IsPrimePow n → LE.le (α := ℝ) 0 0
⊢ 0 ≤ if IsPrimePow n then Real.log (↑n.minFac : ℝ) else 0

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
h : IsPrimePow n
⊢ 0 ≤ Real.log (↑n.minFac : ℝ)

Tactic:
Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))

Premises used: Iff.mpr, Nat.one_le_cast, Real.log_nonneg, Nat.minFac_pos
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
h : IsPrimePow n
⊢ 0 ≤ Real.log (↑n.minFac : ℝ)

Tactic:
exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))

Premises used: Iff.mpr, Nat.one_le_cast, Real.log_nonneg, Nat.minFac_pos
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
h : ¬IsPrimePow n
⊢ LE.le (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n k : ℕ
hk : k ≠ 0
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) (n ^ k) : ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ)

Tactic:
simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk]

Premises used: ArithmeticFunction.vonMangoldt_apply, Nat.pow_minFac, isPrimePow_pow_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
p : ℕ
hp : Nat.Prime p
rw : (if IsPrimePow p then Real.log (↑p.minFac : ℝ) else 0) = Real.log (↑p : ℝ)
rw₁ : (if IsPrimePow p then Real.log (↑p : ℝ) else 0) = Real.log (↑p : ℝ)
rw₂ rw₃ : Real.log (↑p : ℝ) = Real.log (↑p : ℝ)
⊢ (Λ : (a : ℕ) → ℝ) p = Real.log (↑p : ℝ)

Tactic:
rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]

Premises used: Nat.Prime.minFac_eq, Nat.Prime.prime, if_pos, ArithmeticFunction.vonMangoldt_apply, Prime.isPrimePow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
inl : Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) 1 : ℝ) (0 : ℝ) ↔ IsPrimePow (R := ℕ) 1
inr : ∀ (hn : n ≠ 1), Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n
⊢ Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n

Tactic:
rcases eq_or_ne n 1 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
⊢ Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) 1 : ℝ) (0 : ℝ) ↔ IsPrimePow (R := ℕ) 1

Tactic:
simp [not_isPrimePow_one]

Premises used: not_isPrimePow_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
hn : n ≠ 1
⊢ Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n

Tactic:
(Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff

Premises used: Iff.mpr, Ne.ite_ne_right_iff, Nat.Prime.one_lt, Real.log_pos, LT.lt.ne', Nat.one_lt_cast, Nat.minFac_prime, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
hn : n ≠ 1
⊢ Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n

Tactic:
exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff

Premises used: Iff.mpr, Ne.ite_ne_right_iff, Nat.Prime.one_lt, Real.log_pos, LT.lt.ne', Nat.one_lt_cast, Nat.minFac_prime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ LT.lt (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) ↔ IsPrimePow n

Tactic:
vonMangoldt_nonneg.lt_iff_ne.trans (ne_comm.trans vonMangoldt_ne_zero_iff)

Premises used: ArithmeticFunction.vonMangoldt_ne_zero_iff, ArithmeticFunction.vonMangoldt_nonneg, LE.le.lt_iff_ne, Iff.trans, ne_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ ¬IsPrimePow n

Tactic:
vonMangoldt_ne_zero_iff.not_right

Premises used: ArithmeticFunction.vonMangoldt_ne_zero_iff, Iff.not_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ ∑ i ∈ n.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑n : ℝ)

Tactic:
recOnPrimeCoprime ?_ ?_ ?_ n

Premises used: Nat.recOnPrimeCoprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
refine_1 : ∑ i ∈ divisors 0, (Λ : (a : ℕ) → ℝ) i = Real.log (↑0 : ℝ)
refine_2 : ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(p ^ n) : ℝ)
refine_3 :
  ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑a : ℝ) →
            ∑ i ∈ b.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑b : ℝ) →
              ∑ i ∈ (a * b).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(a * b) : ℝ)
⊢ ∑ i ∈ n.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑n : ℝ)

Tactic:
refine recOnPrimeCoprime ?_ ?_ ?_ n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ ∑ i ∈ divisors 0, (Λ : (a : ℕ) → ℝ) i = Real.log (↑0 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n p k : ℕ
hp : Nat.Prime p
refine_2 : HAdd.hAdd (α := ℝ) (∑ k ∈ range k, (Λ : (a : ℕ) → ℝ) (p ^ (k + 1))) 0 = (↑k : ℝ) * Real.log (↑p : ℝ)
⊢ ∑ i ∈ (p ^ k).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(p ^ k) : ℝ)

Tactic:
rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero,
      vonMangoldt_apply_one]

Premises used: Nat.pow_zero, Nat.sum_divisors_prime_pow, ArithmeticFunction.vonMangoldt_apply_one, Real.log_pow, Nat.cast_pow, Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n p k : ℕ
hp : Nat.Prime p
⊢ HAdd.hAdd (α := ℝ) (∑ k ∈ range k, (Λ : (a : ℕ) → ℝ) (p ^ (k + 1))) 0 = (↑k : ℝ) * Real.log (↑p : ℝ)

Tactic:
simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]

Premises used: Nat.succ_ne_zero, ArithmeticFunction.vonMangoldt_apply_prime, ArithmeticFunction.vonMangoldt_apply_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ i ∈ a.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑a : ℝ)
hb : ∑ i ∈ b.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑b : ℝ)
refine_3 :
  ∀ (ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑a : ℝ))
    (hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑b : ℝ)),
    ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
⊢ ∑ i ∈ (a * b).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(a * b) : ℝ)

Tactic:
simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢

Premises used: ArithmeticFunction.vonMangoldt_apply, Finset.sum_filter
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑a : ℝ)
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑b : ℝ)
refine_3 : ∑ a ∈ a.divisors ∪ b.divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
refine_3₁ :
  ∑ a ∈ {d ∈ a.divisors | IsPrimePow d} ∪ {d ∈ b.divisors | IsPrimePow d}, Real.log (↑a.minFac : ℝ) =
    Real.log (↑(a * b) : ℝ)
refine_3₂ :
  HAdd.hAdd (α := ℝ) (∑ x ∈ a.divisors with IsPrimePow x, Real.log (↑x.minFac : ℝ))
      (∑ x ∈ b.divisors with IsPrimePow x, Real.log (↑x.minFac : ℝ)) =
    Real.log (↑(a * b) : ℝ)
refine_3₃ : Real.log (↑a : ℝ) + ∑ x ∈ b.divisors with IsPrimePow x, Real.log (↑x.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
refine_3₄ : Real.log (↑a : ℝ) + Real.log (↑b : ℝ) = Real.log (↑(a * b) : ℝ)
refine_3₅ : Real.log (↑a : ℝ) + Real.log (↑b : ℝ) = Real.log (HMul.hMul (α := ℝ) (↑a : ℝ) (↑b : ℝ))
refine_3₆ refine_3₇ : Real.log (↑a : ℝ) + Real.log (↑b : ℝ) = Real.log (↑a : ℝ) + Real.log (↑b : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)

Tactic:
rw [mul_divisors_filter_prime_pow hab, filter_union,
    sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb, Nat.cast_mul,
    Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')]

Premises used: Iff.mpr, Nat.disjoint_divisors_filter_isPrimePow, pos_of_gt, Finset.sum_union, LT.lt.ne', Nat.cast_mul, Finset.filter_union, Nat.mul_divisors_filter_prime_pow, Real.log_mul, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
h : ∀ (n : ℕ), Eq (α := ℝ) ((Λ * (↑ζ : ArithmeticFunction ℝ) : (a : ℕ) → ℝ) n : ℝ) ((log : (a : ℕ) → ℝ) n : ℝ)
⊢ Λ * (↑ζ : ArithmeticFunction ℝ) = log

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
h : Real.log (↑n : ℝ) = (log : (a : ℕ) → ℝ) n
⊢ Eq (α := ℝ) ((Λ * (↑ζ : ArithmeticFunction ℝ) : (a : ℕ) → ℝ) n : ℝ) ((log : (a : ℕ) → ℝ) n : ℝ)

Tactic:
rw [coe_mul_zeta_apply, vonMangoldt_sum]

Premises used: ArithmeticFunction.vonMangoldt_sum, ArithmeticFunction.coe_mul_zeta_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ Real.log (↑n : ℝ) = (log : (a : ℕ) → ℝ) n

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
rw : Λ * (↑ζ : ArithmeticFunction ℝ) = log
⊢ (↑ζ : ArithmeticFunction ℝ) * Λ = log

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
⊢ Λ * (↑ζ : ArithmeticFunction ℝ) = log

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
rw : Λ * (↑ζ : ArithmeticFunction ℝ) * (↑μ : ArithmeticFunction ℝ) = Λ
rw₁ : Λ * HMul.hMul (α := ArithmeticFunction ℝ) (↑ζ : ArithmeticFunction ℝ) (↑μ : ArithmeticFunction ℝ) = Λ
rw₂ : Λ * 1 = Λ
rw₃ rw₄ : Λ = Λ
⊢ log * (↑μ : ArithmeticFunction ℝ) = Λ

Tactic:
rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]

Premises used: mul_assoc, ArithmeticFunction.coe_zeta_mul_coe_moebius, mul_one, ArithmeticFunction.vonMangoldt_mul_zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
rw : log * (↑μ : ArithmeticFunction ℝ) = Λ
⊢ (↑μ : ArithmeticFunction ℝ) * log = Λ

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
⊢ log * (↑μ : ArithmeticFunction ℝ) = Λ

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
simp :
  Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : ℝ) * -Real.log (↑x.2 : ℝ))
⊢ Eq (α := ℝ)
    (∑ d ∈ n.divisors, HMul.hMul (α := ℝ) (β := ℝ) ((↑((μ : (a : ℕ) → ℤ) d) : ℝ) : ℝ) ((log : (a : ℕ) → ℝ) d : ℝ) : ℝ)
    (-(Λ : (a : ℕ) → ℝ) n : ℝ)

Tactic:
simp only [← log_mul_moebius_eq_vonMangoldt, mul_comm log, mul_apply, log_apply, intCoe_apply, ←
    Finset.sum_neg_distrib, neg_mul_eq_mul_neg]

Premises used: ArithmeticFunction.log_apply, ArithmeticFunction.log, ArithmeticFunction.log_mul_moebius_eq_vonMangoldt, neg_mul_eq_mul_neg, mul_comm, ArithmeticFunction.mul_apply, Finset.sum_neg_distrib, ArithmeticFunction.intCoe_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
rw :
  Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
⊢ Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : ℝ) * -Real.log (↑x.2 : ℝ))

Tactic:
rw [sum_divisorsAntidiagonal fun i j => (μ i : ℝ) * -Real.log j]

Premises used: Int.cast, HMul.hMul, Nat.cast, Real.log, ArithmeticFunction.moebius, DFunLike.coe, Neg.neg, Nat.sum_divisorsAntidiagonal
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
apply :
  ∀ x ∈ n.divisors,
    (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * -Real.log (↑(n / x) : ℝ) =
      (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ) - (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑n : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
simp :
  ∀ (x : ℕ),
    x ∣ n →
      ¬n = 0 →
        (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * -Real.log (↑(n / x) : ℝ) =
          (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ) - (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑n : ℝ)
⊢ ∀ x ∈ n.divisors,
    (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * -Real.log (↑(n / x) : ℝ) =
      (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ) - (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑n : ℝ)

Tactic:
simp only [and_imp, Ne, mem_divisors]

Premises used: Nat.mem_divisors, and_imp, Ne
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
rw : m ≠ 0
⊢ Ne (α := ℝ) (↑m : ℝ) 0

Tactic:
rw [cast_ne_zero]

Premises used: Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0

Tactic:
simpa using mn
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False

Tactic:
exact hn (by simpa using mn)
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ Ne (α := ℝ) (↑m : ℝ) 0

Tactic:
have : (m : ℝ) ≠ 0 := by
      rw [cast_ne_zero]
      rintro rfl
      exact hn (by simpa using mn)
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
rw₁ :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -(Real.log (↑n : ℝ) - Real.log (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
rw₂ :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * (Real.log (↑m : ℝ) - Real.log (↑n : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
rw₃ rw₄ :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
⊢ (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (↑(n / m) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)

Tactic:
rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]

Premises used: Iff.mpr, neg_sub, mul_sub, Real.log_div, Nat.cast_div, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))

Tactic:
have : (∑ i ∈ n.divisors, (μ i : ℝ) * -Real.log (n / i : ℕ)) =
      ∑ i ∈ n.divisors, ((μ i : ℝ) * Real.log i - μ i * Real.log n) := by
    apply sum_congr rfl
    simp only [and_imp, Ne, mem_divisors]
    intro m mn hn
    have : (m : ℝ) ≠ 0 := by
      rw [cast_ne_zero]
      rintro rfl
      exact hn (by simpa using mn)
    rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
rw : (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
⊢ Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))

Tactic:
rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self,
    moebius_mul_coe_zeta]

Premises used: ArithmeticFunction.moebius_mul_coe_zeta, Int.cast_sum, sub_eq_self, eq_comm, Finset.sum_sub_distrib, ArithmeticFunction.coe_mul_zeta_apply, Finset.sum_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
inl : ∀ (hn : n = 1), (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
inr : ∀ (hn : n ≠ 1), (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
⊢ (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0

Tactic:
rcases eq_or_ne n 1 with (hn | hn)

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
hn : n = 1
⊢ (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
hn : n ≠ 1
⊢ (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0

Tactic:
simp [hn]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
⊢ (Λ : (a : ℕ) → ℝ) 0 ≤ Real.log (↑0 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
rw : LE.le (α := ℝ) ((Λ : (a : ℕ) → ℝ) (n + 1) : ℝ) (∑ i ∈ (n + 1).divisors, (Λ : (a : ℕ) → ℝ) i : ℝ)
⊢ (Λ : (a : ℕ) → ℝ) (n + 1) ≤ Real.log (↑(n + 1) : ℝ)

Tactic:
rw [← vonMangoldt_sum]

Premises used: ArithmeticFunction.vonMangoldt_sum
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ ∀ i ∈ (n + 1).divisors, LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) i : ℝ)

Tactic:
fun _ _ => vonMangoldt_nonneg

Premises used: ArithmeticFunction.vonMangoldt_nonneg
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ ∀ i ∈ (n + 1).divisors, LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) i : ℝ)

Tactic:
exact fun _ _ => vonMangoldt_nonneg

Premises used: ArithmeticFunction.vonMangoldt_nonneg
-- Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
Goal:
n : ℕ
⊢ LE.le (α := ℝ) ((Λ : (a : ℕ) → ℝ) (n + 1) : ℝ) (∑ i ∈ (n + 1).divisors, (Λ : (a : ℕ) → ℝ) i : ℝ)

Tactic:
exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
      (mem_divisors_self _ n.succ_ne_zero)

Premises used: Nat.succ_ne_zero, Finset.single_le_sum, Nat.mem_divisors_self
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
x : ℕ
⊢ Eq (α := ℕ) ((ζ : (a : ℕ) → ℕ) x : ℕ) (if x = 0 then 0 else 1 : ℕ)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
x : ℕ
h : x ≠ 0
⊢ Eq (α := ℕ) ((ζ : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
x : ℕ
⊢ Eq (α := ℕ) ((ζ : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ) ↔ x = 0

Tactic:
simp [zeta]

Premises used: ArithmeticFunction.zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
x : ℕ
⊢ LT.lt (α := ℕ) (0 : ℕ) ((ζ : (a : ℕ) → ℕ) x : ℕ) ↔ 0 < x

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
rw :
  Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
⊢ Eq (α := M)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → M) x : M)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i : M)

Tactic:
rw [smul_apply]

Premises used: ArithmeticFunction.smul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
trans :
  Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2)
trans₁ :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)

Tactic:
trans ∑ i ∈ divisorsAntidiagonal x, f i.snd

Premises used: Nat.divisorsAntidiagonal