awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : x = 0
⊢ Eq (α := R)
    (∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((1 : (a : ℕ) → R) x.2 : R) :
      R)
    ((f : (a : ℕ) → R) x : R)

Tactic:
simp [x0]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
⊢ {(x, 1)} ⊆ x.divisorsAntidiagonal

Tactic:
simp [x0]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
⊢ {(x, 1)} ⊆ x.divisorsAntidiagonal

Tactic:
have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ x.divisorsAntidiagonal
neg :
  Eq (α := R) (∑ x ∈ {(x, 1)}, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((1 : (a : ℕ) → R) x.2 : R) : R)
    ((f : (a : ℕ) → R) x : R)
neg₁ :
  ∀ x_1 ∈ x.divisorsAntidiagonal,
    x_1 ∉ {(x, 1)} → HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x_1.1 : R) ((1 : (a : ℕ) → R) x_1.2 : R) = 0
⊢ Eq (α := R)
    (∑ x ∈ x.divisorsAntidiagonal, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((1 : (a : ℕ) → R) x.2 : R) :
      R)
    ((f : (a : ℕ) → R) x : R)

Tactic:
rw [← sum_subset h]

Premises used: Finset.sum_subset
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ x.divisorsAntidiagonal
⊢ Eq (α := R) (∑ x ∈ {(x, 1)}, HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) x.1 : R) ((1 : (a : ℕ) → R) x.2 : R) : R)
    ((f : (a : ℕ) → R) x : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ x.divisorsAntidiagonal
y₁ y₂ : ℕ
ymem : (y₁, y₂) ∈ x.divisorsAntidiagonal
ynotMem : (y₁, y₂) ∉ {(x, 1)}
con : y₂ = 1
⊢ False

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ x.divisorsAntidiagonal
y₁ y₂ : ℕ
ymem : (y₁, y₂) ∈ x.divisorsAntidiagonal
ynotMem : (y₁, y₂) ∉ {(x, 1)}
⊢ y₂ ≠ 1

Tactic:
have y2ne : y₂ ≠ 1 := by
      intro con
      simp_all
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ x.divisorsAntidiagonal
y₁ y₂ : ℕ
ymem : (y₁, y₂) ∈ x.divisorsAntidiagonal
ynotMem : (y₁, y₂) ∉ {(x, 1)}
y2ne : y₂ ≠ 1
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) (y₁, y₂).1 : R) ((1 : (a : ℕ) → R) (y₁, y₂).2 : R) = 0

Tactic:
simp [y2ne]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((0 * f : (a : ℕ) → R) x : R) ((0 : (a : ℕ) → R) x : R)
⊢ 0 * f = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((0 * f : (a : ℕ) → R) x : R) ((0 : (a : ℕ) → R) x : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((f * 0 : (a : ℕ) → R) x : R) ((0 : (a : ℕ) → R) x : R)
⊢ f * 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((f * 0 : (a : ℕ) → R) x : R) ((0 : (a : ℕ) → R) x : R)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
a b c : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((a * (b + c) : (a : ℕ) → R) x : R) ((a * b + a * c : (a : ℕ) → R) x : R)
⊢ a * (b + c) = a * b + a * c

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
a b c : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) ((a * (b + c) : (a : ℕ) → R) x : R) ((a * b + a * c : (a : ℕ) → R) x : R)

Tactic:
simp [← sum_add_distrib, mul_add]

Premises used: Finset.sum_add_distrib, mul_add
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
a b c : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) (((a + b) * c : (a : ℕ) → R) x : R) ((a * c + b * c : (a : ℕ) → R) x : R)
⊢ (a + b) * c = a * c + b * c

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Semiring R
a b c : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R) (((a + b) * c : (a : ℕ) → R) x : R) ((a * c + b * c : (a : ℕ) → R) x : R)

Tactic:
simp [← sum_add_distrib, add_mul]

Premises used: add_mul, Finset.sum_add_distrib
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := R) ((f * g : (a : ℕ) → R) x : R) ((g * f : (a : ℕ) → R) x : R)
⊢ f * g = g * f

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
x : ℕ
h :
  Eq (α := R)
    (∑ x ∈ x.divisorsAntidiagonal,
        HMul.hMul (α := R) (β := R)
          ((f : (a : ℕ) → R) (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).1 : R)
          ((g : (a : ℕ) → R) (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).2 : R) :
      R)
    ((g * f : (a : ℕ) → R) x : R)
⊢ Eq (α := R) ((f * g : (a : ℕ) → R) x : R) ((g * f : (a : ℕ) → R) x : R)

Tactic:
rw [mul_apply, ← map_swap_divisorsAntidiagonal, sum_map]

