-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_sum {n : ℕ} : ∑ i ∈ n.divisors, Λ i = Real.log n

Proof state:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ i ∈ (p ^ k).divisors, Λ 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]

Result:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ k ∈ range k, Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p

Proof state:
case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
intro a b ha' hb' hab ha hb

Result:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ i ∈ a.divisors, Λ i = Real.log ↑a
hb : ∑ i ∈ b.divisors, Λ i = Real.log ↑b
⊢ ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Proof state:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ filter (fun a => IsPrimePow a) a.divisors, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ filter (fun a => IsPrimePow a) b.divisors, Real.log ↑a.minFac = Real.log ↑b
⊢ ∑ a ∈ filter (fun a => IsPrimePow a) (a * b).divisors, 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')]

Result:
no goals

Proof state:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ k ∈ range k, Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p

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

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ i ∈ n.divisors, Λ i = Real.log ↑n

Tactic:
refine recOnPrimeCoprime ?_ ?_ ?_ n

Result:
case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0

case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Proof state:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ i ∈ a.divisors, Λ i = Real.log ↑a
hb : ∑ i ∈ b.divisors, Λ i = Real.log ↑b
⊢ ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

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

Result:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ filter (fun a => IsPrimePow a) a.divisors, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ filter (fun a => IsPrimePow a) b.divisors, Real.log ↑a.minFac = Real.log ↑b
⊢ ∑ a ∈ filter (fun a => IsPrimePow a) (a * b).divisors, Real.log ↑a.minFac = Real.log ↑(a * b)

Proof state:
case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

Tactic:
intro p k hp

Result:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ i ∈ (p ^ k).divisors, Λ i = Real.log ↑(p ^ k)

Proof state:
case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0

Tactic:
simp

Result:
no goals