awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : 0 < n ∧ n ≤ N
rw rw₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ n.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))

Tactic:
rw [divisorsAntidiagonal_eq_prod_filter_of_le hn.1.ne' hn.2]

Premises used: LT.lt.ne', And.right, And.left, Nat.divisorsAntidiagonal_eq_prod_filter_of_le
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
simp_rw :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N,
        if a.1 * a.2 = x then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1 : R) ((g : (a : ℕ) → R) a.2 : R)
        else 0)
    (∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N,
      if a.1 * a.2 ≤ N then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1 : R) ((g : (a : ℕ) → R) a.2 : R) else 0)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ n ∈ Ioc 0 N,
      ∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 = n,
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))
    (∑ x ∈ Ioc 0 N ×ˢ Ioc 0 N with x.1 * x.2 ≤ N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R))

Tactic:
simp_rw [sum_filter]

Premises used: Finset.sum_filter
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ y ∈ Ioc 0 N ×ˢ Ioc 0 N,
      ∑ x ∈ Ioc 0 N,
        if y.1 * y.2 = x then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) y.1 : R) ((g : (a : ℕ) → R) y.2 : R)
        else 0)
    (∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N,
      if a.1 * a.2 ≤ N then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1 : R) ((g : (a : ℕ) → R) a.2 : R) else 0)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N,
        if a.1 * a.2 = x then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1 : R) ((g : (a : ℕ) → R) a.2 : R)
        else 0)
    (∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N,
      if a.1 * a.2 ≤ N then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1 : R) ((g : (a : ℕ) → R) a.2 : R) else 0)

Tactic:
rw [sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
x : ℕ × ℕ
h : x ∈ Ioc 0 N ×ˢ Ioc 0 N
⊢ (∑ x_1 ∈ Ioc 0 N,
      if x.1 * x.2 = x_1 then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R)
      else 0) =
    if x.1 * x.2 ≤ N then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((g : (a : ℕ) → R) x.2 : R) else 0

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (∑ y ∈ Ioc 0 N ×ˢ Ioc 0 N,
      ∑ x ∈ Ioc 0 N,
        if y.1 * y.2 = x then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) y.1 : R) ((g : (a : ℕ) → R) y.2 : R)
        else 0)
    (∑ a ∈ Ioc 0 N ×ˢ Ioc 0 N,
      if a.1 * a.2 ≤ N then HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) a.1 : R) ((g : (a : ℕ) → R) a.2 : R) else 0)

Tactic:
exact sum_congr rfl fun _ _ ↦ (by simp_all)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ y ∈ Ioc 0 N,
        if (x, y).1 * (x, y).2 ≤ N then
          HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x, y).1 : R) ((g : (a : ℕ) → R) (x, y).2 : R)
        else 0)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ m ∈ Ioc 0 (N / n), (g : (a : ℕ) → R) m : R))
⊢ Eq.{u_2 + 1} (α := R) (∑ n ∈ Ioc 0 N, (f * g : (a : ℕ) → R) n)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ m ∈ Ioc 0 (N / n), (g : (a : ℕ) → R) m : R))

Tactic:
rw [sum_Ioc_mul_eq_sum_prod_filter, sum_filter, sum_product]

Premises used: ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter, Finset.sum_filter, Finset.sum_product
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ y ∈ Ioc 0 N,
        if (x, y).1 * (x, y).2 ≤ N then
          HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x, y).1 : R) ((g : (a : ℕ) → R) (x, y).2 : R)
        else 0)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ m ∈ Ioc 0 (N / n), (g : (a : ℕ) → R) m : R))

Tactic:
sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
refine :
  ∀ (n : ℕ) (hn : n ∈ Ioc 0 N),
    (∑ y ∈ Ioc 0 N,
        if (n, y).1 * (n, y).2 ≤ N then
          HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n, y).1 : R) ((g : (a : ℕ) → R) (n, y).2 : R)
        else 0) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ m ∈ Ioc 0 (N / n), (g : (a : ℕ) → R) m : R)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N,
      ∑ y ∈ Ioc 0 N,
        if (x, y).1 * (x, y).2 ≤ N then
          HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (x, y).1 : R) ((g : (a : ℕ) → R) (x, y).2 : R)
        else 0)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ m ∈ Ioc 0 (N / n), (g : (a : ℕ) → R) m : R))

