awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h :
  ∀ (a : ℕ),
    a > 0 → ∑ i ∈ a.divisors, f i = g a ↔
      Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) a : R)
        ((g' : (a : ℕ) → R) a : R)
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ (x : ℕ),
      Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) x : R)
        ((g' : (a : ℕ) → R) x : R)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ GT.gt (α := ℕ) 0 0 → ∑ i ∈ divisors 0, f i = g 0 ↔
    Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) 0 : R)
      ((g' : (a : ℕ) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
h :
  n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔
    Eq (α := R) (∑ i ∈ (n + 1).divisors, (f' : (a : ℕ) → R) i : R) ((g' : (a : ℕ) → R) (n + 1) : R)
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔
    Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) (n + 1) : R)
      ((g' : (a : ℕ) → R) (n + 1) : R)

Tactic:
rw [coe_zeta_smul_apply]

Premises used: ArithmeticFunction.coe_zeta_smul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
h : ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (∑ x ∈ (n + 1).divisors, if x = 0 then 0 else f x) = g (n + 1)
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔
    Eq (α := R) (∑ i ∈ (n + 1).divisors, (f' : (a : ℕ) → R) i : R) ((g' : (a : ℕ) → R) (n + 1) : R)

Tactic:
simp only [forall_prop_of_true, succ_pos', f', g', coe_mk, succ_ne_zero, ite_false]

Premises used: Nat.succ_pos', ite_false, ArithmeticFunction.coe_mk, Nat.succ_ne_zero, forall_prop_of_true
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
h h₁ : ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (n + 1).divisors.sum f = g (n + 1)
⊢ ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (∑ x ∈ (n + 1).divisors, if x = 0 then 0 else f x) = g (n + 1)

Tactic:
rw [sum_congr rfl fun x hx => if_neg (pos_of_mem_divisors hx).ne']

Premises used: LT.lt.ne', if_neg, Finset.sum_congr, Nat.pos_of_mem_divisors, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
h :
  GT.gt (α := ℕ) 0 0 → ∑ i ∈ divisors 0, f i = g 0 ↔
    Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) 0 : R)
      ((g' : (a : ℕ) → R) 0 : R)
h₁ :
  ∀ (n : ℕ),
    n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔
      Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) (n + 1) : R)
        ((g' : (a : ℕ) → R) (n + 1) : R)
⊢ n > 0 → ∑ i ∈ n.divisors, f i = g n ↔
    Eq (α := R) ((HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' : (a : ℕ) → R) n : R)
      ((g' : (a : ℕ) → R) n : R)

Tactic:
cases n with
    | zero => simp
    | succ n =>
      rw [coe_zeta_smul_apply]
      simp only [forall_prop_of_true, succ_pos', f', g', coe_mk, succ_ne_zero, ite_false]
      rw [sum_congr rfl fun x hx => if_neg (pos_of_mem_divisors hx).ne']

Premises used: Nat.succ_pos', ArithmeticFunction.zero, ite_false, ArithmeticFunction.coe_mk, LT.lt.ne', Nat.succ_ne_zero, ArithmeticFunction.coe_zeta_smul_apply, forall_prop_of_true, Nat.succ, if_neg, Finset.sum_congr, Nat.pos_of_mem_divisors, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
trans : HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g' ↔ μ • g' = f'
trans₁ :
  μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
⊢ HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g' ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
trans μ • g' = f'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
mp : HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g' → μ • g' = f'
mpr : μ • g' = f' → HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g'
⊢ HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g' ↔ μ • g' = f'

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g'
⊢ μ • g' = f'

Tactic:
simp only [← h, ← mul_smul, moebius_mul_coe_zeta, coe_zeta_mul_moebius, one_smul]

Premises used: ArithmeticFunction.moebius_mul_coe_zeta, one_smul, ArithmeticFunction.coe_zeta_mul_moebius, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : μ • g' = f'
⊢ HSMul.hSMul (α := ArithmeticFunction ℤ) (↑ζ : ArithmeticFunction ℤ) f' = g'

Tactic:
simp only [← h, ← mul_smul, moebius_mul_coe_zeta, coe_zeta_mul_moebius, one_smul]

Premises used: ArithmeticFunction.moebius_mul_coe_zeta, one_smul, ArithmeticFunction.coe_zeta_mul_moebius, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
rw :
  (∀ (x : ℕ), Eq (α := R) ((μ • g' : (a : ℕ) → R) x : R) ((f' : (a : ℕ) → R) x : R)) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n
⊢ μ • g' = f' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
rw [ArithmeticFunction.ext_iff]

Premises used: ArithmeticFunction.ext_iff
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h :
  ∀ (a : ℕ),
    Eq (α := R) ((μ • g' : (a : ℕ) → R) a : R) ((f' : (a : ℕ) → R) a : R) ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a
⊢ (∀ (x : ℕ), Eq (α := R) ((μ • g' : (a : ℕ) → R) x : R) ((f' : (a : ℕ) → R) x : R)) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ Eq (α := R) ((μ • g' : (a : ℕ) → R) 0 : R) ((f' : (a : ℕ) → R) 0 : R) ↔
    GT.gt (α := ℕ) 0 0 → ∑ x ∈ divisorsAntidiagonal 0, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
h :
  ∑ x ∈ (n + 1).divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (if x.2 = 0 then 0 else g x.2) =
      f (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f (n + 1)
⊢ Eq (α := R) ((μ • g' : (a : ℕ) → R) (n + 1) : R) ((f' : (a : ℕ) → R) (n + 1) : R) ↔
    n + 1 > 0 → ∑ x ∈ (n + 1).divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f (n + 1)

Tactic:
simp only [forall_prop_of_true, succ_pos', smul_apply, f', g', coe_mk, succ_ne_zero,
        ite_false]

Premises used: Nat.succ_pos', ite_false, ArithmeticFunction.smul_apply, ArithmeticFunction.coe_mk, Nat.succ_ne_zero, forall_prop_of_true
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
rw :
  ∀ (x : ℕ × ℕ) (hx : x ∈ (n + 1).divisorsAntidiagonal),
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (if x.2 = 0 then 0 else g x.2) =
      HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
⊢ ∑ x ∈ (n + 1).divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (if x.2 = 0 then 0 else g x.2) =
      f (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f (n + 1)

Tactic:
rw [sum_congr rfl fun x hx => ?_]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
x : ℕ × ℕ
hx : x ∈ (n + 1).divisorsAntidiagonal
rw rw₁ :
  HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)
⊢ HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (if x.2 = 0 then 0 else g x.2) =
    HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2)

Tactic:
rw [if_neg (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)).ne']

Premises used: Nat.snd_mem_divisors_of_mem_antidiagonal, LT.lt.ne', if_neg, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun (x : ℕ) ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
h :
  Eq (α := R) ((μ • g' : (a : ℕ) → R) 0 : R) ((f' : (a : ℕ) → R) 0 : R) ↔
    GT.gt (α := ℕ) 0 0 → ∑ x ∈ divisorsAntidiagonal 0, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f 0
h₁ :
  ∀ (n : ℕ),
    Eq (α := R) ((μ • g' : (a : ℕ) → R) (n + 1) : R) ((f' : (a : ℕ) → R) (n + 1) : R) ↔
      n + 1 > 0 →
        ∑ x ∈ (n + 1).divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f (n + 1)
⊢ Eq (α := R) ((μ • g' : (a : ℕ) → R) n : R) ((f' : (a : ℕ) → R) n : R) ↔
    n > 0 → ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n

Tactic:
cases n with
    | zero => simp
    | succ n =>
      simp only [forall_prop_of_true, succ_pos', smul_apply, f', g', coe_mk, succ_ne_zero,
        ite_false]
      rw [sum_congr rfl fun x hx => ?_]
      rw [if_neg (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)).ne']

Premises used: Nat.succ_pos', ArithmeticFunction.zero, ite_false, ArithmeticFunction.smul_apply, ArithmeticFunction.coe_mk, Nat.succ_ne_zero, forall_prop_of_true, Nat.succ, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
rw :
  (∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n

Tactic:
rw [sum_eq_iff_sum_smul_moebius_eq]

Premises used: ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
h :
  ∀ (a : ℕ),
    a > 0 → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a
⊢ (∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f n

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    a > 0 → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a

Tactic:
fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left

Premises used: imp_congr_right, Eq.congr_left, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
h :
  ∀ a > 0,
    ∀ (x : ℕ × ℕ) (_hx : x ∈ a.divisorsAntidiagonal),
      HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2
⊢ ∀ (a : ℕ),
    a > 0 → ∑ x ∈ a.divisorsAntidiagonal, HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = f a ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = f a

Tactic:
refine fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left

Premises used: imp_congr_right, Eq.congr_left, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : NonAssocRing R
f g : ℕ → R
a : ℕ
h_1 : a > 0
x : ℕ × ℕ
_hx : x ∈ a.divisorsAntidiagonal
h h₁ : (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2 = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2
⊢ HSMul.hSMul (α := ℤ) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) (g x.2) = (↑((μ : (a : ℕ) → ℤ) x.1) : R) * g x.2

Tactic:
rw [zsmul_eq_mul]

Premises used: zsmul_eq_mul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroup R
f g : ℕ → R
⊢ (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
@sum_eq_iff_sum_smul_moebius_eq (Additive R) _ _ _

Premises used: Additive, Multiset.prod, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq, Finset.prod
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
⊢ (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
Iff.trans
        (Iff.trans (forall_congr' fun n => ?_)
          (@prod_eq_iff_prod_pow_moebius_eq Rˣ _
            (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1) fun n =>
            if h : 0 < n then Units.mk0 (g n) (hg n h) else 1))
        (forall_congr' fun n => ?_)

Premises used: ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq, forall_congr', Iff.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
refine_1 :
  ∀ (n : ℕ),
    n > 0 → ∏ i ∈ n.divisors, f i = g n ↔
      n > 0 →
        Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1)
          (if h : 0 < n then Units.mk0 (g n) ⋯ else 1)
refine_2 :
  ∀ (n : ℕ),
    n > 0 →
        Eq.{u_1 + 1} (α := Rˣ)
          (∏ x ∈ n.divisorsAntidiagonal,
            HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
          (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
      n > 0 → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n
⊢ (∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
refine
      Iff.trans
        (Iff.trans (forall_congr' fun n => ?_)
          (@prod_eq_iff_prod_pow_moebius_eq Rˣ _
            (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1) fun n =>
            if h : 0 < n then Units.mk0 (g n) (hg n h) else 1))
        (forall_congr' fun n => ?_)

Premises used: ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq, forall_congr', Iff.trans
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
⊢ n > 0 → ∏ i ∈ n.divisors, f i = g n ↔
    n > 0 →
      Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1)
        (if h : 0 < n then Units.mk0 (g n) ⋯ else 1)

Tactic:
imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
refine_1 :
  ∀ (hn : n > 0),
    ∏ i ∈ n.divisors, f i = g n ↔
      Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1)
        (if h : 0 < n then Units.mk0 (g n) ⋯ else 1)
⊢ n > 0 → ∏ i ∈ n.divisors, f i = g n ↔
    n > 0 →
      Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1)
        (if h : 0 < n then Units.mk0 (g n) ⋯ else 1)

Tactic:
refine imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
⊢ n > 0 →
      Eq.{u_1 + 1} (α := Rˣ)
        (∏ x ∈ n.divisorsAntidiagonal,
          HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
        (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n > 0 → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
refine_2 :
  ∀ (hn : n > 0),
    Eq.{u_1 + 1} (α := Rˣ)
        (∏ x ∈ n.divisorsAntidiagonal,
          HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
        (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
      ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n
⊢ n > 0 →
      Eq.{u_1 + 1} (α := Rˣ)
        (∏ x ∈ n.divisorsAntidiagonal,
          HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
        (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n > 0 → ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
refine imp_congr_right fun hn => ?_

Premises used: imp_congr_right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
rw : ∀ x ∈ n.divisors, f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)
⊢ ∏ i ∈ n.divisors, f i = g n ↔
    Eq.{u_1 + 1} (α := Rˣ) (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1)
      (if h : 0 < n then Units.mk0 (g n) ⋯ else 1)

Tactic:
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]

Premises used: dif_pos, Finset.prod_congr, map_prod, Units.val_inj, Units.coeHom_apply, Units.val_mk0, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ n.divisors
rw : f x = (Units.coeHom R : (a : Rˣ) → R) (Units.mk0 (f x) ⋯)
rw₁ : f x = (↑(Units.mk0 (f x) ⋯) : R)
rw₂ rw₃ : f x = f x
⊢ f x = (Units.coeHom R : (a : Rˣ) → R) (if h : 0 < x then Units.mk0 (f x) ⋯ else 1)

Tactic:
rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]

Premises used: dif_pos, Units.coeHom_apply, Units.val_mk0, Nat.pos_of_mem_divisors
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
rw :
  ∀ x ∈ n.divisorsAntidiagonal,
    (Units.coeHom R : (a : Rˣ) → R)
        (HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)) =
      HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ)
⊢ Eq.{u_1 + 1} (α := Rˣ)
      (∏ x ∈ n.divisorsAntidiagonal,
        HPow.hPow (α := Rˣ) (β := ℤ) (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ((μ : (a : ℕ) → ℤ) x.1 : ℤ))
      (if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, HPow.hPow (β := ℤ) (g x.2) ((μ : (a : ℕ) → ℤ) x.1 : ℤ) = f n

Tactic:
rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]

Premises used: dif_pos, Finset.prod_congr, map_prod, Units.val_inj, Units.coeHom_apply, Units.val_mk0, rfl