Premises used: Nat.map_swap_divisorsAntidiagonal, Finset.sum_map, ArithmeticFunction.mul_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
x : ℕ
⊢ Eq (α := R)
    (∑ x ∈ x.divisorsAntidiagonal,
        HMul.hMul (α := R) (β := R)
          ((f : (a : ℕ) → R) (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).1 : R)
          ((g : (a : ℕ) → R) (((Equiv.prodComm ℕ ℕ).toEmbedding : (a : ℕ × ℕ) → ℕ × ℕ) x).2 : R) :
      R)
    ((g * f : (a : ℕ) → R) x : R)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
x : R
f : ArithmeticFunction S
⊢ HSMul.hSMul (β := (a : ℕ) → S) x (⇑f : (a : ℕ) → S) 0 = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
x : R
f : ArithmeticFunction S
n : ℕ
⊢ (x • f : (a : ℕ) → S) n = HSMul.hSMul (β := S) x ((f : (a : ℕ) → S) n : S)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : R
f g : ArithmeticFunction S
n : ℕ
⊢ Eq (α := S) ((x • f * g : (a : ℕ) → S) n : S) ((x • (f * g) : (a : ℕ) → S) n : S)

Tactic:
simp [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : R
f g : ArithmeticFunction S
n : ℕ
⊢ Eq (α := S) ((f * x • g : (a : ℕ) → S) n : S) ((x • (f * g) : (a : ℕ) → S) n : S)

Tactic:
simp [Finset.smul_sum]

Premises used: Finset.smul_sum
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
x : R
⊢ Eq.{u_2 + 1} (α := S)
    ((((algebraMap R (ArithmeticFunction S) : (a : R) → ArithmeticFunction S) x : ArithmeticFunction S) : (a : ℕ) → S)
        1 :
      S)
    ((algebraMap R S : (a : R) → S) x : S)

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : ArithmeticFunction R
h : ∀ (x : ℕ), Eq (α := M) ((HSMul.hSMul (β := ArithmeticFunction M) r 0 : (a : ℕ) → M) x : M) ((0 : (a : ℕ) → M) x : M)
⊢ HSMul.hSMul (β := ArithmeticFunction M) r 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : ArithmeticFunction R
x : ℕ
⊢ Eq (α := M) ((HSMul.hSMul (β := ArithmeticFunction M) r 0 : (a : ℕ) → M) x : M) ((0 : (a : ℕ) → M) x : M)

Tactic:
simp only [smul_apply, sum_const_zero, smul_zero, zero_apply]

Premises used: ArithmeticFunction.smul_apply, smul_zero, Finset.sum_const_zero, ArithmeticFunction.zero_apply
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : ArithmeticFunction R
x y : ArithmeticFunction M
h : ∀ (x_1 : ℕ), Eq (α := M) ((r • (x + y) : (a : ℕ) → M) x_1 : M) ((r • x + r • y : (a : ℕ) → M) x_1 : M)
⊢ r • (x + y) = r • x + r • y

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : ArithmeticFunction R
x y : ArithmeticFunction M
x_1 : ℕ
⊢ Eq (α := M) ((r • (x + y) : (a : ℕ) → M) x_1 : M) ((r • x + r • y : (a : ℕ) → M) x_1 : M)

Tactic:
simp only [sum_add_distrib, smul_add, smul_apply, add_apply]

Premises used: Finset.sum_add_distrib, ArithmeticFunction.smul_apply, ArithmeticFunction.add_apply, smul_add
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
h : ∀ (x_1 : ℕ), Eq (α := M) (((r + s) • x : (a : ℕ) → M) x_1 : M) ((r • x + s • x : (a : ℕ) → M) x_1 : M)
⊢ (r + s) • x = r • x + s • x

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
x_1 : ℕ
⊢ Eq (α := M) (((r + s) • x : (a : ℕ) → M) x_1 : M) ((r • x + s • x : (a : ℕ) → M) x_1 : M)

Tactic:
simp only [add_smul, sum_add_distrib, smul_apply, add_apply]

Premises used: Finset.sum_add_distrib, ArithmeticFunction.smul_apply, ArithmeticFunction.add_apply, add_smul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : ArithmeticFunction M
h :
  ∀ (x : ℕ),
    Eq (α := M) ((HSMul.hSMul.{u_1, u_2, u_2} (α := ArithmeticFunction R) 0 r : (a : ℕ) → M) x : M)
      ((0 : (a : ℕ) → M) x : M)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ArithmeticFunction R) 0 r = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : ArithmeticFunction M
x : ℕ
⊢ Eq (α := M) ((HSMul.hSMul.{u_1, u_2, u_2} (α := ArithmeticFunction R) 0 r : (a : ℕ) → M) x : M)
    ((0 : (a : ℕ) → M) x : M)

Tactic:
simp only [smul_apply, sum_const_zero, zero_smul, zero_apply]

