awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (hypothesis)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ 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))
have hn₁ : 0 < n ∧ n ≤ N
Tactic: simp only [mem_Ioc] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : 0 < n ∧ n ≤ N
⊢ 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))
have 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))
Tactic: rw [divisorsAntidiagonal_eq_prod_filter_of_le hn.1.ne' hn.2]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ 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))
have 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)
Tactic: simp_rw [sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ 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)
have 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)
Tactic: rw [sum_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N : ℕ
⊢ 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))
have 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))
Tactic: rw [sum_Ioc_mul_eq_sum_prod_filter, sum_filter, sum_product]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
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))
have 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)
Tactic: refine sum_congr rfl fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N 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)
have 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))
Tactic: simp only [sum_ite, not_le, sum_const_zero, add_zero, mul_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 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))
have e_s : {x ∈ Ioc 0 N | n * x ≤ N} = Ioc 0 (N / n)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ {x ∈ Ioc 0 N | n * x ≤ N} = Ioc 0 (N / n)
have e_s : ∀ (a : ℕ), a ∈ {x ∈ Ioc 0 N | n * x ≤ N} ↔ a ∈ Ioc 0 (N / n)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
a : ℕ
⊢ a ∈ {x ∈ Ioc 0 N | n * x ≤ N} ↔ a ∈ Ioc 0 (N / n)
have e_s : ∀ (hn : 0 < n ∧ n ≤ N), 0 < a → (a ≤ N ∧ n * a ≤ N ↔ a ≤ N / n)
Tactic: simp only [mem_filter, mem_Ioc, and_assoc, and_congr_right_iff] at hn ⊢
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f g : ArithmeticFunction R
N n a : ℕ
hn : 0 < n ∧ n ≤ N
h : 0 < a
⊢ a ≤ N ∧ n * a ≤ N ↔ a ≤ N / n
have e_s : a ≤ N ∧ n * a ≤ N → a ≤ N / n
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
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
⊢ a ≤ N ∧ n * a ≤ N ↔ a ≤ N / n
have e_s₁ : a ≤ N / n → a ≤ N ∧ n * a ≤ N
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
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
⊢ a ≤ N / n
have e_s : a ≤ n * a / n
Tactic: grw [← h, Nat.mul_div_cancel_left _ (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
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
⊢ a ≤ N / n
have e_s₁ : a ≤ a
Tactic: grw [← h, Nat.mul_div_cancel_left _ (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
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
⊢ a ≤ N ∧ n * a ≤ N
have e_s : N / n ≤ N ∧ n * (N / n) ≤ N
Tactic: grw [hm]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ 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))
have 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))
Tactic: rw [sum_Ioc_mul_eq_sum_sum]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
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))
have 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)
Tactic: refine sum_congr rfl fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N 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)
have 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)
Tactic: simp_rw [natCoe_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
R : Type u_2
inst : Semiring R
f : ArithmeticFunction R
N n : ℕ
hn : n ∈ Ioc 0 N
⊢ 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)
have 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)
Tactic: rw_mod_cast [sum_Ioc_zeta]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
N : ℕ
⊢ Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (sigma 0 : (a : ℕ) → ℕ) n) (∑ n ∈ Ioc 0 N, N / n)
have rw : Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (zeta * zeta : (a : ℕ) → ℕ) n) (∑ n ∈ Ioc 0 N, N / n)
Tactic: rw [← zeta_mul_pow_eq_sigma, pow_zero_eq_zeta]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Misc (goal)
Goal:
N : ℕ
⊢ Eq (α := ℕ) (∑ n ∈ Ioc 0 N, (zeta * zeta : (a : ℕ) → ℕ) n) (∑ n ∈ Ioc 0 N, N / n)
have h : Eq (α := ℕ) (∑ n ∈ Ioc 0 N, N / n)
  (∑ n ∈ Ioc 0 N, HMul.hMul (α := ℕ) (β := ℕ) ((zeta : (a : ℕ) → ℕ) n : ℕ) ((↑(N / n) : ℕ) : ℕ))
Tactic: convert! sum_Ioc_mul_zeta_eq_sum zeta N using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ↔ Squarefree n
have mp : Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) → Squarefree n
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
mp : Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) → Squarefree n
⊢ Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ↔ Squarefree n
have mpr : Squarefree n → Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
h : Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
⊢ Squarefree n
have mp : ∀ (h : ¬Squarefree n), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ∨
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)
have 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
Tactic: simp only [moebius, coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ (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
have pos : Squarefree n →
  HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 0 ∨
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
      HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ (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
have neg : ¬Squarefree n → Eq (α := ℤ) 0 0 ∨ Eq (α := ℤ) 0 1 ∨ False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
h : Squarefree n
⊢ HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 0 ∨
    HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
      HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1
have pos : HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = 1 ∨
  HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) n : ℕ) = -1
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
h : ¬Squarefree n
⊢ Eq (α := ℤ) 0 0 ∨ Eq (α := ℤ) 0 1 ∨ False
have neg : Eq (α := ℤ) 0 0
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (hypothesis)
Goal:
n : ℕ
⊢ Ne (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ↔
    Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)
have this : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (0 : ℤ) ∨
  Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (1 : ℤ) ∨ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) n : ℤ) (-1 : ℤ)