Tactic:
refine sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
simp :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N with n * x ≤ N, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) x : R))
    (∑ i ∈ Ioc 0 (N / n), HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) i : R))
⊢ (∑ y ∈ Ioc 0 N,
      if (n, y).1 * (n, y).2 ≤ N then
        HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (n, y).1 : R) ((g : (a : ℕ) → R) (n, y).2 : R)
      else 0) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ m ∈ Ioc 0 (N / n), (g : (a : ℕ) → R) m : R)

Tactic:
simp only [sum_ite, not_le, sum_const_zero, add_zero, mul_sum]

Premises used: not_le, Finset.mul_sum, Finset.sum_const_zero, add_zero, Finset.sum_ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
e_s : {x ∈ Ioc 0 N | n * x ≤ N} = Ioc 0 (N / n)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ Ioc 0 N with n * x ≤ N, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) x : R))
    (∑ i ∈ Ioc 0 (N / n), HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) i : R))

Tactic:
congr
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
e_s : ∀ (a : ℕ), a ∈ {x ∈ Ioc 0 N | n * x ≤ N} ↔ a ∈ Ioc 0 (N / n)
⊢ {x ∈ Ioc 0 N | n * x ≤ N} = Ioc 0 (N / n)

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
a : ℕ
e_s : ∀ (hn : 0 < n ∧ n ≤ N), 0 < a → (a ≤ N ∧ n * a ≤ N ↔ a ≤ N / n)
⊢ a ∈ {x ∈ Ioc 0 N | n * x ≤ N} ↔ a ∈ Ioc 0 (N / n)

Tactic:
simp only [mem_filter, mem_Ioc, and_assoc, and_congr_right_iff] at hn ⊢

Premises used: and_congr_right_iff, and_assoc, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n a : ℕ
hn : 0 < n ∧ n ≤ N
h : 0 < a
e_s : a ≤ N ∧ n * a ≤ N → a ≤ N / n
e_s₁ : a ≤ N / n → a ≤ N ∧ n * a ≤ N
⊢ a ≤ N ∧ n * a ≤ N ↔ a ≤ N / n

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n a : ℕ
hn : 0 < n ∧ n ≤ N
h_1 : 0 < a
left : a ≤ N
h : n * a ≤ N
⊢ 0 < n

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n a : ℕ
hn : 0 < n ∧ n ≤ N
h_1 : 0 < a
left : a ≤ N
h : n * a ≤ N
e_s : a ≤ n * a / n
e_s₁ e_s₂ : a ≤ a
⊢ a ≤ N / n

Tactic:
grw [← h, Nat.mul_div_cancel_left _ (by lia)]

Premises used: Nat.mul_div_cancel_left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n a : ℕ
hn : 0 < n ∧ n ≤ N
h : 0 < a
hm : a ≤ N / n
e_s : N / n ≤ N ∧ n * (N / n) ≤ N
⊢ a ≤ N ∧ n * a ≤ N

Tactic:
grw [hm]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n a : ℕ
hn : 0 < n ∧ n ≤ N
h : 0 < a
hm : a ≤ N / n
⊢ N / n ≤ N ∧ n * (N / n) ≤ N

Tactic:
simp [mul_div_le, div_le_self]

Premises used: Nat.div_le_self, Nat.mul_div_le
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N : ℕ
rw :
  Eq.{u_2 + 1} (α := R)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R)
        (∑ m ∈ Ioc 0 (N / n), (((↑zeta : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R))
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R))
⊢ Eq.{u_2 + 1} (α := R)
    (∑ n ∈ Ioc 0 N, (HMul.hMul (β := ArithmeticFunction R) f (↑zeta : ArithmeticFunction R) : (a : ℕ) → R) n)
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R))

Tactic:
rw [sum_Ioc_mul_eq_sum_sum]

Premises used: ArithmeticFunction.sum_Ioc_mul_eq_sum_sum
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R)
        (∑ m ∈ Ioc 0 (N / n), (((↑zeta : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R))
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R))