Premises used: ArithmeticFunction.smul_apply, Finset.sum_const_zero, ArithmeticFunction.zero_apply, zero_smul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ℕ → R
hf : Invertible (f 1)
rw :
  (if Eq (α := ℕ) 0 0 then 0
    else
      if Eq (α := ℕ) 0 1 then @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _
      else
        -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
          ∑ d : ↥(properDivisors 0),
            have this := ⋯;
            f (0 / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    0
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ dirichletInverseFun f hf 0 = 0

Tactic:
rw [dirichletInverseFun, if_pos rfl]

Premises used: ArithmeticFunction.dirichletInverseFun, if_pos, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ℕ → R
hf : Invertible (f 1)
rw :
  (if Eq (α := ℕ) 1 0 then 0
    else
      if Eq (α := ℕ) 1 1 then @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _
      else
        -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
          ∑ d : ↥(properDivisors 1),
            have this := ⋯;
            f (1 / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _
rw₁ :
  (if Eq (α := ℕ) 1 1 then @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _
    else
      -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
        ∑ d : ↥(properDivisors 1),
          have this := ⋯;
          f (1 / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _
rw₂ rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _
⊢ dirichletInverseFun f hf 1 = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _

Tactic:
rw [dirichletInverseFun, if_neg one_ne_zero, if_pos rfl]

Premises used: ArithmeticFunction.dirichletInverseFun, if_pos, one_ne_zero, if_neg, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
rw :
  (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d : ↥n.properDivisors,
        have this := ⋯;
        f (n / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d
⊢ dirichletInverseFun f hf n =
    -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
rw [dirichletInverseFun, if_neg hn0, if_neg hn1]

Premises used: ArithmeticFunction.dirichletInverseFun, if_neg
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
rw :
  -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
    ∑ x : ↥n.properDivisors, f (n / (↑x : ℕ)) * dirichletInverseFun f hf (↑x : ℕ)
| -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
    ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
rw [← Finset.sum_attach, Finset.attach_eq_univ]

Premises used: Finset.attach_eq_univ, Finset.sum_attach
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
conv_rhs :
  (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d : ↥n.properDivisors,
        have this := ⋯;
        f (n / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d
conv_rhs₁ :
  (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d : ↥n.properDivisors,
        have this := ⋯;
        f (n / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ x : ↥n.properDivisors, f (n / (↑x : ℕ)) * dirichletInverseFun f hf (↑x : ℕ)
⊢ (-@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d : ↥n.properDivisors,
        have this := ⋯;
        f (n / (↑d : ℕ)) * dirichletInverseFun f hf (↑d : ℕ)) =
    -@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (f 1) _ *
      ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
conv_rhs => rw [← Finset.sum_attach, Finset.attach_eq_univ]

Premises used: Finset.attach_eq_univ, Finset.sum_attach
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
h : ∀ (n : ℕ), Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
⊢ f * dirichletInverse (⇑f : (a : ℕ) → R) hf = 1

Tactic:
ext n
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
n : ℕ
pos :
  ∀ (hn0 : n = 0),
    Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
neg :
  ∀ (hn0 : ¬n = 0),
    Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
⊢ Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
by_cases hn0 : n = 0
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
n : ℕ
hn0 : n = 0
⊢ Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
simp [hn0]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
n : ℕ
hn0 : ¬n = 0
pos :
  ∀ (hn1 : n = 1),
    Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
neg :
  ∀ (hn1 : ¬n = 1),
    Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)
⊢ Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
by_cases hn1 : n = 1
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
n : ℕ
hn0 : ¬n = 0
hn1 : n = 1
⊢ Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
simp [hn1]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
neg :
  Eq.{u_1 + 1} (α := R)
    (∑ i ∈ cons n n.properDivisors ⋯,
        HMul.hMul (α := R) ((f : (a : ℕ) → R) (n / i) : R) (dirichletInverseFun (⇑f : (a : ℕ) → R) hf i) :
      R)
    ((1 : (a : ℕ) → R) n : R)
⊢ Eq (α := R) ((f * dirichletInverse (⇑f : (a : ℕ) → R) hf : (a : ℕ) → R) n : R) ((1 : (a : ℕ) → R) n : R)

Tactic:
rw [dirichletInverse, mul_apply, coe_mk,
    Nat.sum_divisorsAntidiagonal' fun x y ↦ f x * dirichletInverseFun f hf y,
    ← Nat.cons_self_properDivisors hn0]

Premises used: HMul.hMul, ArithmeticFunction.dirichletInverseFun, ArithmeticFunction.coe_mk, ArithmeticFunction.dirichletInverse, Nat.cons_self_properDivisors, Nat.sum_divisorsAntidiagonal', ArithmeticFunction.mul_apply, DFunLike.coe
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : Ring R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i ∈ cons n n.properDivisors ⋯,
        HMul.hMul (α := R) ((f : (a : ℕ) → R) (n / i) : R) (dirichletInverseFun (⇑f : (a : ℕ) → R) hf i) :
      R)
    ((1 : (a : ℕ) → R) n : R)

Tactic:
simp [hn0, hn1, pos_of_ne_zero]

Premises used: pos_of_ne_zero
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
hf : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R)
rw : f * dirichletInverse (⇑f : (a : ℕ) → R) hf = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := ArithmeticFunction R) 1 1
⊢ dirichletInverse (⇑f : (a : ℕ) → R) hf * f = 1

Tactic:
rw [mul_comm, self_mul_dirichletInverse]

Premises used: ArithmeticFunction.self_mul_dirichletInverse, mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
mp : IsUnit f → IsUnit (M := R) ((f : (a : ℕ) → R) 1 : R)
mpr : IsUnit (M := R) ((f : (a : ℕ) → R) 1 : R) → IsUnit f
⊢ IsUnit f ↔ IsUnit (M := R) ((f : (a : ℕ) → R) 1 : R)

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ IsUnit (M := R) (((↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)

Tactic:
⟨⟨f.val 1, f⁻¹.val 1, ?_, ?_⟩, rfl⟩

Premises used: Units.val, IsUnit, Inv.inv, Units.mk, Exists.intro, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : (ArithmeticFunction R)ˣ
mp :
  HMul.hMul (α := R) (β := R) (((↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
      (((↑f⁻¹ : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) =
    1
mp₁ :
  HMul.hMul (α := R) (β := R) (((↑f⁻¹ : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
      (((↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) =
    1
⊢ IsUnit (M := R) (((↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)

Tactic:
refine ⟨⟨f.val 1, f⁻¹.val 1, ?_, ?_⟩, rfl⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : (ArithmeticFunction R)ˣ
mp : Eq (α := R) (((↑f : ArithmeticFunction R) * (↑f⁻¹ : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) (1 : R)
mp₁ : Eq.{u_1 + 1} (α := R) ((1 : (a : ℕ) → R) 1 : R) (1 : R)
mp₂ mp₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (β := R) (((↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
      (((↑f⁻¹ : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) =
    1

Tactic:
rw [← ArithmeticFunction.mul_apply_one, Units.mul_inv, one_one]

Premises used: Units.mul_inv, ArithmeticFunction.one_one, ArithmeticFunction.mul_apply_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : (ArithmeticFunction R)ˣ
mp : Eq (α := R) (((↑f⁻¹ : ArithmeticFunction R) * (↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) (1 : R)
mp₁ : Eq.{u_1 + 1} (α := R) ((1 : (a : ℕ) → R) 1 : R) (1 : R)
mp₂ mp₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) (β := R) (((↑f⁻¹ : ArithmeticFunction R) : (a : ℕ) → R) 1 : R)
      (((↑f : ArithmeticFunction R) : (a : ℕ) → R) 1 : R) =
    1

Tactic:
rw [← ArithmeticFunction.mul_apply_one, Units.inv_mul, one_one]

Premises used: Units.inv_mul, ArithmeticFunction.one_one, ArithmeticFunction.mul_apply_one
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
this : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R) → Invertible f
⊢ IsUnit (M := R) ((f : (a : ℕ) → R) 1 : R) → IsUnit f

Tactic:
simpa using Nonempty.map this

Premises used: Nonempty.map
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
mpr : Invertible (α := R) ((f : (a : ℕ) → R) 1 : R) → Invertible f
⊢ IsUnit (M := R) ((f : (a : ℕ) → R) 1 : R) → IsUnit f

Tactic:
suffices Invertible (f 1) → Invertible f by simpa using Nonempty.map this
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : CommRing R
f : ArithmeticFunction R
⊢ Invertible (α := R) ((f : (a : ℕ) → R) 1 : R) → Invertible f

Tactic:
exact fun hf ↦ ⟨_, dirichletInverse_mul_self f hf, self_mul_dirichletInverse f hf⟩
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
h : f.IsMultiplicative
⊢ Eq (α := R) ((f : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
inst : MonoidWithZero R
f : ArithmeticFunction R
hf : f.IsMultiplicative
m n : ℕ
h : m.gcd n = 1
⊢ (f : (a : ℕ) → R) (m * n) = HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R)

Tactic:
hf.2 h

Premises used: And.right
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Defs
Goal:
R : Type u_1
ι : Type u_2
inst : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
hs : (↑∅ : Set ι).Pairwise (Coprime on g)
⊢ Eq (α := R) ((f : (a : ℕ) → R) (∏ i ∈ ∅, g i) : R) (∏ i ∈ ∅, (f : (a : ℕ) → R) (g i) : R)

Tactic:
simp [hf]