awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ 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
have rw : ∀ x ∈ n.divisorsAntidiagonal,
  (Units.coeHom R : (a : Rˣ) → R)
      (HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) sorry else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
    HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
Tactic: rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ (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 : ℤ)
have rw : (Units.coeHom R : (a : Rˣ) → R) (HPow.hPow (β := ℤ) (Units.mk0 (g x.2) sorry) ((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ (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 : ℤ)
have rw₁ : (↑(HPow.hPow (β := ℤ) (Units.mk0 (g x.2) sorry) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) : R) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ (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 : ℤ)
have rw₂ : HPow.hPow (β := ℤ) (↑(Units.mk0 (g x.2) sorry) : R) ((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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 : ℤ)
⊢ (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 : ℤ)
have rw₃ : HPow.hPow (β := ℤ) (g x.2) ((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ)
have rw : 0 ≤ if IsPrimePow n then Real.log (↑n.minFac : ℝ) else 0
Tactic: rw [vonMangoldt_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log (↑n.minFac : ℝ) else 0
have pos : IsPrimePow n → 0 ≤ Real.log (↑n.minFac : ℝ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
pos : IsPrimePow n → 0 ≤ Real.log (↑n.minFac : ℝ)
⊢ 0 ≤ if IsPrimePow n then Real.log (↑n.minFac : ℝ) else 0
have neg : ¬IsPrimePow n → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
p : ℕ
hp : Nat.Prime p
⊢ (Λ : (a : ℕ) → ℝ) p = Real.log (↑p : ℝ)
have rw : (if IsPrimePow p then Real.log (↑p.minFac : ℝ) else 0) = Real.log (↑p : ℝ)
Tactic: rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
p : ℕ
hp : Nat.Prime p
rw : (if IsPrimePow p then Real.log (↑p.minFac : ℝ) else 0) = Real.log (↑p : ℝ)
⊢ (Λ : (a : ℕ) → ℝ) p = Real.log (↑p : ℝ)
have rw₁ : (if IsPrimePow p then Real.log (↑p : ℝ) else 0) = Real.log (↑p : ℝ)
Tactic: rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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 : ℝ)
⊢ (Λ : (a : ℕ) → ℝ) p = Real.log (↑p : ℝ)
have rw₂ : Real.log (↑p : ℝ) = Real.log (↑p : ℝ)
Tactic: rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n
have inl : Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) 1 : ℝ) (0 : ℝ) ↔ IsPrimePow (R := ℕ) 1
Tactic: rcases eq_or_ne n 1 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
inl : Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) 1 : ℝ) (0 : ℝ) ↔ IsPrimePow (R := ℕ) 1
⊢ Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n
have inr : ∀ (hn : n ≠ 1), Ne (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) ↔ IsPrimePow n
Tactic: rcases eq_or_ne n 1 with (rfl | hn)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ ∑ i ∈ n.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑n : ℝ)
have refine_1 : ∑ i ∈ divisors 0, (Λ : (a : ℕ) → ℝ) i = Real.log (↑0 : ℝ)
Tactic: refine recOnPrimeCoprime ?_ ?_ ?_ n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
refine_1 : ∑ i ∈ divisors 0, (Λ : (a : ℕ) → ℝ) i = Real.log (↑0 : ℝ)
⊢ ∑ i ∈ n.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑n : ℝ)
have refine_2 : ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(p ^ n) : ℝ)
Tactic: refine recOnPrimeCoprime ?_ ?_ ?_ n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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) : ℝ)
⊢ ∑ i ∈ n.divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑n : ℝ)
have 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) : ℝ)
Tactic: refine recOnPrimeCoprime ?_ ?_ ?_ n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ i ∈ (p ^ k).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(p ^ k) : ℝ)
have refine_2 : HAdd.hAdd (α := ℝ) (∑ k ∈ range k, (Λ : (a : ℕ) → ℝ) (p ^ (k + 1))) 0 = (↑k : ℝ) * Real.log (↑p : ℝ)
Tactic: rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero,
      vonMangoldt_apply_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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 : ℝ)
