n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * -Real.log ↑x.snd
n : ℕ
⊢ ∑ d in divisors n, ↑(↑μ d) * ↑log d = -↑Λ n
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]
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * -Real.log ↑x.snd
rw [sum_divisorsAntidiagonal fun i j => (μ i : ℝ) * -Real.log j]
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
n : ℕ
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
have : (∑ i : ℕ in n.divisors, (μ i : ℝ) * -Real.log (n / i : ℕ)) =
    ∑ i : ℕ in 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.def, 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]
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ↑(↑1 n) * Real.log ↑n = 0
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ∑ x in divisors n, ↑(↑μ x) * Real.log ↑x = ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i)
rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self,
  moebius_mul_coe_zeta]
no goals
n : ℕ
this :
  ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
⊢ ↑(↑1 n) * Real.log ↑n = 0
rcases eq_or_ne n 1 with (hn | hn) <;> simp [hn]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors n → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
n : ℕ
⊢ ∑ i in divisors n, ↑(↑μ i) * -Real.log ↑(n / i) = ∑ i in divisors n, (↑(↑μ i) * Real.log ↑i - ↑(↑μ i) * Real.log ↑n)
apply sum_congr rfl
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
n : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors n → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
simp only [and_imp, Int.cast_eq_zero, mul_eq_mul_left_iff, Ne.def, neg_inj, mem_divisors]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(↑μ x) * -Real.log ↑(n / x) = ↑(↑μ x) * Real.log ↑x - ↑(↑μ x) * Real.log ↑n
intro m mn hn
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
have : (m : ℝ) ≠ 0 := by
  rw [cast_ne_zero]
  rintro rfl
  exact hn (by simpa using mn)
no goals
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : ↑m ≠ 0
⊢ ↑(↑μ m) * -Real.log ↑(n / m) = ↑(↑μ m) * Real.log ↑m - ↑(↑μ m) * Real.log ↑n
rw [Nat.cast_div mn this, Real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub]
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ ↑m ≠ 0
rw [cast_ne_zero]
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0
rintro rfl
no goals
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ False
exact hn (by simpa using mn)
no goals
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0
simpa using mn