Tactic:
sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N : ℕ
refine :
  ∀ (n : ℕ) (hn : n ∈ Ioc 0 N),
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R)
        (∑ m ∈ Ioc 0 (N / n), (((↑zeta : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R) =
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ n ∈ Ioc 0 N,
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R)
        (∑ m ∈ Ioc 0 (N / n), (((↑zeta : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R))
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R))

Tactic:
refine sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
simp_rw :
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ x ∈ Ioc 0 (N / n), (↑((zeta : (a : ℕ) → ℕ) x) : R) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R)
      (∑ m ∈ Ioc 0 (N / n), (((↑zeta : ArithmeticFunction R) : ArithmeticFunction R) : (a : ℕ) → R) m : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R)

Tactic:
simp_rw [natCoe_apply]

Premises used: ArithmeticFunction.natCoe_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(∑ x ∈ Ioc 0 (N / n), (zeta : (a : ℕ) → ℕ) x) : R) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (∑ x ∈ Ioc 0 (N / n), (↑((zeta : (a : ℕ) → ℕ) x) : R) : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((↑(N / n) : R) : R)

Tactic:
rw_mod_cast [sum_Ioc_zeta]

Premises used: ArithmeticFunction.sum_Ioc_zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
rw : Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (zeta * zeta : (a : ℕ) → ℕ) n) (∑ n ∈ Ioc 0 N, N / n)
⊢ Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (sigma 0 : (a : ℕ) → ℕ) n) (∑ n ∈ Ioc 0 N, N / n)

Tactic:
rw [← zeta_mul_pow_eq_sigma, pow_zero_eq_zeta]

Premises used: ArithmeticFunction.zeta_mul_pow_eq_sigma, ArithmeticFunction.pow_zero_eq_zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
⊢ Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (zeta * (↑zeta : ArithmeticFunction ℕ) : (a : ℕ) → ℕ) n)
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := ℕ) (β := ℕ) ((zeta : (a : ℕ) → ℕ) n : ℕ) ((↑(N / n) : ℕ) : ℕ))

Tactic:
sum_Ioc_mul_zeta_eq_sum zeta N

Premises used: ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum, ArithmeticFunction.zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
h :
  Eq (α := ℕ) (∑ n ∈ Ioc 0 N, N / n)
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := ℕ) (β := ℕ) ((zeta : (a : ℕ) → ℕ) n : ℕ) ((↑(N / n) : ℕ) : ℕ))
⊢ Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (zeta * zeta : (a : ℕ) → ℕ) n) (∑ n ∈ Ioc 0 N, N / n)

Tactic:
convert! sum_Ioc_mul_zeta_eq_sum zeta N using 1

Premises used: ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum, ArithmeticFunction.zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
⊢ ∀ x ∈ Ioc 0 N, N / x = if x = 0 then 0 else N / x

Tactic:
grind
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
N : ℕ
⊢ Eq (α := ℕ) (∑ n ∈ Ioc 0 N, N / n)
    (∑ n ∈ Ioc 0 N, HMul.hMul (α := ℕ) (β := ℕ) ((zeta : (a : ℕ) → ℕ) n : ℕ) ((↑(N / n) : ℕ) : ℕ))

Tactic:
simpa using sum_congr rfl (by grind)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ #(m * n).divisors = #m.divisors * #n.divisors

Tactic:
simp only [← sigma_zero_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

Premises used: ArithmeticFunction.sigma_zero_apply, ArithmeticFunction.isMultiplicative_sigma, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Misc
Goal:
m n : ℕ
hmn : m.Coprime n
⊢ ∑ d ∈ (m * n).divisors, d = HMul.hMul (α := ℕ) (∑ d ∈ m.divisors, d) (∑ d ∈ n.divisors, d)

Tactic:
simp only [← sigma_one_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

Premises used: ArithmeticFunction.sigma_one_apply, ArithmeticFunction.isMultiplicative_sigma, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
⊢ Eq (α := ℤ)
    ((fun (n : ℕ) ↦ if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) 0)
    0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ (μ : (a : ℕ) → ℤ) n = HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ)

Tactic:
if_pos h

Premises used: if_pos, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)

Tactic:
if_neg h

Premises used: if_neg, ite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
mp : Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) → Squarefree n
mpr : Squarefree n → Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
⊢ Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ↔ Squarefree n

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
mp : ∀ (h : ¬Squarefree n), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
⊢ Squarefree n

Tactic:
contrapose h
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
simp :
  (if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) = 0 ∨
    (if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) = 1 ∨
      (if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) = -1
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)

Tactic:
simp only [moebius, coe_mk]

