awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
⊢ (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (↑(n / m) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
have rw₁ : (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -(Real.log (↑n : ℝ) - Real.log (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
rw₁ :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -(Real.log (↑n : ℝ) - Real.log (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
⊢ (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (↑(n / m) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
have rw₂ : (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * (Real.log (↑m : ℝ) - Real.log (↑n : ℝ)) =
  (↑((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
this : Ne (α := ℝ) (↑m : ℝ) 0
rw :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
rw₁ :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -(Real.log (↑n : ℝ) - Real.log (↑m : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
rw₂ :
  (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * (Real.log (↑m : ℝ) - Real.log (↑n : ℝ)) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
⊢ (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * -Real.log (↑(n / m) : ℝ) =
    (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ)
have rw₃ : (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑m : ℝ) - (↑((μ : (a : ℕ) → ℤ) m) : ℝ) * Real.log (↑n : ℝ) =
  (↑((μ : (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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (hypothesis)
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
have this : Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
  (∑ i ∈ n.divisors,
    ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
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, Ne, 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
⊢ Eq (α := ℝ) (∑ x ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) x) : ℝ) * Real.log (↑x : ℝ))
    (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
have rw : (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
Tactic: rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self,
    moebius_mul_coe_zeta]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
⊢ (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
have inl : ∀ (hn : n = 1), (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
Tactic: rcases eq_or_ne n 1 with (hn | hn)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
this :
  Eq (α := ℝ) (∑ i ∈ n.divisors, (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * -Real.log (↑(n / i) : ℝ))
    (∑ i ∈ n.divisors,
      ((↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑i : ℝ) - (↑((μ : (a : ℕ) → ℤ) i) : ℝ) * Real.log (↑n : ℝ)))
inl : ∀ (hn : n = 1), (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
⊢ (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
have inr : ∀ (hn : n ≠ 1), (↑((1 : (a : ℕ) → ℤ) n) : ℝ) * Real.log (↑n : ℝ) = 0
Tactic: rcases eq_or_ne n 1 with (hn | hn)
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt (goal)
Goal:
n : ℕ
⊢ (Λ : (a : ℕ) → ℝ) (n + 1) ≤ Real.log (↑(n + 1) : ℝ)
have rw : LE.le (α := ℝ) ((Λ : (a : ℕ) → ℝ) (n + 1) : ℝ) (∑ i ∈ (n + 1).divisors, (Λ : (a : ℕ) → ℝ) i : ℝ)
Tactic: rw [← vonMangoldt_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ Eq (α := M)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → M) x : M)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i : M)
have rw : Eq.{u_2 + 1} (α := M)
  (∑ x ∈ x.divisorsAntidiagonal,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
      ((f : (a : ℕ) → M) x.2 : M))
  (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
Tactic: rw [smul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
have trans : Eq.{u_2 + 1} (α := M)
  (∑ x ∈ x.divisorsAntidiagonal,
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
      ((f : (a : ℕ) → M) x.2 : M))
  (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2)
Tactic: trans ∑ i ∈ divisorsAntidiagonal x, f i.snd
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
trans :
  Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2)
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
have trans₁ : Eq.{u_2 + 1} (α := M) (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
Tactic: trans ∑ i ∈ divisorsAntidiagonal x, f i.snd
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ Eq.{u_2 + 1} (α := M)
    (∑ x ∈ x.divisorsAntidiagonal,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x.1 : R)
        ((f : (a : ℕ) → M) x.2 : M))
    (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2)
have refine : ∀ (i : ℕ × ℕ) (hi : i ∈ x.divisorsAntidiagonal),
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
Tactic: refine sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
have hi₁ : i ∈ (i.1 * i.2).divisorsAntidiagonal
Tactic: rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
Cleared hypotheses: x, hi
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ x.divisorsAntidiagonal
hi₁ : i ∈ (i.1 * i.2).divisorsAntidiagonal
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
have h : i.1 * i.2 ≠ 0
Tactic: rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
Cleared hypotheses: x, hi
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑((ζ : (a : ℕ) → ℕ) i.1) : R) ((f : (a : ℕ) → M) i.2 : M) =
  (f : (a : ℕ) → M) i.2
Tactic: rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑((ζ : (a : ℕ) → ℕ) i.1) : R) ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑1 : R) ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
Tactic: rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑((ζ : (a : ℕ) → ℕ) i.1) : R) ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑1 : R) ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 1 ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
Tactic: rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑((ζ : (a : ℕ) → ℕ) i.1) : R) ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (↑1 : R) ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 1 ((f : (a : ℕ) → M) i.2 : M) = (f : (a : ℕ) → M) i.2
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) (((↑ζ : ArithmeticFunction R) : (a : ℕ) → R) i.1 : R)
      ((f : (a : ℕ) → M) i.2 : M) =
    (f : (a : ℕ) → M) i.2
have rw₃ : Eq (α := M) ((f : (a : ℕ) → M) i.2 : M) ((f : (a : ℕ) → M) i.2 : M)
Tactic: rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
have rw : Eq.{u_2 + 1} (α := M) (∑ i ∈ map { toFun := fun (d : ℕ) ↦ (x / d, d), inj' := sorry } x.divisors, (f : (a : ℕ) → M) i.2)
  (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
Tactic: rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
rw :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ map { toFun := fun (d : ℕ) ↦ (x / d, d), inj' := ⋯ } x.divisors, (f : (a : ℕ) → M) i.2)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
have rw₁ : Eq.{u_2 + 1} (α := M)
  (∑ x_1 ∈ x.divisors, (f : (a : ℕ) → M) (({ toFun := fun (d : ℕ) ↦ (x / d, d), inj' := sorry } : (a : ℕ) → ℕ × ℕ) x_1).2)
  (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
Tactic: rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : MulAction R M
f : ArithmeticFunction M
x : ℕ
rw :
  Eq.{u_2 + 1} (α := M) (∑ i ∈ map { toFun := fun (d : ℕ) ↦ (x / d, d), inj' := ⋯ } x.divisors, (f : (a : ℕ) → M) i.2)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
rw₁ :
  Eq.{u_2 + 1} (α := M)
    (∑ x_1 ∈ x.divisors, (f : (a : ℕ) → M) (({ toFun := fun (d : ℕ) ↦ (x / d, d), inj' := ⋯ } : (a : ℕ) → ℕ × ℕ) x_1).2)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
⊢ Eq.{u_2 + 1} (α := M) (∑ i ∈ x.divisorsAntidiagonal, (f : (a : ℕ) → M) i.2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
have rw₂ : Eq.{u_2 + 1} (α := M) (∑ x_1 ∈ x.divisors, (f : (a : ℕ) → M) (x / x_1, x_1).2) (∑ i ∈ x.divisors, (f : (a : ℕ) → M) i)
Tactic: rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
⊢ HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f =
    HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R)
have h : ∀ (n : ℕ),
  Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) n : R)
    ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) n : R)
    ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) n : R)
have h : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ n.divisorsAntidiagonal,
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2 : R) ((↑((ζ : (a : ℕ) → ℕ) x.1) : R) : R))
  (∑ x ∈ n.divisorsAntidiagonal,
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
Tactic: simp_rw [mul_apply, natCoe_apply, (cast_commute ..).eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2 : R) ((↑((ζ : (a : ℕ) → ℕ) x.1) : R) : R))
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
have h : Eq.{u_1 + 1} (α := R)
  (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
  (∑ x ∈ n.divisorsAntidiagonal,
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
Tactic: rw [sum_divisorsAntidiagonal fun x y ↦ f y * ζ x, sum_divisorsAntidiagonal' fun x y ↦ f x * ζ y]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
n : ℕ
h :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.2 : R) ((↑((ζ : (a : ℕ) → ℕ) x.1) : R) : R))
    (∑ x ∈ n.divisorsAntidiagonal,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((↑((ζ : (a : ℕ) → ℕ) x.2) : R) : R))
have h₁ : Eq.{u_1 + 1} (α := R)
  (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
  (∑ i ∈ n.divisors, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n / i) : R) ((↑((ζ : (a : ℕ) → ℕ) i) : R) : R))
Tactic: rw [sum_divisorsAntidiagonal fun x y ↦ f y * ζ x, sum_divisorsAntidiagonal' fun x y ↦ f x * ζ y]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)
have rw : Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R)
  (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)
Tactic: rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
rw :
  Eq (α := R) ((HMul.hMul (α := ArithmeticFunction R) (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)
⊢ Eq (α := R) ((HMul.hMul (β := ArithmeticFunction R) f (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R)
    (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i) (∑ i ∈ x.divisors, (f : (a : ℕ) → R) i)
Tactic: rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
f : ArithmeticFunction ℕ
x : ℕ
⊢ Eq (α := ℕ) ((ζ * f : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
have rw : Eq (α := ℕ) (((↑ζ : ArithmeticFunction ℕ) * f : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
Tactic: rw [← natCoe_nat ζ, coe_zeta_mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
f : ArithmeticFunction ℕ
x : ℕ
rw : Eq (α := ℕ) (((↑ζ : ArithmeticFunction ℕ) * f : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) ((ζ * f : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
have rw₁ : Eq (α := ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i)
Tactic: rw [← natCoe_nat ζ, coe_zeta_mul_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
f : ArithmeticFunction ℕ
x : ℕ
⊢ Eq (α := ℕ) ((f * ζ : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
have rw : Eq (α := ℕ) ((f * (↑ζ : ArithmeticFunction ℕ) : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
Tactic: rw [← natCoe_nat ζ, coe_mul_zeta_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
f : ArithmeticFunction ℕ
x : ℕ
rw : Eq (α := ℕ) ((f * (↑ζ : ArithmeticFunction ℕ) : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
⊢ Eq (α := ℕ) ((f * ζ : (a : ℕ) → ℕ) x : ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i : ℕ)
have rw₁ : Eq (α := ℕ) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i) (∑ i ∈ x.divisors, (f : (a : ℕ) → ℕ) i)
Tactic: rw [← natCoe_nat ζ, coe_mul_zeta_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
f : ArithmeticFunction ℕ
⊢ ζ * f = f * ζ
have rw : (↑ζ : ArithmeticFunction ℕ) * f = f * (↑ζ : ArithmeticFunction ℕ)
Tactic: rw [← natCoe_nat ζ, coe_zeta_mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
f : ArithmeticFunction ℕ
rw : (↑ζ : ArithmeticFunction ℕ) * f = f * (↑ζ : ArithmeticFunction ℕ)
⊢ ζ * f = f * ζ
have rw₁ : f * (↑ζ : ArithmeticFunction ℕ) = f * (↑ζ : ArithmeticFunction ℕ)
Tactic: rw [← natCoe_nat ζ, coe_zeta_mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ f.pmul g = g.pmul f
have h : ∀ (x : ℕ), Eq (α := R) ((f.pmul g : (a : ℕ) → R) x : R) ((g.pmul f : (a : ℕ) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
⊢ (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)
have h : ∀ (x : ℕ), Eq (α := R) (((f₁.pmul f₂).pmul f₃ : (a : ℕ) → R) x : R) ((f₁.pmul (f₂.pmul f₃) : (a : ℕ) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
⊢ f.pmul (↑ζ : ArithmeticFunction R) = f
have h : ∀ (x : ℕ), Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
have h : Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
h : Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) 0 : R) ((f : (a : ℕ) → R) 0 : R)
⊢ Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
have h₁ : ∀ (n : ℕ), Eq (α := R) ((f.pmul (↑ζ : ArithmeticFunction R) : (a : ℕ) → R) (n + 1) : R) ((f : (a : ℕ) → R) (n + 1) : R)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Zeta (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
f : ArithmeticFunction R
⊢ pmul (↑ζ : ArithmeticFunction R) f = f
have h : ∀ (x : ℕ), Eq (α := R) ((pmul (↑ζ : ArithmeticFunction R) f : (a : ℕ) → R) x : R) ((f : (a : ℕ) → R) x : R)
Tactic: ext x