Tactic: have := moebius_eq_or n
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
l : ℕ
hl : Squarefree l
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1
have rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) l : ℕ)) 2 = 1
Tactic: rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
l : ℕ
hl : Squarefree l
rw : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) l : ℕ)) 2 = 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1
have rw₁ : HPow.hPow (α := ℤ) (-1) (HMul.hMul (α := ℕ) (β := ℕ) ((cardFactors : (a : ℕ) → ℕ) l : ℕ) (2 : ℕ)) = 1
Tactic: rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1
have rw₂ : HPow.hPow (α := ℤ) (-1) (HMul.hMul (α := ℕ) (β := ℕ) (2 : ℕ) ((cardFactors : (a : ℕ) → ℕ) l : ℕ)) = 1
Tactic: rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1
have rw₃ : HPow.hPow (β := ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-1) 2) ((cardFactors : (a : ℕ) → ℕ) l : ℕ) = 1
Tactic: rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1
have rw₄ : HPow.hPow (α := ℤ) (β := ℕ) 1 ((cardFactors : (a : ℕ) → ℕ) l : ℕ) = 1
Tactic: rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
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
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) l : ℤ) 2 = 1
have rw₅ : Eq (α := ℤ) 1 1
Tactic: rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = if Squarefree n then 1 else 0
have pos : ∀ (h : Squarefree n), HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
pos : ∀ (h : Squarefree n), HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = if Squarefree n then 1 else 0
have neg : ∀ (h : ¬Squarefree n), HPow.hPow (α := ℤ) (β := ℕ) ((μ : (a : ℕ) → ℤ) n : ℤ) 2 = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (if Squarefree n then 1 else 0 : ℤ)
have pos : ∀ (h : Squarefree n), Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
pos : ∀ (h : Squarefree n), Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (if Squarefree n then 1 else 0 : ℤ)
have neg : ∀ (h : ¬Squarefree n), Eq (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (0 : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
n : ℕ
⊢ LE.le (α := ℤ) (|(μ : (a : ℕ) → ℤ) n| : ℤ) (1 : ℤ)
have rw : if Squarefree n then LE.le (α := ℤ) 1 1 else LE.le (α := ℤ) 0 1
Tactic: rw [abs_moebius, apply_ite (· ≤ 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p : ℕ
hp : Nat.Prime p
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)
have rw : HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) p : ℕ) = -1
Tactic: rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p : ℕ
hp : Nat.Prime p
rw : HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) p : ℕ) = -1
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)
have rw₁ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 = -1
Tactic: rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p : ℕ
hp : Nat.Prime p
rw : HPow.hPow (α := ℤ) (β := ℕ) (-1) ((cardFactors : (a : ℕ) → ℕ) p : ℕ) = -1
rw₁ : HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 = -1
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)
have rw₂ : Eq (α := ℤ) (-1) (-1)
Tactic: rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (if k = 1 then -1 else 0 : ℤ)
have pos : ∀ (h : k = 1), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
pos : ∀ (h : k = 1), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (if k = 1 then -1 else 0 : ℤ)
have neg : ∀ (h : ¬k = 1), Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)
have pos : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 1) : ℤ) (-1 : ℤ)
Tactic: rw [h, pow_one, moebius_apply_prime hp]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
pos : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 1) : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)
have pos₁ : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)
Tactic: rw [h, pow_one, moebius_apply_prime hp]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
pos : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (HPow.hPow (β := ℕ) p 1) : ℤ) (-1 : ℤ)
pos₁ : Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) p : ℤ) (-1 : ℤ)
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (-1 : ℤ)
have pos₂ : Eq (α := ℤ) (-1) (-1)
Tactic: rw [h, pow_one, moebius_apply_prime hp]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ Eq (α := ℤ) ((μ : (a : ℕ) → ℤ) (p ^ k) : ℤ) (0 : ℤ)
have neg : ¬Squarefree (p ^ k)
Tactic: rw [moebius_eq_zero_of_not_squarefree]
-- Lean 4 proof step from Mathlib.NumberTheory.ArithmeticFunction.Moebius (goal)
Goal:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)
have neg : ¬Squarefree p ∨ ¬k = 1
Tactic: rw [squarefree_pow_iff hp.ne_one hk, not_and_or]