-- Mathlib/NumberTheory/VonMangoldt.lean
theorem sum_moebius_mul_log_eq {n : ℕ} : (∑ d ∈ n.divisors, (μ d : ℝ) * log d) = -Λ n

Proof state:
n : ℕ
⊢ ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)

Tactic:
apply sum_congr rfl

Result:
n : ℕ
⊢ ∀ x ∈ n.divisors, ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Proof state:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n

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

Result:
no goals

Proof state:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ i ∈ n.divisors, ↑(μ 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]

Result:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ↑(1 n) * Real.log ↑n = 0

Proof state:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑m ≠ 0

Tactic:
rw [cast_ne_zero]

Result:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0

Proof state:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ↑(1 n) * Real.log ↑n = 0

Tactic:
rcases eq_or_ne n 1 with (hn | hn) <;> simp [hn]

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Tactic:
intro m mn hn

Result:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n

Proof state:
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False

Tactic:
exact hn (by simpa using mn)

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ d ∈ n.divisors, ↑(μ d) * log d = -Λ 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]

Result:
n : ℕ
⊢ ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * -Real.log ↑x.2

Proof state:
n : ℕ
⊢ ∀ x ∈ n.divisors, ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Tactic:
simp only [and_imp, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne, neg_inj, mem_divisors]

Result:
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Proof state:
n : ℕ
⊢ ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * -Real.log ↑x.2

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

Result:
n : ℕ
⊢ ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)

Proof state:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0

Tactic:
rintro rfl

Result:
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False

Proof state:
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0

Tactic:
simpa using mn

Result:
no goals

Proof state:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n

Tactic:
have : (m : ℝ) ≠ 0 := by
  rw [cast_ne_zero]
  rintro rfl
  exact hn (by simpa using mn)

Result:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n

Proof state:
n : ℕ
⊢ ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)

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, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne, neg_inj, 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]

Result:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)