Premises used: ArithmeticFunction.coe_mk, ArithmeticFunction.moebius
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
pos :
  Squarefree n →
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 0 ∨
      HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
        HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1
neg : ¬Squarefree n → Eq (α := ℤ) 0 0 ∨ Eq (α := ℤ) 0 1 ∨ False
⊢ (if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) = 0 ∨
    (if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) = 1 ∨
      (if Squarefree n then HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) else 0) = -1

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
pos :
  HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1
⊢ HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 0 ∨
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
      HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1

Tactic:
right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1

Tactic:
neg_one_pow_eq_or ..

Premises used: neg_one_pow_eq_or
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1

Tactic:
exact neg_one_pow_eq_or ..

Premises used: neg_one_pow_eq_or
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
neg : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) 0 0 ∨ Eq (α := ℤ) 0 1 ∨ False

Tactic:
left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
⊢ Eq (α := ℤ) 0 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)

Tactic:
have := moebius_eq_or n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
this :
  Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)
⊢ Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ↔
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)

Tactic:
lia
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
l : ℕ
hl : Squarefree l
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) l : ℕ)) 2 = 1
rw₁ : HPow.hPow (α := ℤ) (-1) (HMul.hMul (α := ℕ) (β := ℕ) ((cardFactors : (a : ℕ) → ℕ) l : ℕ) (2 : ℕ)) = 1
rw₂ : HPow.hPow (α := ℤ) (-1) (HMul.hMul (α := ℕ) (β := ℕ) (2 : ℕ) ((cardFactors : (a : ℕ) → ℕ) l : ℕ)) = 1
rw₃ : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 2) ((cardFactors : (a : ℕ) → ℕ) l : ℕ) = 1
rw₄ : HPow.hPow (α := ℤ) (β := ℕ) 1 ((cardFactors : (a : ℕ) → ℕ) l : ℕ) = 1
rw₅ rw₆ : Eq (α := ℤ) 1 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1

Tactic:
rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]

Premises used: one_pow, neg_one_sq, ArithmeticFunction.moebius_apply_of_squarefree, pow_mul, mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
l : ℕ
hl : Squarefree l
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) l| : ℤ) (1 : ℤ)

Tactic:
simp only [moebius_apply_of_squarefree hl, abs_pow, abs_neg, abs_one, one_pow]

Premises used: one_pow, abs_neg, ArithmeticFunction.moebius_apply_of_squarefree, abs_one, abs_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
pos : ∀ (h : Squarefree n), HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 1
neg : ∀ (h : ¬Squarefree n), HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 0
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = if Squarefree n then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 1

Tactic:
moebius_sq_eq_one_of_squarefree h

Premises used: ArithmeticFunction.moebius_sq_eq_one_of_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 1

Tactic:
exact moebius_sq_eq_one_of_squarefree h

Premises used: ArithmeticFunction.moebius_sq_eq_one_of_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 0

Tactic:
simp only [moebius_eq_zero_of_not_squarefree h, zero_pow (show 2 ≠ 0 by simp)]

Premises used: ArithmeticFunction.moebius_eq_zero_of_not_squarefree, zero_pow
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
pos : ∀ (h : Squarefree n), Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)
neg : ∀ (h : ¬Squarefree n), Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (if Squarefree n then 1 else 0 : ℤ)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)

Tactic:
abs_moebius_eq_one_of_squarefree h

Premises used: ArithmeticFunction.abs_moebius_eq_one_of_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : Squarefree n
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)

Tactic:
exact abs_moebius_eq_one_of_squarefree h

Premises used: ArithmeticFunction.abs_moebius_eq_one_of_squarefree
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
h : ¬Squarefree n
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (0 : ℤ)

Tactic:
simp only [moebius_eq_zero_of_not_squarefree h, abs_zero]

Premises used: ArithmeticFunction.moebius_eq_zero_of_not_squarefree, abs_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
rw : if Squarefree n then LE.le (α := ℤ) 1 1 else LE.le (α := ℤ) 0 1
⊢ LE.le (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)

Tactic:
rw [abs_moebius, apply_ite (· ≤ 1)]

Premises used: apply_ite, LE.le, OfNat.ofNat, ArithmeticFunction.abs_moebius
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
n : ℕ
⊢ if Squarefree n then LE.le (α := ℤ) 1 1 else LE.le (α := ℤ) 0 1

Tactic:
simp