⊢ ∑ i ∈ (a * b).divisors, (Λ : (a : ℕ) → ℝ) i = Real.log (↑(a * b) : ℝ)
have 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) : ℝ)
Tactic: simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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 : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have refine_3 : ∑ a ∈ a.divisors ∪ 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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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) : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have refine_3₁ : ∑ a ∈ {d ∈ a.divisors | IsPrimePow d} ∪ {d ∈ b.divisors | IsPrimePow d}, 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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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) : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have 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) : ℝ)
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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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) : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have refine_3₃ : Real.log (↑a : ℝ) + ∑ x ∈ b.divisors with IsPrimePow x, Real.log (↑x.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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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) : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have refine_3₄ : Real.log (↑a : ℝ) + Real.log (↑b : ℝ) = 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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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) : ℝ)
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have refine_3₅ : Real.log (↑a : ℝ) + Real.log (↑b : ℝ) = Real.log (HMul.hMul (α := ℝ) (↑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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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 : ℝ))
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log (↑a.minFac : ℝ) = Real.log (↑(a * b) : ℝ)
have refine_3₆ : Real.log (↑a : ℝ) + Real.log (↑b : ℝ) = Real.log (↑a : ℝ) + Real.log (↑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')]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
⊢ Λ * (↑ζ : ArithmeticFunction ℝ) = log
have h : ∀ (n : ℕ), Eq (α := ℝ) ((Λ * (↑ζ : ArithmeticFunction ℝ) : (a : ℕ) → ℝ) n : ℝ) ((log : (a : ℕ) → ℝ) n : ℝ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ Eq (α := ℝ) ((Λ * (↑ζ : ArithmeticFunction ℝ) : (a : ℕ) → ℝ) n : ℝ) ((log : (a : ℕ) → ℝ) n : ℝ)
have h : Real.log (↑n : ℝ) = (log : (a : ℕ) → ℝ) n
Tactic: rw [coe_mul_zeta_apply, vonMangoldt_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
⊢ (↑ζ : ArithmeticFunction ℝ) * Λ = log
have rw : Λ * (↑ζ : ArithmeticFunction ℝ) = log
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
⊢ log * (↑μ : ArithmeticFunction ℝ) = Λ
have rw : Λ * (↑ζ : ArithmeticFunction ℝ) * (↑μ : ArithmeticFunction ℝ) = Λ
Tactic: rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
rw : Λ * (↑ζ : ArithmeticFunction ℝ) * (↑μ : ArithmeticFunction ℝ) = Λ
⊢ log * (↑μ : ArithmeticFunction ℝ) = Λ
have rw₁ : Λ * HMul.hMul (α := ArithmeticFunction ℝ) (↑ζ : ArithmeticFunction ℝ) (↑μ : ArithmeticFunction ℝ) = Λ
Tactic: rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
rw : Λ * (↑ζ : ArithmeticFunction ℝ) * (↑μ : ArithmeticFunction ℝ) = Λ
rw₁ : Λ * HMul.hMul (α := ArithmeticFunction ℝ) (↑ζ : ArithmeticFunction ℝ) (↑μ : ArithmeticFunction ℝ) = Λ
⊢ log * (↑μ : ArithmeticFunction ℝ) = Λ
have rw₂ : Λ * 1 = Λ
Tactic: rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
rw : Λ * (↑ζ : ArithmeticFunction ℝ) * (↑μ : ArithmeticFunction ℝ) = Λ
rw₁ : Λ * HMul.hMul (α := ArithmeticFunction ℝ) (↑ζ : ArithmeticFunction ℝ) (↑μ : ArithmeticFunction ℝ) = Λ
rw₂ : Λ * 1 = Λ
⊢ log * (↑μ : ArithmeticFunction ℝ) = Λ
have rw₃ : Λ = Λ
Tactic: rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
⊢ (↑μ : ArithmeticFunction ℝ) * log = Λ
have rw : log * (↑μ : ArithmeticFunction ℝ) = Λ
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ Eq (α := ℝ)
    (∑ d ∈ n.divisors, HMul.hMul (α := ℝ) (β := ℝ) ((↑((μ : (a : ℕ) → ℤ) d) : ℝ) : ℝ) ((log : (a : ℕ) → ℝ) d : ℝ) : ℝ)
    (-(Λ : (a : ℕ) → ℝ) n : ℝ)
have simp : Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
  (∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : ℝ) * -Real.log (↑x.2 : ℝ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : ℝ) * -Real.log (↑x.2 : ℝ))
have rw : Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
  (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
Tactic: rw [sum_divisorsAntidiagonal fun i j => (μ i : ℝ) * -Real.log j]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
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 : ℝ)))
have apply : ∀ x ∈ n.divisors,
  (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * -Real.log (↑(n / x) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ) - (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑n : ℝ)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * -Real.log (↑(n / x) : ℝ) =
      (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ) - (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑n : ℝ)
have simp : ∀ (x : ℕ),
  x ∣ n →
    ¬n = 0 →
      (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * -Real.log (↑(n / x) : ℝ) =
        (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ) - (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑n : ℝ)
Tactic: simp only [and_imp, Ne, mem_divisors]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ Ne (α := ℝ) (↑m : ℝ) 0
have rw : m ≠ 0
Tactic: rw [cast_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (hypothesis)
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (↑(n / m) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
have this : Ne (α := ℝ) (↑m : ℝ) 0
Tactic: have : (m : ℝ) ≠ 0 := by
      rw [cast_ne_zero]
      rintro rfl
      exact hn (by simpa using mn)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : Ne (α := ℝ) (↑m : ℝ) 0
⊢ (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (↑(n / m) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
have rw : (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (HDiv.hDiv (α := ℝ) (↑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]