case refine'_1
n : ℕ
⊢ ∑ i in divisors 0, ↑Λ i = Real.log ↑0

case refine'_2
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → ∑ i in divisors (p ^ n), ↑Λ i = Real.log ↑(p ^ n)

case refine'_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          ∑ i in divisors a, ↑Λ i = Real.log ↑a →
            ∑ i in divisors b, ↑Λ i = Real.log ↑b → ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
n : ℕ
⊢ ∑ i in divisors n, ↑Λ i = Real.log ↑n
refine' recOnPrimeCoprime _ _ _ n
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ i in divisors a, ↑Λ i = Real.log ↑a
hb : ∑ i in divisors b, ↑Λ i = Real.log ↑b
⊢ ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
case refine'_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        coprime a b →
          ∑ i in divisors a, ↑Λ i = Real.log ↑a →
            ∑ i in divisors b, ↑Λ i = Real.log ↑b → ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
intro a b ha' hb' hab ha hb
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ a in filter (fun a => IsPrimePow a) (divisors a), Real.log ↑(minFac a) = Real.log ↑a
hb : ∑ a in filter (fun a => IsPrimePow a) (divisors b), Real.log ↑(minFac a) = Real.log ↑b
⊢ ∑ a in filter (fun a => IsPrimePow a) (divisors (a * b)), Real.log ↑(minFac a) = Real.log ↑(a * b)
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ i in divisors a, ↑Λ i = Real.log ↑a
hb : ∑ i in divisors b, ↑Λ i = Real.log ↑b
⊢ ∑ i in divisors (a * b), ↑Λ i = Real.log ↑(a * b)
simp only [vonMangoldt_apply, ← sum_filter] at ha hb⊢
no goals
case refine'_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : coprime a b
ha : ∑ a in filter (fun a => IsPrimePow a) (divisors a), Real.log ↑(minFac a) = Real.log ↑a
hb : ∑ a in filter (fun a => IsPrimePow a) (divisors b), Real.log ↑(minFac a) = Real.log ↑b
⊢ ∑ a in filter (fun a => IsPrimePow a) (divisors (a * b)), Real.log ↑(minFac a) = Real.log ↑(a * b)
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')]
no goals
case refine'_1
n : ℕ
⊢ ∑ i in divisors 0, ↑Λ i = Real.log ↑0
simp
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ i in divisors (p ^ k), ↑Λ i = Real.log ↑(p ^ k)
case refine'_2
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → ∑ i in divisors (p ^ n), ↑Λ i = Real.log ↑(p ^ n)
intro p k hp
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ k in range k, ↑Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ i in divisors (p ^ k), ↑Λ i = Real.log ↑(p ^ k)
rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', pow_zero,
  vonMangoldt_apply_one]
no goals
case refine'_2
n p k : ℕ
hp : Prime p
⊢ ∑ k in range k, ↑Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p
simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]