[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
f : ArithmeticFunction ℕ
⊢ (fun n => ↑(↑f n)) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℤ
⊢ (fun n => ↑(↑f n)) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
⊢ ↑↑f = ↑f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑↑f x✝ = ↑↑f x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑↑1 n = ↑1 n
[PROOFSTEP]
simp [one_apply]
[GOAL]
R : Type u_1
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑↑1 n = ↑1 n
[PROOFSTEP]
simp [one_apply]
[GOAL]
R : Type u_1
inst✝ : AddMonoid R
f g : ArithmeticFunction R
⊢ (fun n => ↑f n + ↑g n) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
n : ℕ
⊢ (fun x => if x = 1 then ↑n else 0) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
x✝ : ℕ
⊢ ↑(NatCast.natCast 0) x✝ = ↑0 x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
n x : ℕ
⊢ ↑(NatCast.natCast (n + 1)) x = ↑(NatCast.natCast n + 1) x
[PROOFSTEP]
by_cases h : x = 1
[GOAL]
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
n x : ℕ
h : x = 1
⊢ ↑(NatCast.natCast (n + 1)) x = ↑(NatCast.natCast n + 1) x
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
src✝¹ : AddMonoid (ArithmeticFunction R) := instAddMonoid
src✝ : One (ArithmeticFunction R) := one
n x : ℕ
h : ¬x = 1
⊢ ↑(NatCast.natCast (n + 1)) x = ↑(NatCast.natCast n + 1) x
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
inst✝ : AddGroup R
src✝ : AddMonoid (ArithmeticFunction R) := instAddMonoid
f : ArithmeticFunction R
⊢ (fun n => -↑f n) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
⊢ AddGroup (ArithmeticFunction R)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Zero R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
f : ArithmeticFunction R
g : ArithmeticFunction M
⊢ (fun n => ∑ x in divisorsAntidiagonal n, ↑f x.fst • ↑g x.snd) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction R
⊢ ↑(f * g) 1 = ↑f 1 * ↑g 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
⊢ ↑(f * g) = ↑f * ↑g
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
n : ℕ
⊢ ↑↑(f * g) n = ↑(↑f * ↑g) n
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
⊢ ↑(f * g) = ↑f * ↑g
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ArithmeticFunction ℤ
n : ℕ
⊢ ↑↑(f * g) n = ↑(↑f * ↑g) n
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
⊢ (f * g) • h = f • g • h
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ↑((f * g) • h) n = ↑(f • g • h) n
[PROOFSTEP]
simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, Finset.sum_sigma']
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∑ x in Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst,
      ↑f x.snd.fst • ↑g x.snd.snd • ↑h x.fst.snd =
    ∑ x in Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd,
      ↑f x.fst.fst • ↑g x.snd.fst • ↑h x.snd.snd
[PROOFSTEP]
apply Finset.sum_bij
[GOAL]
case h.hi
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ) (ha : a ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst),
    ?h.i a ha ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd
case h.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ) (ha : a ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst),
    ↑f a.snd.fst • ↑g a.snd.snd • ↑h a.fst.snd =
      ↑f (?h.i a ha).fst.fst • ↑g (?h.i a ha).snd.fst • ↑h (?h.i a ha).snd.snd
case h.i_inj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (a₁ a₂ : (_ : ℕ × ℕ) × ℕ × ℕ) (ha₁ : a₁ ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst)
    (ha₂ : a₂ ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst),
    ?h.i a₁ ha₁ = ?h.i a₂ ha₂ → a₁ = a₂
case h.i_surj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (b : (_ : ℕ × ℕ) × ℕ × ℕ),
    (b ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd) → ∃ a ha, b = ?h.i a ha
case h.i
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ (a : (_ : ℕ × ℕ) × ℕ × ℕ) →
    (a ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ
[PROOFSTEP]
pick_goal 5
[GOAL]
case h.i
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ (a : (_ : ℕ × ℕ) × ℕ × ℕ) →
    (a ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ
[PROOFSTEP]
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ _H
[GOAL]
case h.i.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
_H : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst
⊢ (_ : ℕ × ℕ) × ℕ × ℕ
[PROOFSTEP]
exact ⟨(k, l * j), (l, j)⟩
[GOAL]
case h.hi
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ) (ha : a ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst),
    Sigma.casesOn (motive := fun x =>
        (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ) a
        (fun fst snd =>
          Prod.casesOn (motive := fun x =>
            ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
              (_ : ℕ × ℕ) × ℕ × ℕ)
            fst fun i j =>
            Prod.casesOn (motive := fun x =>
              ({ fst := (i, j), snd := x } ∈
                  Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                (_ : ℕ × ℕ) × ℕ × ℕ)
              snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
        ha ∈
      Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd
[PROOFSTEP]
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H
[GOAL]
case h.hi.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst
⊢ Sigma.casesOn (motive := fun x =>
      (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
      { fst := (i, j), snd := (k, l) }
      (fun fst snd =>
        Prod.casesOn (motive := fun x =>
          ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
            (_ : ℕ × ℕ) × ℕ × ℕ)
          fst fun i j =>
          Prod.casesOn (motive := fun x =>
            ({ fst := (i, j), snd := x } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
              (_ : ℕ × ℕ) × ℕ × ℕ)
            snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
      H ∈
    Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd
[PROOFSTEP]
simp only [Finset.mem_sigma, mem_divisorsAntidiagonal] at H ⊢
[GOAL]
case h.hi.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : (i * j = n ∧ n ≠ 0) ∧ k * l = i ∧ i ≠ 0
⊢ (k * (l * j) = n ∧ n ≠ 0) ∧ True ∧ l * j ≠ 0
[PROOFSTEP]
rcases H with ⟨⟨rfl, n0⟩, rfl, i0⟩
[GOAL]
case h.hi.mk.mk.mk.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
j k l : ℕ
n0 : k * l * j ≠ 0
i0 : k * l ≠ 0
⊢ (k * (l * j) = k * l * j ∧ k * l * j ≠ 0) ∧ True ∧ l * j ≠ 0
[PROOFSTEP]
refine' ⟨⟨(mul_assoc _ _ _).symm, n0⟩, trivial, _⟩
[GOAL]
case h.hi.mk.mk.mk.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
j k l : ℕ
n0 : k * l * j ≠ 0
i0 : k * l ≠ 0
⊢ l * j ≠ 0
[PROOFSTEP]
rw [mul_ne_zero_iff] at *
[GOAL]
case h.hi.mk.mk.mk.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
j k l : ℕ
n0 : k * l ≠ 0 ∧ j ≠ 0
i0 : k ≠ 0 ∧ l ≠ 0
⊢ l ≠ 0 ∧ j ≠ 0
[PROOFSTEP]
exact ⟨i0.2, n0.2⟩
[GOAL]
case h.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (a : (_ : ℕ × ℕ) × ℕ × ℕ) (ha : a ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst),
    ↑f a.snd.fst • ↑g a.snd.snd • ↑h a.fst.snd =
      ↑f
          (Sigma.casesOn (motive := fun x =>
                (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ) a
                (fun fst snd =>
                  Prod.casesOn (motive := fun x =>
                    ({ fst := x, snd := snd } ∈
                        Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                      (_ : ℕ × ℕ) × ℕ × ℕ)
                    fst fun i j =>
                    Prod.casesOn (motive := fun x =>
                      ({ fst := (i, j), snd := x } ∈
                          Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                        (_ : ℕ × ℕ) × ℕ × ℕ)
                      snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
                ha).fst.fst •
        ↑g
            (Sigma.casesOn (motive := fun x =>
                  (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
                  a
                  (fun fst snd =>
                    Prod.casesOn (motive := fun x =>
                      ({ fst := x, snd := snd } ∈
                          Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                        (_ : ℕ × ℕ) × ℕ × ℕ)
                      fst fun i j =>
                      Prod.casesOn (motive := fun x =>
                        ({ fst := (i, j), snd := x } ∈
                            Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                          (_ : ℕ × ℕ) × ℕ × ℕ)
                        snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
                  ha).snd.fst •
          ↑h
            (Sigma.casesOn (motive := fun x =>
                  (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
                  a
                  (fun fst snd =>
                    Prod.casesOn (motive := fun x =>
                      ({ fst := x, snd := snd } ∈
                          Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                        (_ : ℕ × ℕ) × ℕ × ℕ)
                      fst fun i j =>
                      Prod.casesOn (motive := fun x =>
                        ({ fst := (i, j), snd := x } ∈
                            Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                          (_ : ℕ × ℕ) × ℕ × ℕ)
                        snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
                  ha).snd.snd
[PROOFSTEP]
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ _H
[GOAL]
case h.h.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
_H : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst
⊢ ↑f { fst := (i, j), snd := (k, l) }.snd.fst •
      ↑g { fst := (i, j), snd := (k, l) }.snd.snd • ↑h { fst := (i, j), snd := (k, l) }.fst.snd =
    ↑f
        (Sigma.casesOn (motive := fun x =>
              (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
              { fst := (i, j), snd := (k, l) }
              (fun fst snd =>
                Prod.casesOn (motive := fun x =>
                  ({ fst := x, snd := snd } ∈
                      Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                    (_ : ℕ × ℕ) × ℕ × ℕ)
                  fst fun i j =>
                  Prod.casesOn (motive := fun x =>
                    ({ fst := (i, j), snd := x } ∈
                        Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                      (_ : ℕ × ℕ) × ℕ × ℕ)
                    snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
              _H).fst.fst •
      ↑g
          (Sigma.casesOn (motive := fun x =>
                (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
                { fst := (i, j), snd := (k, l) }
                (fun fst snd =>
                  Prod.casesOn (motive := fun x =>
                    ({ fst := x, snd := snd } ∈
                        Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                      (_ : ℕ × ℕ) × ℕ × ℕ)
                    fst fun i j =>
                    Prod.casesOn (motive := fun x =>
                      ({ fst := (i, j), snd := x } ∈
                          Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                        (_ : ℕ × ℕ) × ℕ × ℕ)
                      snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
                _H).snd.fst •
        ↑h
          (Sigma.casesOn (motive := fun x =>
                (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
                { fst := (i, j), snd := (k, l) }
                (fun fst snd =>
                  Prod.casesOn (motive := fun x =>
                    ({ fst := x, snd := snd } ∈
                        Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                      (_ : ℕ × ℕ) × ℕ × ℕ)
                    fst fun i j =>
                    Prod.casesOn (motive := fun x =>
                      ({ fst := (i, j), snd := x } ∈
                          Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                        (_ : ℕ × ℕ) × ℕ × ℕ)
                      snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
                _H).snd.snd
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
case h.i_inj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (a₁ a₂ : (_ : ℕ × ℕ) × ℕ × ℕ) (ha₁ : a₁ ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst)
    (ha₂ : a₂ ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst),
    Sigma.casesOn (motive := fun x =>
          (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ) a₁
          (fun fst snd =>
            Prod.casesOn (motive := fun x =>
              ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                (_ : ℕ × ℕ) × ℕ × ℕ)
              fst fun i j =>
              Prod.casesOn (motive := fun x =>
                ({ fst := (i, j), snd := x } ∈
                    Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                  (_ : ℕ × ℕ) × ℕ × ℕ)
                snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
          ha₁ =
        Sigma.casesOn (motive := fun x =>
          (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ) a₂
          (fun fst snd =>
            Prod.casesOn (motive := fun x =>
              ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                (_ : ℕ × ℕ) × ℕ × ℕ)
              fst fun i j =>
              Prod.casesOn (motive := fun x =>
                ({ fst := (i, j), snd := x } ∈
                    Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                  (_ : ℕ × ℕ) × ℕ × ℕ)
                snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
          ha₂ →
      a₁ = a₂
[PROOFSTEP]
rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩ ⟨⟨i, j⟩, ⟨k, l⟩⟩ H₁ H₂
[GOAL]
case h.i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n a b c d i j k l : ℕ
H₁ : { fst := (a, b), snd := (c, d) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst
H₂ : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst
⊢ Sigma.casesOn (motive := fun x =>
        (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
        { fst := (a, b), snd := (c, d) }
        (fun fst snd =>
          Prod.casesOn (motive := fun x =>
            ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
              (_ : ℕ × ℕ) × ℕ × ℕ)
            fst fun i j =>
            Prod.casesOn (motive := fun x =>
              ({ fst := (i, j), snd := x } ∈
                  Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                (_ : ℕ × ℕ) × ℕ × ℕ)
              snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
        H₁ =
      Sigma.casesOn (motive := fun x =>
        (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
        { fst := (i, j), snd := (k, l) }
        (fun fst snd =>
          Prod.casesOn (motive := fun x =>
            ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
              (_ : ℕ × ℕ) × ℕ × ℕ)
            fst fun i j =>
            Prod.casesOn (motive := fun x =>
              ({ fst := (i, j), snd := x } ∈
                  Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                (_ : ℕ × ℕ) × ℕ × ℕ)
              snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
        H₂ →
    { fst := (a, b), snd := (c, d) } = { fst := (i, j), snd := (k, l) }
[PROOFSTEP]
simp only [Finset.mem_sigma, mem_divisorsAntidiagonal, and_imp, Prod.mk.inj_iff, add_comm, heq_iff_eq] at H₁ H₂ ⊢
[GOAL]
case h.i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n a b c d i j k l : ℕ
H₁ : (a * b = n ∧ n ≠ 0) ∧ c * d = a ∧ a ≠ 0
H₂ : (i * j = n ∧ n ≠ 0) ∧ k * l = i ∧ i ≠ 0
⊢ { fst := (c, d * b), snd := (d, b) } = { fst := (k, l * j), snd := (l, j) } →
    { fst := (a, b), snd := (c, d) } = { fst := (i, j), snd := (k, l) }
[PROOFSTEP]
simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_eq_eq, and_imp]
  -- porting note: added
[GOAL]
case h.i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n a b c d i j k l : ℕ
H₁ : (a * b = n ∧ n ≠ 0) ∧ c * d = a ∧ a ≠ 0
H₂ : (i * j = n ∧ n ≠ 0) ∧ k * l = i ∧ i ≠ 0
⊢ c = k → d * b = l * j → d = l → b = j → (a = i ∧ b = j) ∧ c = k ∧ d = l
[PROOFSTEP]
rintro h h2 rfl rfl
[GOAL]
case h.i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h✝ : ArithmeticFunction M
n a b c d i k : ℕ
H₁ : (a * b = n ∧ n ≠ 0) ∧ c * d = a ∧ a ≠ 0
h : c = k
H₂ : (i * b = n ∧ n ≠ 0) ∧ k * d = i ∧ i ≠ 0
h2 : d * b = d * b
⊢ (a = i ∧ b = b) ∧ c = k ∧ d = d
[PROOFSTEP]
subst h
[GOAL]
case h.i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n a b c d i : ℕ
H₁ : (a * b = n ∧ n ≠ 0) ∧ c * d = a ∧ a ≠ 0
h2 : d * b = d * b
H₂ : (i * b = n ∧ n ≠ 0) ∧ c * d = i ∧ i ≠ 0
⊢ (a = i ∧ b = b) ∧ c = c ∧ d = d
[PROOFSTEP]
exact ⟨⟨Eq.trans H₁.2.1.symm H₂.2.1, rfl⟩, rfl, rfl⟩
[GOAL]
case h.i_surj
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n : ℕ
⊢ ∀ (b : (_ : ℕ × ℕ) × ℕ × ℕ),
    (b ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd) →
      ∃ a ha,
        b =
          Sigma.casesOn (motive := fun x =>
            (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ) a
            (fun fst snd =>
              Prod.casesOn (motive := fun x =>
                ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                  (_ : ℕ × ℕ) × ℕ × ℕ)
                fst fun i j =>
                Prod.casesOn (motive := fun x =>
                  ({ fst := (i, j), snd := x } ∈
                      Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                    (_ : ℕ × ℕ) × ℕ × ℕ)
                  snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
            ha
[PROOFSTEP]
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H
[GOAL]
case h.i_surj.mk.mk.mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd
⊢ ∃ a ha,
    { fst := (i, j), snd := (k, l) } =
      Sigma.casesOn (motive := fun x =>
        (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ) a
        (fun fst snd =>
          Prod.casesOn (motive := fun x =>
            ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
              (_ : ℕ × ℕ) × ℕ × ℕ)
            fst fun i j =>
            Prod.casesOn (motive := fun x =>
              ({ fst := (i, j), snd := x } ∈
                  Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
                (_ : ℕ × ℕ) × ℕ × ℕ)
              snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
        ha
[PROOFSTEP]
refine' ⟨⟨(i * k, l), (i, k)⟩, _, _⟩
[GOAL]
case h.i_surj.mk.mk.mk.refine'_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd
⊢ { fst := (i * k, l), snd := (i, k) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst
[PROOFSTEP]
simp only [Finset.mem_sigma, mem_divisorsAntidiagonal] at H ⊢
[GOAL]
case h.i_surj.mk.mk.mk.refine'_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : (i * j = n ∧ n ≠ 0) ∧ k * l = j ∧ j ≠ 0
⊢ (i * k * l = n ∧ n ≠ 0) ∧ True ∧ i * k ≠ 0
[PROOFSTEP]
rcases H with ⟨⟨rfl, n0⟩, rfl, j0⟩
[GOAL]
case h.i_surj.mk.mk.mk.refine'_1.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
i k l : ℕ
n0 : i * (k * l) ≠ 0
j0 : k * l ≠ 0
⊢ (i * k * l = i * (k * l) ∧ i * (k * l) ≠ 0) ∧ True ∧ i * k ≠ 0
[PROOFSTEP]
refine' ⟨⟨mul_assoc _ _ _, n0⟩, trivial, _⟩
[GOAL]
case h.i_surj.mk.mk.mk.refine'_1.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
i k l : ℕ
n0 : i * (k * l) ≠ 0
j0 : k * l ≠ 0
⊢ i * k ≠ 0
[PROOFSTEP]
rw [mul_ne_zero_iff] at *
[GOAL]
case h.i_surj.mk.mk.mk.refine'_1.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
i k l : ℕ
n0 : i ≠ 0 ∧ k * l ≠ 0
j0 : k ≠ 0 ∧ l ≠ 0
⊢ i ≠ 0 ∧ k ≠ 0
[PROOFSTEP]
exact ⟨n0.1, j0.1⟩
[GOAL]
case h.i_surj.mk.mk.mk.refine'_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : { fst := (i, j), snd := (k, l) } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.snd
⊢ { fst := (i, j), snd := (k, l) } =
    Sigma.casesOn (motive := fun x =>
      (x ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) → (_ : ℕ × ℕ) × ℕ × ℕ)
      { fst := (i * k, l), snd := (i, k) }
      (fun fst snd =>
        Prod.casesOn (motive := fun x =>
          ({ fst := x, snd := snd } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
            (_ : ℕ × ℕ) × ℕ × ℕ)
          fst fun i j =>
          Prod.casesOn (motive := fun x =>
            ({ fst := (i, j), snd := x } ∈ Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst) →
              (_ : ℕ × ℕ) × ℕ × ℕ)
            snd fun k l _H => { fst := (k, l * j), snd := (l, j) })
      (_ :
        { fst := (i * k, l), snd := (i, k) } ∈
          Finset.sigma (divisorsAntidiagonal n) fun a => divisorsAntidiagonal a.fst)
[PROOFSTEP]
simp only [true_and_iff, mem_divisorsAntidiagonal, and_true_iff, Prod.mk.inj_iff, eq_self_iff_true, Ne.def, mem_sigma,
  heq_iff_eq] at H ⊢
[GOAL]
case h.i_surj.mk.mk.mk.refine'_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
n i j k l : ℕ
H : (i * j = n ∧ ¬n = 0) ∧ k * l = j ∧ ¬j = 0
⊢ { fst := (i, j), snd := (k, l) } = { fst := (i, k * l), snd := (k, l) }
[PROOFSTEP]
rw [H.2.1]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
⊢ 1 • b = b
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ↑(1 • b) x = ↑b x
[PROOFSTEP]
rw [smul_apply]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
[PROOFSTEP]
by_cases x0 : x = 0
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
[PROOFSTEP]
simp [x0]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
[PROOFSTEP]
have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
⊢ {(1, x)} ⊆ divisorsAntidiagonal x
[PROOFSTEP]
simp [x0]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in divisorsAntidiagonal x, ↑1 x.fst • ↑b x.snd = ↑b x
[PROOFSTEP]
rw [← sum_subset h]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in {(1, x)}, ↑1 x.fst • ↑b x.snd = ↑b x
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
⊢ ∀ (x_1 : ℕ × ℕ), x_1 ∈ divisorsAntidiagonal x → ¬x_1 ∈ {(1, x)} → ↑1 x_1.fst • ↑b x_1.snd = 0
[PROOFSTEP]
intro y ymem ynmem
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
⊢ ↑1 y.fst • ↑b y.snd = 0
[PROOFSTEP]
have y1ne : y.fst ≠ 1 := by
  intro con
  simp only [Con, mem_divisorsAntidiagonal, one_mul, Ne.def] at ymem 
  simp only [mem_singleton, Prod.ext_iff] at ynmem 
  cases y
  subst con
  simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem 
  tauto
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
⊢ y.fst ≠ 1
[PROOFSTEP]
intro con
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
con : y.fst = 1
⊢ False
[PROOFSTEP]
simp only [Con, mem_divisorsAntidiagonal, one_mul, Ne.def] at ymem 
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ynmem : ¬y ∈ {(1, x)}
con : y.fst = 1
ymem : y.fst * y.snd = x ∧ ¬x = 0
⊢ False
[PROOFSTEP]
simp only [mem_singleton, Prod.ext_iff] at ynmem 
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
con : y.fst = 1
ymem : y.fst * y.snd = x ∧ ¬x = 0
ynmem : ¬(y.fst = 1 ∧ y.snd = x)
⊢ False
[PROOFSTEP]
cases y
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
fst✝ snd✝ : ℕ
con : (fst✝, snd✝).fst = 1
ymem : (fst✝, snd✝).fst * (fst✝, snd✝).snd = x ∧ ¬x = 0
ynmem : ¬((fst✝, snd✝).fst = 1 ∧ (fst✝, snd✝).snd = x)
⊢ False
[PROOFSTEP]
subst con
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
snd✝ : ℕ
ymem : (1, snd✝).fst * (1, snd✝).snd = x ∧ ¬x = 0
ynmem : ¬((1, snd✝).fst = 1 ∧ (1, snd✝).snd = x)
⊢ False
[PROOFSTEP]
simp only [true_and, one_mul, x0, not_false_eq_true, and_true] at ynmem ymem 
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
snd✝ : ℕ
ynmem : ¬snd✝ = x
ymem : snd✝ = x
⊢ False
[PROOFSTEP]
tauto
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
x0 : ¬x = 0
h : {(1, x)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(1, x)}
y1ne : y.fst ≠ 1
⊢ ↑1 y.fst • ↑b y.snd = 0
[PROOFSTEP]
simp [y1ne]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f * 1 = f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑(f * 1) x = ↑f x
[PROOFSTEP]
rw [mul_apply]
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑1 x.snd = ↑f x
[PROOFSTEP]
by_cases x0 : x = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑1 x.snd = ↑f x
[PROOFSTEP]
simp [x0]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑1 x.snd = ↑f x
[PROOFSTEP]
have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
⊢ {(x, 1)} ⊆ divisorsAntidiagonal x
[PROOFSTEP]
simp [x0]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑1 x.snd = ↑f x
[PROOFSTEP]
rw [← sum_subset h]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
⊢ ∑ x in {(x, 1)}, ↑f x.fst * ↑1 x.snd = ↑f x
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
⊢ ∀ (x_1 : ℕ × ℕ), x_1 ∈ divisorsAntidiagonal x → ¬x_1 ∈ {(x, 1)} → ↑f x_1.fst * ↑1 x_1.snd = 0
[PROOFSTEP]
intro y ymem ynmem
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(x, 1)}
⊢ ↑f y.fst * ↑1 y.snd = 0
[PROOFSTEP]
have y2ne : y.snd ≠ 1 := by
  intro con
  cases y; subst con
  simp only [Con, mem_divisorsAntidiagonal, mul_one, Ne.def] at ymem 
  simp only [mem_singleton, Prod.ext_iff] at ynmem 
  tauto
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(x, 1)}
⊢ y.snd ≠ 1
[PROOFSTEP]
intro con
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(x, 1)}
con : y.snd = 1
⊢ False
[PROOFSTEP]
cases y
[GOAL]
case mk
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
fst✝ snd✝ : ℕ
ymem : (fst✝, snd✝) ∈ divisorsAntidiagonal x
ynmem : ¬(fst✝, snd✝) ∈ {(x, 1)}
con : (fst✝, snd✝).snd = 1
⊢ False
[PROOFSTEP]
subst con
[GOAL]
case mk
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
fst✝ : ℕ
ymem : (fst✝, 1) ∈ divisorsAntidiagonal x
ynmem : ¬(fst✝, 1) ∈ {(x, 1)}
⊢ False
[PROOFSTEP]
simp only [Con, mem_divisorsAntidiagonal, mul_one, Ne.def] at ymem 
[GOAL]
case mk
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
fst✝ : ℕ
ynmem : ¬(fst✝, 1) ∈ {(x, 1)}
ymem : fst✝ = x ∧ ¬x = 0
⊢ False
[PROOFSTEP]
simp only [mem_singleton, Prod.ext_iff] at ynmem 
[GOAL]
case mk
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
fst✝ : ℕ
ymem : fst✝ = x ∧ ¬x = 0
ynmem : ¬(fst✝ = x ∧ True)
⊢ False
[PROOFSTEP]
tauto
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
x0 : ¬x = 0
h : {(x, 1)} ⊆ divisorsAntidiagonal x
y : ℕ × ℕ
ymem : y ∈ divisorsAntidiagonal x
ynmem : ¬y ∈ {(x, 1)}
y2ne : y.snd ≠ 1
⊢ ↑f y.fst * ↑1 y.snd = 0
[PROOFSTEP]
simp [y2ne]
[GOAL]
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
a b c : ArithmeticFunction R
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
a b c : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(a * (b + c)) x✝ = ↑(a * b + a * c) x✝
[PROOFSTEP]
simp only [← sum_add_distrib, mul_add, mul_apply, add_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
a b c : ArithmeticFunction R
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
a b c : ArithmeticFunction R
x✝ : ℕ
⊢ ↑((a + b) * c) x✝ = ↑(a * c + b * c) x✝
[PROOFSTEP]
simp only [← sum_add_distrib, add_mul, mul_apply, add_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
f : ArithmeticFunction R
⊢ 0 * f = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
f : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(0 * f) x✝ = ↑0 x✝
[PROOFSTEP]
simp only [mul_apply, zero_mul, sum_const_zero, zero_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
f : ArithmeticFunction R
⊢ f * 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
src✝² : AddMonoidWithOne (ArithmeticFunction R) := instAddMonoidWithOne
src✝¹ : Monoid (ArithmeticFunction R) := instMonoid
src✝ : AddCommMonoid (ArithmeticFunction R) := instAddCommMonoid
f : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(f * 0) x✝ = ↑0 x✝
[PROOFSTEP]
simp only [mul_apply, sum_const_zero, mul_zero, zero_apply]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
src✝ : Semiring (ArithmeticFunction R) := instSemiring
f g : ArithmeticFunction R
⊢ f * g = g * f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
src✝ : Semiring (ArithmeticFunction R) := instSemiring
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(f * g) x✝ = ↑(g * f) x✝
[PROOFSTEP]
rw [mul_apply, ← map_swap_divisorsAntidiagonal, sum_map]
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
src✝ : Semiring (ArithmeticFunction R) := instSemiring
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ∑ x in divisorsAntidiagonal x✝,
      ↑f (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).fst * ↑g (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).snd =
    ↑(g * f) x✝
[PROOFSTEP]
simp [mul_comm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
⊢ r • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(r • 0) x✝ = ↑0 x✝
[PROOFSTEP]
simp only [smul_apply, sum_const_zero, smul_zero, zero_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
x y : ArithmeticFunction M
⊢ r • (x + y) = r • x + r • y
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
x y : ArithmeticFunction M
x✝ : ℕ
⊢ ↑(r • (x + y)) x✝ = ↑(r • x + r • y) x✝
[PROOFSTEP]
simp only [sum_add_distrib, smul_add, smul_apply, add_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
⊢ (r + s) • x = r • x + s • x
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
x✝ : ℕ
⊢ ↑((r + s) • x) x✝ = ↑(r • x + s • x) x✝
[PROOFSTEP]
simp only [add_smul, sum_add_distrib, smul_apply, add_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction M
⊢ 0 • r = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction M
x✝ : ℕ
⊢ ↑(0 • r) x✝ = ↑0 x✝
[PROOFSTEP]
simp only [smul_apply, sum_const_zero, zero_smul, zero_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ↑(↑ζ • f) x = ∑ i in divisors x, ↑f i
[PROOFSTEP]
rw [smul_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑↑ζ x.fst • ↑f x.snd = ∑ i in divisors x, ↑f i
[PROOFSTEP]
trans ∑ i in divisorsAntidiagonal x, f i.snd
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑↑ζ x.fst • ↑f x.snd = ∑ i in divisorsAntidiagonal x, ↑f i.snd
[PROOFSTEP]
refine' sum_congr rfl fun i hi => _
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal x
⊢ ↑↑ζ i.fst • ↑f i.snd = ↑f i.snd
[PROOFSTEP]
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal (i.fst * i.snd)
h : i.fst * i.snd ≠ 0
⊢ ↑↑ζ i.fst • ↑f i.snd = ↑f i.snd
[PROOFSTEP]
rw [natCoe_apply, zeta_apply_ne (left_ne_zero_of_mul h), cast_one, one_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i in divisorsAntidiagonal x, ↑f i.snd = ∑ i in divisors x, ↑f i
[PROOFSTEP]
rw [← map_div_left_divisors, sum_map, Function.Embedding.coeFn_mk]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑(f * ↑ζ) x = ∑ i in divisors x, ↑f i
[PROOFSTEP]
rw [mul_apply]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑↑ζ x.snd = ∑ i in divisors x, ↑f i
[PROOFSTEP]
trans ∑ i in divisorsAntidiagonal x, f i.1
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ x in divisorsAntidiagonal x, ↑f x.fst * ↑↑ζ x.snd = ∑ i in divisorsAntidiagonal x, ↑f i.fst
[PROOFSTEP]
refine' sum_congr rfl fun i hi => _
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal x
⊢ ↑f i.fst * ↑↑ζ i.snd = ↑f i.fst
[PROOFSTEP]
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
[GOAL]
case intro
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
i : ℕ × ℕ
hi : i ∈ divisorsAntidiagonal (i.fst * i.snd)
h : i.fst * i.snd ≠ 0
⊢ ↑f i.fst * ↑↑ζ i.snd = ↑f i.fst
[PROOFSTEP]
rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ i in divisorsAntidiagonal x, ↑f i.fst = ∑ i in divisors x, ↑f i
[PROOFSTEP]
rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
f g : ArithmeticFunction R
⊢ (fun x => ↑f x * ↑g x) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ pmul f g = pmul g f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ↑(pmul f g) x✝ = ↑(pmul g f) x✝
[PROOFSTEP]
simp [mul_comm]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ pmul f ↑ζ = f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑(pmul f ↑ζ) x = ↑f x
[PROOFSTEP]
cases x
[GOAL]
case h.zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ ↑(pmul f ↑ζ) Nat.zero = ↑f Nat.zero
[PROOFSTEP]
simp [Nat.succ_ne_zero]
[GOAL]
case h.succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ ↑(pmul f ↑ζ) (succ n✝) = ↑f (succ n✝)
[PROOFSTEP]
simp [Nat.succ_ne_zero]
[GOAL]
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ pmul (↑ζ) f = f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑(pmul (↑ζ) f) x = ↑f x
[PROOFSTEP]
cases x
[GOAL]
case h.zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ ↑(pmul (↑ζ) f) Nat.zero = ↑f Nat.zero
[PROOFSTEP]
simp [Nat.succ_ne_zero]
[GOAL]
case h.succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ ↑(pmul (↑ζ) f) (succ n✝) = ↑f (succ n✝)
[PROOFSTEP]
simp [Nat.succ_ne_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ (fun x => ↑f x ^ k) 0 = 0
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ ↑f 0 ^ k = 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
h0 : ¬k = 0
⊢ 0 ^ k = 0
[PROOFSTEP]
exact zero_pow (Nat.pos_of_ne_zero h0)
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ ppow f 0 = ↑ζ
[PROOFSTEP]
rw [ppow, dif_pos rfl]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ ↑(ppow f k) x = ↑f x ^ k
[PROOFSTEP]
rw [ppow, dif_neg (ne_of_gt kpos)]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ ↑{ toFun := fun x => ↑f x ^ k, map_zero' := (_ : (fun x => ↑f x ^ k) 0 = 0) } x = ↑f x ^ k
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
⊢ ppow f (k + 1) = pmul f (ppow f k)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ ↑(ppow f (k + 1)) x = ↑(pmul f (ppow f k)) x
[PROOFSTEP]
rw [ppow_apply (Nat.succ_pos k), _root_.pow_succ]
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ ↑f x * ↑f x ^ k = ↑(pmul f (ppow f k)) x
[PROOFSTEP]
induction k
[GOAL]
case h.zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ↑f x * ↑f x ^ Nat.zero = ↑(pmul f (ppow f Nat.zero)) x
[PROOFSTEP]
simp
[GOAL]
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ↑f x * ↑f x ^ n✝ = ↑(pmul f (ppow f n✝)) x
⊢ ↑f x * ↑f x ^ succ n✝ = ↑(pmul f (ppow f (succ n✝))) x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
⊢ ppow f (k + 1) = pmul (ppow f k) f
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ ↑(ppow f (k + 1)) x = ↑(pmul (ppow f k) f) x
[PROOFSTEP]
rw [ppow_apply (Nat.succ_pos k), _root_.pow_succ']
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ ↑f x ^ k * ↑f x = ↑(pmul (ppow f k) f) x
[PROOFSTEP]
induction k
[GOAL]
case h.zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
kpos : 0 < Nat.zero
⊢ ↑f x ^ Nat.zero * ↑f x = ↑(pmul (ppow f Nat.zero) f) x
[PROOFSTEP]
simp
[GOAL]
case h.succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
n_ih✝ : ∀ {kpos : 0 < n✝}, ↑f x ^ n✝ * ↑f x = ↑(pmul (ppow f n✝) f) x
kpos : 0 < succ n✝
⊢ ↑f x ^ succ n✝ * ↑f x = ↑(pmul (ppow f (succ n✝)) f) x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : GroupWithZero R
f g : ArithmeticFunction R
⊢ (fun n => ↑f n / ↑g n) 0 = 0
[PROOFSTEP]
simp only [map_zero, ne_eq, not_true, div_zero]
[GOAL]
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ pdiv f ↑ζ = f
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n : ℕ
⊢ ↑(pdiv f ↑ζ) n = ↑f n
[PROOFSTEP]
cases n
[GOAL]
case h.zero
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
⊢ ↑(pdiv f ↑ζ) Nat.zero = ↑f Nat.zero
[PROOFSTEP]
simp [succ_ne_zero]
[GOAL]
case h.succ
R : Type u_1
inst✝ : DivisionSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ ↑(pdiv f ↑ζ) (succ n✝) = ↑f (succ n✝)
[PROOFSTEP]
simp [succ_ne_zero]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s : Finset ι
hs : Set.Pairwise (↑s) (coprime on g)
⊢ ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
[PROOFSTEP]
classical
induction' s using Finset.induction_on with a s has ih hs
· simp [hf]
rw [coe_insert, Set.pairwise_insert_of_symmetric (coprime.symmetric.comap g)] at hs 
rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
exact Nat.coprime_prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm
[GOAL]
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s : Finset ι
hs : Set.Pairwise (↑s) (coprime on g)
⊢ ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
[PROOFSTEP]
induction' s using Finset.induction_on with a s has ih hs
[GOAL]
case empty
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s : Finset ι
hs✝ : Set.Pairwise (↑s) (coprime on g)
hs : Set.Pairwise (↑∅) (coprime on g)
⊢ ↑f (∏ i in ∅, g i) = ∏ i in ∅, ↑f (g i)
[PROOFSTEP]
simp [hf]
[GOAL]
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑(insert a s)) (coprime on g)
⊢ ↑f (∏ i in insert a s, g i) = ∏ i in insert a s, ↑f (g i)
[PROOFSTEP]
rw [coe_insert, Set.pairwise_insert_of_symmetric (coprime.symmetric.comap g)] at hs 
[GOAL]
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑s) (coprime on g) ∧ ∀ (b : ι), b ∈ ↑s → a ≠ b → (coprime on g) a b
⊢ ↑f (∏ i in insert a s, g i) = ∏ i in insert a s, ↑f (g i)
[PROOFSTEP]
rw [prod_insert has, prod_insert has, hf.map_mul_of_coprime, ih hs.1]
[GOAL]
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : IsMultiplicative f
s✝ : Finset ι
hs✝ : Set.Pairwise (↑s✝) (coprime on g)
a : ι
s : Finset ι
has : ¬a ∈ s
ih : Set.Pairwise (↑s) (coprime on g) → ↑f (∏ i in s, g i) = ∏ i in s, ↑f (g i)
hs : Set.Pairwise (↑s) (coprime on g) ∧ ∀ (b : ι), b ∈ ↑s → a ≠ b → (coprime on g) a b
⊢ coprime (g a) (∏ x in s, g x)
[PROOFSTEP]
exact Nat.coprime_prod_right fun i hi => hs.2 _ hi (hi.ne_of_not_mem has).symm
[GOAL]
R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : IsMultiplicative f
⊢ ↑↑f 1 = 1
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : IsMultiplicative f
m n : ℕ
cop : coprime m n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
[PROOFSTEP]
simp [h.2 cop]
[GOAL]
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : IsMultiplicative f
⊢ ↑↑f 1 = 1
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : IsMultiplicative f
m n : ℕ
cop : coprime m n
⊢ ↑↑f (m * n) = ↑↑f m * ↑↑f n
[PROOFSTEP]
simp [h.2 cop]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ↑(f * g) 1 = 1
[PROOFSTEP]
simp [hf.1, hg.1]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ∀ {m n : ℕ}, coprime m n → ↑(f * g) (m * n) = ↑(f * g) m * ↑(f * g) n
[PROOFSTEP]
simp only [mul_apply]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ∀ {m n : ℕ},
    coprime m n →
      ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
        (∑ x in divisorsAntidiagonal m, ↑f x.fst * ↑g x.snd) * ∑ x in divisorsAntidiagonal n, ↑f x.fst * ↑g x.snd
[PROOFSTEP]
intro m n cop
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
    (∑ x in divisorsAntidiagonal m, ↑f x.fst * ↑g x.snd) * ∑ x in divisorsAntidiagonal n, ↑f x.fst * ↑g x.snd
[PROOFSTEP]
rw [sum_mul_sum]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd =
    ∑ p in divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n, ↑f p.fst.fst * ↑g p.fst.snd * (↑f p.snd.fst * ↑g p.snd.snd)
[PROOFSTEP]
symm
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∑ p in divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n, ↑f p.fst.fst * ↑g p.fst.snd * (↑f p.snd.fst * ↑g p.snd.snd) =
    ∑ x in divisorsAntidiagonal (m * n), ↑f x.fst * ↑g x.snd
[PROOFSTEP]
apply sum_bij fun (x : (ℕ × ℕ) × ℕ × ℕ) _h => (x.1.1 * x.2.1, x.1.2 * x.2.2)
[GOAL]
case hi
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    a ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd) ∈ divisorsAntidiagonal (m * n)
[PROOFSTEP]
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
[GOAL]
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (m * n)
[PROOFSTEP]
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h 
[GOAL]
case hi.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (m * n)
[PROOFSTEP]
rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
[GOAL]
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) ∈
    divisorsAntidiagonal (a1 * a2 * (b1 * b2))
[PROOFSTEP]
simp only [mem_divisorsAntidiagonal, Nat.mul_eq_zero, Ne.def]
[GOAL]
case hi.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2) ∧ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
[PROOFSTEP]
constructor
[GOAL]
case hi.mk.mk.mk.intro.intro.intro.left
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ a1 * b1 * (a2 * b2) = a1 * a2 * (b1 * b2)
[PROOFSTEP]
ring
[GOAL]
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
[PROOFSTEP]
rw [Nat.mul_eq_zero] at *
[GOAL]
case hi.mk.mk.mk.intro.intro.intro.right
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬(a1 = 0 ∨ a2 = 0)
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬(b1 = 0 ∨ b2 = 0)
⊢ ¬((a1 = 0 ∨ a2 = 0) ∨ b1 = 0 ∨ b2 = 0)
[PROOFSTEP]
apply not_or_of_not ha hb
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a : (ℕ × ℕ) × ℕ × ℕ),
    a ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      ↑f a.fst.fst * ↑g a.fst.snd * (↑f a.snd.fst * ↑g a.snd.snd) =
        ↑f (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd).fst * ↑g (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd).snd
[PROOFSTEP]
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ h
[GOAL]
case h.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
[PROOFSTEP]
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h 
[GOAL]
case h.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 : ℕ
h : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
[PROOFSTEP]
rcases h with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
[GOAL]
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f ((a1, a2), b1, b2).fst.fst * ↑g ((a1, a2), b1, b2).fst.snd *
      (↑f ((a1, a2), b1, b2).snd.fst * ↑g ((a1, a2), b1, b2).snd.snd) =
    ↑f
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).fst *
      ↑g
        (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst,
            ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd).snd
[PROOFSTEP]
dsimp only
[GOAL]
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f a1 * ↑g a2 * (↑f b1 * ↑g b2) = ↑f (a1 * b1) * ↑g (a2 * b2)
[PROOFSTEP]
rw [hf.map_mul_of_coprime cop.coprime_mul_right.coprime_mul_right_right,
  hg.map_mul_of_coprime cop.coprime_mul_left.coprime_mul_left_right]
[GOAL]
case h.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ↑f a1 * ↑g a2 * (↑f b1 * ↑g b2) = ↑f a1 * ↑f b1 * (↑g a2 * ↑g b2)
[PROOFSTEP]
ring
[GOAL]
case i_inj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (a₁ a₂ : (ℕ × ℕ) × ℕ × ℕ),
    a₁ ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
      a₂ ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n →
        (a₁.fst.fst * a₁.snd.fst, a₁.fst.snd * a₁.snd.snd) = (a₂.fst.fst * a₂.snd.fst, a₂.fst.snd * a₂.snd.snd) →
          a₁ = a₂
[PROOFSTEP]
rintro ⟨⟨a1, a2⟩, ⟨b1, b2⟩⟩ ⟨⟨c1, c2⟩, ⟨d1, d2⟩⟩ hab hcd h
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
hab : ((a1, a2), b1, b2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
[PROOFSTEP]
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at hab 
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal m ×ˢ divisorsAntidiagonal n
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
hab : (a1 * a2 = m ∧ ¬m = 0) ∧ b1 * b2 = n ∧ ¬n = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
[PROOFSTEP]
rcases hab with ⟨⟨rfl, ha⟩, ⟨rfl, hb⟩⟩
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hcd : ((c1, c2), d1, d2) ∈ divisorsAntidiagonal (a1 * a2) ×ˢ divisorsAntidiagonal (b1 * b2)
hb : ¬b1 * b2 = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
[PROOFSTEP]
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at hcd 
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
h :
  (((a1, a2), b1, b2).fst.fst * ((a1, a2), b1, b2).snd.fst, ((a1, a2), b1, b2).fst.snd * ((a1, a2), b1, b2).snd.snd) =
    (((c1, c2), d1, d2).fst.fst * ((c1, c2), d1, d2).snd.fst, ((c1, c2), d1, d2).fst.snd * ((c1, c2), d1, d2).snd.snd)
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
[PROOFSTEP]
simp only [Prod.mk.inj_iff] at h 
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2) = ((c1, c2), d1, d2)
[PROOFSTEP]
ext
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2).fst.fst = ((c1, c2), d1, d2).fst.fst
[PROOFSTEP]
dsimp only
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2).fst.snd = ((c1, c2), d1, d2).fst.snd
[PROOFSTEP]
dsimp only
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2).snd.fst = ((c1, c2), d1, d2).snd.fst
[PROOFSTEP]
dsimp only
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ ((a1, a2), b1, b2).snd.snd = ((c1, c2), d1, d2).snd.snd
[PROOFSTEP]
dsimp only
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a1 = c1
[PROOFSTEP]
trans Nat.gcd (a1 * a2) (a1 * b1)
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a1 = gcd (a1 * a2) (a1 * b1)
[PROOFSTEP]
rw [Nat.gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a1 * b1) = c1
[PROOFSTEP]
rw [← hcd.1.1, ← hcd.2.1] at cop 
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a1 * b1) = c1
[PROOFSTEP]
rw [← hcd.1.1, h.1, Nat.gcd_mul_left, cop.coprime_mul_left.coprime_mul_right_right.gcd_eq_one, mul_one]
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₁.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a2 = c2
[PROOFSTEP]
trans Nat.gcd (a1 * a2) (a2 * b2)
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ a2 = gcd (a1 * a2) (a2 * b2)
[PROOFSTEP]
rw [mul_comm, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a2 * b2) = c2
[PROOFSTEP]
rw [← hcd.1.1, ← hcd.2.1] at cop 
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (a1 * a2) (a2 * b2) = c2
[PROOFSTEP]
rw [← hcd.1.1, h.2, mul_comm, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.gcd_eq_one, mul_one]
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₁
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = d1
[PROOFSTEP]
trans Nat.gcd (b1 * b2) (a1 * b1)
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b1 = gcd (b1 * b2) (a1 * b1)
[PROOFSTEP]
rw [mul_comm, Nat.gcd_mul_right, cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one, one_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a1 * b1) = d1
[PROOFSTEP]
rw [← hcd.1.1, ← hcd.2.1] at cop 
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a1 * b1) = d1
[PROOFSTEP]
rw [← hcd.2.1, h.1, mul_comm c1 d1, Nat.gcd_mul_left, cop.coprime_mul_right.coprime_mul_left_right.symm.gcd_eq_one,
  mul_one]
[GOAL]
case i_inj.mk.mk.mk.mk.mk.mk.intro.intro.intro.h₂.h₂
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b2 = d2
[PROOFSTEP]
trans Nat.gcd (b1 * b2) (a2 * b2)
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ b2 = gcd (b1 * b2) (a2 * b2)
[PROOFSTEP]
rw [Nat.gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (a1 * a2) (b1 * b2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a2 * b2) = d2
[PROOFSTEP]
rw [← hcd.1.1, ← hcd.2.1] at cop 
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
a1 a2 b1 b2 c1 c2 d1 d2 : ℕ
ha : ¬a1 * a2 = 0
cop : coprime (c1 * c2) (d1 * d2)
hb : ¬b1 * b2 = 0
hcd : (c1 * c2 = a1 * a2 ∧ ¬a1 * a2 = 0) ∧ d1 * d2 = b1 * b2 ∧ ¬b1 * b2 = 0
h : a1 * b1 = c1 * d1 ∧ a2 * b2 = c2 * d2
⊢ gcd (b1 * b2) (a2 * b2) = d2
[PROOFSTEP]
rw [← hcd.2.1, h.2, Nat.gcd_mul_right, cop.coprime_mul_left.coprime_mul_right_right.symm.gcd_eq_one, one_mul]
[GOAL]
case i_surj
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ∀ (b : ℕ × ℕ), b ∈ divisorsAntidiagonal (m * n) → ∃ a ha, b = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
[PROOFSTEP]
rintro ⟨b1, b2⟩ h
[GOAL]
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : (b1, b2) ∈ divisorsAntidiagonal (m * n)
⊢ ∃ a ha, (b1, b2) = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
[PROOFSTEP]
simp only [mem_divisorsAntidiagonal, Ne.def, mem_product] at h 
[GOAL]
case i_surj.mk
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ∃ a ha, (b1, b2) = (a.fst.fst * a.snd.fst, a.fst.snd * a.snd.snd)
[PROOFSTEP]
use((b1.gcd m, b2.gcd m), (b1.gcd n, b2.gcd n))
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ∃ ha,
    (b1, b2) =
      (((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).fst.fst * ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).snd.fst,
        ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).fst.snd * ((gcd b1 m, gcd b2 m), gcd b1 n, gcd b2 n).snd.snd)
[PROOFSTEP]
simp only [exists_prop, Prod.mk.inj_iff, Ne.def, mem_product, mem_divisorsAntidiagonal]
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ((gcd b1 m * gcd b2 m = m ∧ ¬m = 0) ∧ gcd b1 n * gcd b2 n = n ∧ ¬n = 0) ∧
    b1 = gcd b1 m * gcd b1 n ∧ b2 = gcd b2 m * gcd b2 n
[PROOFSTEP]
rw [← cop.gcd_mul _, ← cop.gcd_mul _, ← h.1, Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop h.1,
  Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul cop.symm _]
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ b1 = gcd b1 (b1 * b2) ∧ b2 = gcd b2 (b1 * b2)
[PROOFSTEP]
rw [Nat.mul_eq_zero, not_or] at h 
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m = 0 ∧ ¬n = 0
⊢ ((m = m ∧ ¬m = 0) ∧ n = n ∧ ¬n = 0) ∧ b1 = gcd b1 (b1 * b2) ∧ b2 = gcd b2 (b1 * b2)
[PROOFSTEP]
simp [h.2.1, h.2.2]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
b1 b2 : ℕ
h : b1 * b2 = m * n ∧ ¬m * n = 0
⊢ b1 * b2 = n * m
[PROOFSTEP]
rw [mul_comm n m, h.1]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ↑(ArithmeticFunction.pmul f g) 1 = 1
[PROOFSTEP]
simp [hf, hg]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑(ArithmeticFunction.pmul f g) (m * n) = ↑(ArithmeticFunction.pmul f g) m * ↑(ArithmeticFunction.pmul f g) n
[PROOFSTEP]
simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑f m * ↑f n * (↑g m * ↑g n) = ↑f m * ↑g m * (↑f n * ↑g n)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
⊢ ↑(ArithmeticFunction.pdiv f g) 1 = 1
[PROOFSTEP]
simp [hf, hg]
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑(ArithmeticFunction.pdiv f g) (m * n) = ↑(ArithmeticFunction.pdiv f g) m * ↑(ArithmeticFunction.pdiv f g) n
[PROOFSTEP]
simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop, div_eq_mul_inv, mul_inv]
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : IsMultiplicative f
hg : IsMultiplicative g
m n : ℕ
cop : coprime m n
⊢ ↑f m * ↑f n * ((↑g m)⁻¹ * (↑g n)⁻¹) = ↑f m * (↑g m)⁻¹ * (↑f n * (↑g n)⁻¹)
[PROOFSTEP]
apply mul_mul_mul_comm
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
⊢ IsMultiplicative f ↔ ↑f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
[PROOFSTEP]
refine' and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => _⟩)
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
⊢ ↑f (m * n) = ↑f m * ↑f n
[PROOFSTEP]
rcases eq_or_ne m 0 with (rfl | hm)
[GOAL]
case inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h : 0 ≠ 0 → n ≠ 0 → coprime 0 n → ↑f (0 * n) = ↑f 0 * ↑f n
hmn : coprime 0 n
⊢ ↑f (0 * n) = ↑f 0 * ↑f n
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
hm : m ≠ 0
⊢ ↑f (m * n) = ↑f m * ↑f n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inr.inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h : m ≠ 0 → 0 ≠ 0 → coprime m 0 → ↑f (m * 0) = ↑f m * ↑f 0
hmn : coprime m 0
⊢ ↑f (m * 0) = ↑f m * ↑f 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → coprime m n → ↑f (m * n) = ↑f m * ↑f n
hmn : coprime m n
hm : m ≠ 0
hn : n ≠ 0
⊢ ↑f (m * n) = ↑f m * ↑f n
[PROOFSTEP]
exact h hm hn hmn
[GOAL]
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ f = g ↔ ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ f = g → ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
[PROOFSTEP]
intro h p i _
[GOAL]
case mp
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : f = g
p i : ℕ
a✝ : Prime p
⊢ ↑f (p ^ i) = ↑g (p ^ i)
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
⊢ (∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)) → f = g
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
⊢ f = g
[PROOFSTEP]
ext n
[GOAL]
case mpr.h
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
⊢ ↑f n = ↑g n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : n = 0
⊢ ↑f n = ↑g n
[PROOFSTEP]
rw [hn, ArithmeticFunction.map_zero, ArithmeticFunction.map_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ↑f n = ↑g n
[PROOFSTEP]
rw [multiplicative_factorization f hf hn, multiplicative_factorization g hg hn]
[GOAL]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => ↑f (p ^ k)) = Finsupp.prod (factorization n) fun p k => ↑g (p ^ k)
[PROOFSTEP]
refine' Finset.prod_congr rfl _
[GOAL]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ∀ (x : ℕ),
    x ∈ (factorization n).support →
      (fun p k => ↑f (p ^ k)) x (↑(factorization n) x) = (fun p k => ↑g (p ^ k)) x (↑(factorization n) x)
[PROOFSTEP]
simp only [support_factorization, List.mem_toFinset]
[GOAL]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ factors n → ↑f (x ^ ↑(factorization n) x) = ↑g (x ^ ↑(factorization n) x)
[PROOFSTEP]
intro p hp
[GOAL]
case neg
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ArithmeticFunction R
hf : IsMultiplicative f
g : ArithmeticFunction R
hg : IsMultiplicative g
h : ∀ (p i : ℕ), Prime p → ↑f (p ^ i) = ↑g (p ^ i)
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ factors n
⊢ ↑f (p ^ ↑(factorization n) p) = ↑g (p ^ ↑(factorization n) p)
[PROOFSTEP]
exact h p _ (Nat.prime_of_mem_factors hp)
[GOAL]
R : Type u_1
k n : ℕ
⊢ ↑(pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k
[PROOFSTEP]
cases k
[GOAL]
case zero
R : Type u_1
n : ℕ
⊢ ↑(pow Nat.zero) n = if Nat.zero = 0 ∧ n = 0 then 0 else n ^ Nat.zero
[PROOFSTEP]
simp [pow]
[GOAL]
case succ
R : Type u_1
n n✝ : ℕ
⊢ ↑(pow (succ n✝)) n = if succ n✝ = 0 ∧ n = 0 then 0 else n ^ succ n✝
[PROOFSTEP]
rename_i k
[GOAL]
case succ
R : Type u_1
n k : ℕ
⊢ ↑(pow (succ k)) n = if succ k = 0 ∧ n = 0 then 0 else n ^ succ k
[PROOFSTEP]
simp [pow, (ne_of_lt (Nat.succ_pos k)).symm]
[GOAL]
R : Type u_1
⊢ pow 0 = ζ
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
n : ℕ
⊢ ↑(pow 0) n = ↑ζ n
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
k : ℕ
⊢ (fun n => ∑ d in divisors n, d ^ k) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n : ℕ
⊢ ↑(σ 1) n = ∑ d in divisors n, d
[PROOFSTEP]
simp [sigma_apply]
[GOAL]
R : Type u_1
n : ℕ
⊢ ↑(σ 0) n = card (divisors n)
[PROOFSTEP]
simp [sigma_apply]
[GOAL]
R : Type u_1
p i : ℕ
hp : Prime p
⊢ ↑(σ 0) (p ^ i) = i + 1
[PROOFSTEP]
rw [sigma_zero_apply, divisors_prime_pow hp, card_map, card_range]
[GOAL]
R : Type u_1
k : ℕ
⊢ ζ * pow k = σ k
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
k x✝ : ℕ
⊢ ↑(ζ * pow k) x✝ = ↑(σ k) x✝
[PROOFSTEP]
rw [sigma, zeta_mul_apply]
[GOAL]
case h
R : Type u_1
k x✝ : ℕ
⊢ ∑ i in divisors x✝, ↑(pow k) i =
    ↑{ toFun := fun n => ∑ d in divisors n, d ^ k, map_zero' := (_ : ∑ d in divisors 0, d ^ k = 0) } x✝
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h
R : Type u_1
k x✝ : ℕ
⊢ ∀ (x : ℕ), x ∈ divisors x✝ → ↑(pow k) x = x ^ k
[PROOFSTEP]
intro x hx
[GOAL]
case h
R : Type u_1
k x✝ x : ℕ
hx : x ∈ divisors x✝
⊢ ↑(pow k) x = x ^ k
[PROOFSTEP]
rw [pow_apply, if_neg (not_and_of_not_right _ _)]
[GOAL]
R : Type u_1
k x✝ x : ℕ
hx : x ∈ divisors x✝
⊢ ¬x = 0
[PROOFSTEP]
contrapose! hx
[GOAL]
R : Type u_1
k x✝ x : ℕ
hx : x = 0
⊢ ¬x ∈ divisors x✝
[PROOFSTEP]
simp [hx]
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
⊢ ↑1 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑1 (m * n) = ↑1 m * ↑1 n
[PROOFSTEP]
intro m n hm _hn hmn
[GOAL]
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
⊢ ↑1 (m * n) = ↑1 m * ↑1 n
[PROOFSTEP]
rcases eq_or_ne m 1 with (rfl | hm')
[GOAL]
case inl
R : Type u_1
inst✝ : MonoidWithZero R
n : ℕ
_hn : n ≠ 0
hm : 1 ≠ 0
hmn : coprime 1 n
⊢ ↑1 (1 * n) = ↑1 1 * ↑1 n
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ ↑1 (m * n) = ↑1 m * ↑1 n
[PROOFSTEP]
rw [one_apply_ne, one_apply_ne hm', zero_mul]
[GOAL]
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ m * n ≠ 1
[PROOFSTEP]
rw [Ne.def, mul_eq_one, not_and_or]
[GOAL]
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : coprime m n
hm' : m ≠ 1
⊢ ¬m = 1 ∨ ¬n = 1
[PROOFSTEP]
exact Or.inl hm'
[GOAL]
R : Type u_1
⊢ ↑ζ 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑ζ (m * n) = ↑ζ m * ↑ζ n
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
⊢ IsMultiplicative (ArithmeticFunction.ppow f k)
[PROOFSTEP]
induction' k with k hi
[GOAL]
case zero
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
⊢ IsMultiplicative (ArithmeticFunction.ppow f Nat.zero)
[PROOFSTEP]
exact isMultiplicative_zeta.nat_cast
[GOAL]
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
hi : IsMultiplicative (ArithmeticFunction.ppow f k)
⊢ IsMultiplicative (ArithmeticFunction.ppow f (succ k))
[PROOFSTEP]
rw [ppow_succ]
[GOAL]
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative f
k : ℕ
hi : IsMultiplicative (ArithmeticFunction.ppow f k)
⊢ IsMultiplicative (ArithmeticFunction.pmul f (ArithmeticFunction.ppow f k))
[PROOFSTEP]
apply hf.pmul hi
[GOAL]
R : Type u_1
k : ℕ
⊢ IsMultiplicative (σ k)
[PROOFSTEP]
rw [← zeta_mul_pow_eq_sigma]
[GOAL]
R : Type u_1
k : ℕ
⊢ IsMultiplicative (ζ * pow k)
[PROOFSTEP]
apply isMultiplicative_zeta.mul isMultiplicative_pow
[GOAL]
R : Type u_1
⊢ (fun n => List.length (factors n)) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
⊢ ↑Ω 1 = 0
[PROOFSTEP]
simp [cardFactors]
[GOAL]
R : Type u_1
n : ℕ
⊢ ↑Ω n = 1 ↔ Prime n
[PROOFSTEP]
refine' ⟨fun h => _, fun h => List.length_eq_one.2 ⟨n, factors_prime h⟩⟩
[GOAL]
R : Type u_1
n : ℕ
h : ↑Ω n = 1
⊢ Prime n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
h : ↑Ω Nat.zero = 1
⊢ Prime Nat.zero
[PROOFSTEP]
contrapose! h
[GOAL]
case zero
R : Type u_1
h : ¬Prime Nat.zero
⊢ ↑Ω Nat.zero ≠ 1
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
n : ℕ
h : ↑Ω (succ n) = 1
⊢ Prime (succ n)
[PROOFSTEP]
rcases List.length_eq_one.1 h with ⟨x, hx⟩
[GOAL]
case succ.intro
R : Type u_1
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ Prime (succ n)
[PROOFSTEP]
rw [← prod_factors n.succ_ne_zero, hx, List.prod_singleton]
[GOAL]
case succ.intro
R : Type u_1
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ Prime x
[PROOFSTEP]
apply prime_of_mem_factors
[GOAL]
case succ.intro.h
R : Type u_1
n : ℕ
h : ↑Ω (succ n) = 1
x : ℕ
hx : factors (succ n) = [x]
⊢ x ∈ factors ?succ.intro.n
case succ.intro.n R : Type u_1 n : ℕ h : ↑Ω (succ n) = 1 x : ℕ hx : factors (succ n) = [x] ⊢ ℕ
[PROOFSTEP]
rw [hx, List.mem_singleton]
[GOAL]
R : Type u_1
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ ↑Ω (m * n) = ↑Ω m + ↑Ω n
[PROOFSTEP]
rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
  UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq, Multiset.card_add, Multiset.coe_card,
  Multiset.coe_card]
[GOAL]
R : Type u_1
s : Multiset ℕ
h0 : Multiset.prod s ≠ 0
⊢ ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)
[PROOFSTEP]
revert h0
[GOAL]
R : Type u_1
s : Multiset ℕ
⊢ Multiset.prod s ≠ 0 → ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)
[PROOFSTEP]
refine s.induction_on ?_ ?_
[GOAL]
case refine_1
R : Type u_1
s : Multiset ℕ
⊢ Multiset.prod 0 ≠ 0 → ↑Ω (Multiset.prod 0) = Multiset.sum (Multiset.map (↑Ω) 0)
[PROOFSTEP]
simp
[GOAL]
case refine_2
R : Type u_1
s : Multiset ℕ
⊢ ∀ ⦃a : ℕ⦄ {s : Multiset ℕ},
    (Multiset.prod s ≠ 0 → ↑Ω (Multiset.prod s) = Multiset.sum (Multiset.map (↑Ω) s)) →
      Multiset.prod (a ::ₘ s) ≠ 0 → ↑Ω (Multiset.prod (a ::ₘ s)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ s))
[PROOFSTEP]
intro a t h h0
[GOAL]
case refine_2
R : Type u_1
s : Multiset ℕ
a : ℕ
t : Multiset ℕ
h : Multiset.prod t ≠ 0 → ↑Ω (Multiset.prod t) = Multiset.sum (Multiset.map (↑Ω) t)
h0 : Multiset.prod (a ::ₘ t) ≠ 0
⊢ ↑Ω (Multiset.prod (a ::ₘ t)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ t))
[PROOFSTEP]
rw [Multiset.prod_cons, mul_ne_zero_iff] at h0 
[GOAL]
case refine_2
R : Type u_1
s : Multiset ℕ
a : ℕ
t : Multiset ℕ
h : Multiset.prod t ≠ 0 → ↑Ω (Multiset.prod t) = Multiset.sum (Multiset.map (↑Ω) t)
h0 : a ≠ 0 ∧ Multiset.prod t ≠ 0
⊢ ↑Ω (Multiset.prod (a ::ₘ t)) = Multiset.sum (Multiset.map (↑Ω) (a ::ₘ t))
[PROOFSTEP]
simp [h0, cardFactors_mul, h]
[GOAL]
R : Type u_1
p k : ℕ
hp : Prime p
⊢ ↑Ω (p ^ k) = k
[PROOFSTEP]
rw [cardFactors_apply, hp.factors_pow, List.length_replicate]
[GOAL]
R : Type u_1
⊢ (fun n => List.length (List.dedup (factors n))) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
⊢ ↑ω 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
⊢ ↑ω 1 = 0
[PROOFSTEP]
simp [cardDistinctFactors]
[GOAL]
R : Type u_1
n : ℕ
h0 : n ≠ 0
⊢ ↑ω n = ↑Ω n ↔ Squarefree n
[PROOFSTEP]
rw [squarefree_iff_nodup_factors h0, cardDistinctFactors_apply]
[GOAL]
R : Type u_1
n : ℕ
h0 : n ≠ 0
⊢ List.length (List.dedup (factors n)) = ↑Ω n ↔ List.Nodup (factors n)
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
n : ℕ
h0 : n ≠ 0
⊢ List.length (List.dedup (factors n)) = ↑Ω n → List.Nodup (factors n)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
n : ℕ
h0 : n ≠ 0
⊢ List.Nodup (factors n) → List.length (List.dedup (factors n)) = ↑Ω n
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
n : ℕ
h0 : n ≠ 0
h : List.length (List.dedup (factors n)) = ↑Ω n
⊢ List.Nodup (factors n)
[PROOFSTEP]
rw [← n.factors.dedup_sublist.eq_of_length h]
[GOAL]
case mp
R : Type u_1
n : ℕ
h0 : n ≠ 0
h : List.length (List.dedup (factors n)) = ↑Ω n
⊢ List.Nodup (List.dedup (factors n))
[PROOFSTEP]
apply List.nodup_dedup
[GOAL]
case mpr
R : Type u_1
n : ℕ
h0 : n ≠ 0
h : List.Nodup (factors n)
⊢ List.length (List.dedup (factors n)) = ↑Ω n
[PROOFSTEP]
rw [h.dedup]
[GOAL]
case mpr
R : Type u_1
n : ℕ
h0 : n ≠ 0
h : List.Nodup (factors n)
⊢ List.length (factors n) = ↑Ω n
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ ↑ω (p ^ k) = 1
[PROOFSTEP]
rw [cardDistinctFactors_apply, hp.factors_pow, List.replicate_dedup hk, List.length_singleton]
[GOAL]
R : Type u_1
p : ℕ
hp : Prime p
⊢ ↑ω p = 1
[PROOFSTEP]
rw [← pow_one p, cardDistinctFactors_apply_prime_pow hp one_ne_zero]
[GOAL]
R : Type u_1
⊢ (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
⊢ ↑μ 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n : ℕ
⊢ ↑μ n ≠ 0 ↔ Squarefree n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
n : ℕ
⊢ ↑μ n ≠ 0 → Squarefree n
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
n : ℕ
⊢ Squarefree n → ↑μ n ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
n : ℕ
h : ↑μ n ≠ 0
⊢ Squarefree n
[PROOFSTEP]
contrapose! h
[GOAL]
case mp
R : Type u_1
n : ℕ
h : ¬Squarefree n
⊢ ↑μ n = 0
[PROOFSTEP]
simp [h]
[GOAL]
case mpr
R : Type u_1
n : ℕ
h : Squarefree n
⊢ ↑μ n ≠ 0
[PROOFSTEP]
simp [h, pow_ne_zero]
[GOAL]
R : Type u_1
n : ℕ
⊢ ↑μ n ≠ 0 ↔ ↑μ n = 1 ∨ ↑μ n = -1
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
n : ℕ
⊢ ↑μ n ≠ 0 → ↑μ n = 1 ∨ ↑μ n = -1
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
n : ℕ
⊢ ↑μ n = 1 ∨ ↑μ n = -1 → ↑μ n ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
n : ℕ
h : ↑μ n ≠ 0
⊢ ↑μ n = 1 ∨ ↑μ n = -1
[PROOFSTEP]
rw [moebius_ne_zero_iff_squarefree] at h 
[GOAL]
case mp
R : Type u_1
n : ℕ
h : Squarefree n
⊢ ↑μ n = 1 ∨ ↑μ n = -1
[PROOFSTEP]
rw [moebius_apply_of_squarefree h]
[GOAL]
case mp
R : Type u_1
n : ℕ
h : Squarefree n
⊢ (-1) ^ ↑Ω n = 1 ∨ (-1) ^ ↑Ω n = -1
[PROOFSTEP]
apply neg_one_pow_eq_or
[GOAL]
case mpr
R : Type u_1
n : ℕ
h : ↑μ n = 1 ∨ ↑μ n = -1
⊢ ↑μ n ≠ 0
[PROOFSTEP]
rcases h with (h | h)
[GOAL]
case mpr.inl
R : Type u_1
n : ℕ
h : ↑μ n = 1
⊢ ↑μ n ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case mpr.inr
R : Type u_1
n : ℕ
h : ↑μ n = -1
⊢ ↑μ n ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
p : ℕ
hp : Prime p
⊢ ↑μ p = -1
[PROOFSTEP]
rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]
[GOAL]
R : Type u_1
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ ↑μ (p ^ k) = if k = 1 then -1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : k = 1
⊢ ↑μ (p ^ k) = -1
[PROOFSTEP]
rw [h, pow_one, moebius_apply_prime hp]
[GOAL]
case neg
R : Type u_1
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ↑μ (p ^ k) = 0
[PROOFSTEP]
rw [moebius_eq_zero_of_not_squarefree]
[GOAL]
case neg
R : Type u_1
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)
[PROOFSTEP]
rw [squarefree_pow_iff hp.ne_one hk, not_and_or]
[GOAL]
case neg
R : Type u_1
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1
[PROOFSTEP]
exact Or.inr h
[GOAL]
R : Type u_1
n : ℕ
hn : IsPrimePow n
hn' : ¬Prime n
⊢ ↑μ n = 0
[PROOFSTEP]
obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn
[GOAL]
case intro.intro.intro.intro
R : Type u_1
p k : ℕ
hp : Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Prime (p ^ k)
⊢ ↑μ (p ^ k) = 0
[PROOFSTEP]
rw [moebius_apply_prime_pow hp hk.ne', if_neg]
[GOAL]
case intro.intro.intro.intro.hnc
R : Type u_1
p k : ℕ
hp : Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Prime (p ^ k)
⊢ ¬k = 1
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro.hnc
R : Type u_1
p : ℕ
hp : Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Prime (p ^ 1)
⊢ False
[PROOFSTEP]
exact hn' (by simpa)
[GOAL]
R : Type u_1
p : ℕ
hp : Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Prime (p ^ 1)
⊢ Prime (p ^ 1)
[PROOFSTEP]
simpa
[GOAL]
R : Type u_1
⊢ IsMultiplicative μ
[PROOFSTEP]
rw [IsMultiplicative.iff_ne_zero]
[GOAL]
R : Type u_1
⊢ ↑μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑μ (m * n) = ↑μ m * ↑μ n
[PROOFSTEP]
refine'
  ⟨by simp, fun {n m} hn hm hnm => _⟩
    -- porting note: the rest of this proof was a single `simp only` with all the lemmas thrown in
      -- followed by the last `rw`.
[GOAL]
R : Type u_1
⊢ ↑μ 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ↑μ (n * m) = ↑μ n * ↑μ m
[PROOFSTEP]
simp only [moebius, ZeroHom.coe_mk]
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
          map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
      (n * m) =
    ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
            map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
        n *
      ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
            map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
        m
[PROOFSTEP]
dsimp only [coe_mk, ZeroHom.toFun_eq_coe, Eq.ndrec, ZeroHom.coe_mk]
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree (n * m) then (-1) ^ ↑Ω (n * m) else 0) =
    (if Squarefree n then (-1) ^ ↑Ω n else 0) * if Squarefree m then (-1) ^ ↑Ω m else 0
[PROOFSTEP]
simp only [IsUnit.mul_iff, Nat.isUnit_iff, squarefree_mul hnm, ite_and, mul_ite, ite_mul, zero_mul, mul_zero]
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ ↑Ω (n * m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
[PROOFSTEP]
rw [cardFactors_mul hn hm]
  -- porting note: `simp` does not seem to use this lemma.
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
[PROOFSTEP]
simp only [moebius, ZeroHom.coe_mk, squarefree_mul hnm, ite_and, cardFactors_mul hn hm]
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
[PROOFSTEP]
rw [pow_add, ite_mul_zero_left, ite_mul_zero_right]
[GOAL]
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ((if Squarefree m then (-1) ^ ↑Ω n else 0) * if Squarefree n then (-1) ^ ↑Ω m else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
h✝¹ : Squarefree m
h✝ : Squarefree n
⊢ (-1) ^ ↑Ω n * (-1) ^ ↑Ω m = (-1) ^ ↑Ω n * (-1) ^ ↑Ω m
[PROOFSTEP]
simp
  -- porting note: added
[GOAL]
case neg
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
h✝¹ : Squarefree m
h✝ : ¬Squarefree n
⊢ (-1) ^ ↑Ω n * 0 = 0
[PROOFSTEP]
simp
  -- porting note: added
[GOAL]
case pos
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
h✝¹ : ¬Squarefree m
h✝ : Squarefree n
⊢ 0 * (-1) ^ ↑Ω m = 0
[PROOFSTEP]
simp
  -- porting note: added
[GOAL]
case neg
R : Type u_1
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
h✝¹ : ¬Squarefree m
h✝ : ¬Squarefree n
⊢ 0 * 0 = 0
[PROOFSTEP]
simp
  -- porting note: added
[GOAL]
R : Type u_1
⊢ μ * ↑ζ = 1
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
n : ℕ
⊢ ↑(μ * ↑ζ) n = ↑1 n
[PROOFSTEP]
refine' recOnPosPrimePosCoprime _ _ _ _ n
[GOAL]
case h.refine'_1
R : Type u_1
n : ℕ
⊢ ∀ (p n : ℕ), Prime p → 0 < n → ↑(μ * ↑ζ) (p ^ n) = ↑1 (p ^ n)
[PROOFSTEP]
intro p n hp hn
[GOAL]
case h.refine'_1
R : Type u_1
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ↑(μ * ↑ζ) (p ^ n) = ↑1 (p ^ n)
[PROOFSTEP]
rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ']
[GOAL]
case h.refine'_1
R : Type u_1
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ∑ k in range n, ↑μ (p ^ (k + 1)) + ↑μ (p ^ 0) = ↑1 (p ^ n)
[PROOFSTEP]
simp_rw [pow_zero, moebius_apply_one, moebius_apply_prime_pow hp (Nat.succ_ne_zero _), Nat.succ_inj', sum_ite_eq',
  mem_range, if_pos hn, add_left_neg]
[GOAL]
case h.refine'_1
R : Type u_1
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ 0 = ↑1 (p ^ n)
[PROOFSTEP]
rw [one_apply_ne]
[GOAL]
case h.refine'_1
R : Type u_1
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ p ^ n ≠ 1
[PROOFSTEP]
rw [Ne.def, pow_eq_one_iff]
[GOAL]
case h.refine'_1
R : Type u_1
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ ¬p = 1
[PROOFSTEP]
exact hp.ne_one
[GOAL]
case h.refine'_1
R : Type u_1
n✝ p n : ℕ
hp : Prime p
hn : 0 < n
⊢ n ≠ 0
[PROOFSTEP]
exact hn.ne'
[GOAL]
case h.refine'_2
R : Type u_1
n : ℕ
⊢ ↑(μ * ↑ζ) 0 = ↑1 0
[PROOFSTEP]
rw [ZeroHom.map_zero, ZeroHom.map_zero]
[GOAL]
case h.refine'_3
R : Type u_1
n : ℕ
⊢ ↑(μ * ↑ζ) 1 = ↑1 1
[PROOFSTEP]
simp
[GOAL]
case h.refine'_4
R : Type u_1
n : ℕ
⊢ ∀ (a b : ℕ), 1 < a → 1 < b → coprime a b → ↑(μ * ↑ζ) a = ↑1 a → ↑(μ * ↑ζ) b = ↑1 b → ↑(μ * ↑ζ) (a * b) = ↑1 (a * b)
[PROOFSTEP]
intro a b _ha _hb hab ha' hb'
[GOAL]
case h.refine'_4
R : Type u_1
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : coprime a b
ha' : ↑(μ * ↑ζ) a = ↑1 a
hb' : ↑(μ * ↑ζ) b = ↑1 b
⊢ ↑(μ * ↑ζ) (a * b) = ↑1 (a * b)
[PROOFSTEP]
rw [IsMultiplicative.map_mul_of_coprime _ hab, ha', hb', IsMultiplicative.map_mul_of_coprime isMultiplicative_one hab]
[GOAL]
R : Type u_1
n a b : ℕ
_ha : 1 < a
_hb : 1 < b
hab : coprime a b
ha' : ↑(μ * ↑ζ) a = ↑1 a
hb' : ↑(μ * ↑ζ) b = ↑1 b
⊢ IsMultiplicative (μ * ↑ζ)
[PROOFSTEP]
exact isMultiplicative_moebius.mul isMultiplicative_zeta.nat_cast
[GOAL]
R : Type u_1
⊢ ↑ζ * μ = 1
[PROOFSTEP]
rw [mul_comm, moebius_mul_coe_zeta]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ ↑μ * ↑ζ = 1
[PROOFSTEP]
rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]
[GOAL]
R : Type u_1
inst✝ : Ring R
⊢ ↑ζ * ↑μ = 1
[PROOFSTEP]
rw [← coe_coe, ← intCoe_mul, coe_zeta_mul_moebius, intCoe_one]
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
⊢ (∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
let f' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else f x, if_pos rfl⟩
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
⊢ (∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
let g' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else g x, if_pos rfl⟩
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ (∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
trans (ζ : ArithmeticFunction ℤ) • f' = g'
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ (∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = g n) ↔ ↑ζ • f' = g'
[PROOFSTEP]
rw [ext_iff]
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ (∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = g n) ↔ ∀ (x : ℕ), ↑(↑ζ • f') x = ↑g' x
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ∀ (a : ℕ), a > 0 → ∑ i in divisors a, f i = g a ↔ ↑(↑ζ • f') a = ↑g' a
[PROOFSTEP]
intro n
[GOAL]
case h
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ n > 0 → ∑ i in divisors n, f i = g n ↔ ↑(↑ζ • f') n = ↑g' n
[PROOFSTEP]
cases n with
| zero => simp
| succ n =>
  rw [coe_zeta_smul_apply]
  simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', if_false, ZeroHom.coe_mk]
  simp only [coe_mk, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors hx))]
[GOAL]
case h
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ n > 0 → ∑ i in divisors n, f i = g n ↔ ↑(↑ζ • f') n = ↑g' n
[PROOFSTEP]
cases n with
| zero => simp
| succ n =>
  rw [coe_zeta_smul_apply]
  simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', if_false, ZeroHom.coe_mk]
  simp only [coe_mk, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors hx))]
[GOAL]
case h.zero
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ Nat.zero > 0 → ∑ i in divisors Nat.zero, f i = g Nat.zero ↔ ↑(↑ζ • f') Nat.zero = ↑g' Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case h.zero
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ Nat.zero > 0 → ∑ i in divisors Nat.zero, f i = g Nat.zero ↔ ↑(↑ζ • f') Nat.zero = ↑g' Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ succ n > 0 → ∑ i in divisors (succ n), f i = g (succ n) ↔ ↑(↑ζ • f') (succ n) = ↑g' (succ n)
[PROOFSTEP]

| succ n =>
  rw [coe_zeta_smul_apply]
  simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', if_false, ZeroHom.coe_mk]
  simp only [coe_mk, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors hx))]
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ succ n > 0 → ∑ i in divisors (succ n), f i = g (succ n) ↔ ↑(↑ζ • f') (succ n) = ↑g' (succ n)
[PROOFSTEP]
rw [coe_zeta_smul_apply]
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ succ n > 0 → ∑ i in divisors (succ n), f i = g (succ n) ↔ ∑ i in divisors (succ n), ↑f' i = ↑g' (succ n)
[PROOFSTEP]
simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', if_false, ZeroHom.coe_mk]
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ∑ i in divisors (succ n), f i = g (succ n) ↔
    ∑ x in divisors (succ n),
        ↑{ toFun := fun x => if x = 0 then 0 else f x, map_zero' := (_ : (if 0 = 0 then 0 else f 0) = 0) } x =
      ↑{ toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) } (succ n)
[PROOFSTEP]
simp only [coe_mk, succ_ne_zero, ite_false]
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ∑ i in divisors (succ n), f i = g (succ n) ↔ (∑ x in divisors (succ n), if x = 0 then 0 else f x) = g (succ n)
[PROOFSTEP]
rw [sum_congr rfl fun x hx => ?_]
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n x : ℕ
hx : x ∈ divisors (succ n)
⊢ f x = if x = 0 then 0 else f x
[PROOFSTEP]
rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors hx))]
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ↑ζ • f' = g' ↔ ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
trans μ • g' = f'
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ↑ζ • f' = g' ↔ μ • g' = f'
[PROOFSTEP]
constructor
[GOAL]
case mp
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ↑ζ • f' = g' → μ • g' = f'
[PROOFSTEP]
intro h
[GOAL]
case mpr
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ μ • g' = f' → ↑ζ • f' = g'
[PROOFSTEP]
intro h
[GOAL]
case mp
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
h : ↑ζ • f' = g'
⊢ μ • g' = f'
[PROOFSTEP]
rw [← h, ← mul_smul, moebius_mul_coe_zeta, one_smul]
[GOAL]
case mpr
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
h : μ • g' = f'
⊢ ↑ζ • f' = g'
[PROOFSTEP]
rw [← h, ← mul_smul, coe_zeta_mul_moebius, one_smul]
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ μ • g' = f' ↔ ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
rw [ext_iff]
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ (∀ (x : ℕ), ↑(μ • g') x = ↑f' x) ↔ ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ∀ (a : ℕ), ↑(μ • g') a = ↑f' a ↔ a > 0 → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a
[PROOFSTEP]
intro n
[GOAL]
case h
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ↑(μ • g') n = ↑f' n ↔ n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
cases n with
| zero => simp
|
  succ n =>
  simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', smul_apply, if_false, ZeroHom.coe_mk]
    -- porting note: added following `simp only`
  simp only [Nat.isUnit_iff, coe_mk, ZeroHom.toFun_eq_coe, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)))]
[GOAL]
case h
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ↑(μ • g') n = ↑f' n ↔ n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
cases n with
| zero => simp
|
  succ n =>
  simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', smul_apply, if_false, ZeroHom.coe_mk]
    -- porting note: added following `simp only`
  simp only [Nat.isUnit_iff, coe_mk, ZeroHom.toFun_eq_coe, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)))]
[GOAL]
case h.zero
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ↑(μ • g') Nat.zero = ↑f' Nat.zero ↔
    Nat.zero > 0 → ∑ x in divisorsAntidiagonal Nat.zero, ↑μ x.fst • g x.snd = f Nat.zero
[PROOFSTEP]

| zero => simp
[GOAL]
case h.zero
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
⊢ ↑(μ • g') Nat.zero = ↑f' Nat.zero ↔
    Nat.zero > 0 → ∑ x in divisorsAntidiagonal Nat.zero, ↑μ x.fst • g x.snd = f Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ↑(μ • g') (succ n) = ↑f' (succ n) ↔ succ n > 0 → ∑ x in divisorsAntidiagonal (succ n), ↑μ x.fst • g x.snd = f (succ n)
[PROOFSTEP]

|
  succ n =>
  simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', smul_apply, if_false, ZeroHom.coe_mk]
    -- porting note: added following `simp only`
  simp only [Nat.isUnit_iff, coe_mk, ZeroHom.toFun_eq_coe, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)))]
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ↑(μ • g') (succ n) = ↑f' (succ n) ↔ succ n > 0 → ∑ x in divisorsAntidiagonal (succ n), ↑μ x.fst • g x.snd = f (succ n)
[PROOFSTEP]
simp only [n.succ_ne_zero, forall_prop_of_true, succ_pos', smul_apply, if_false, ZeroHom.coe_mk]
  -- porting note: added following `simp only`
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ ∑ x in divisorsAntidiagonal (succ n),
        ↑μ x.fst •
          ↑{ toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) } x.snd =
      ↑{ toFun := fun x => if x = 0 then 0 else f x, map_zero' := (_ : (if 0 = 0 then 0 else f 0) = 0) } (succ n) ↔
    ∑ x in divisorsAntidiagonal (succ n), ↑μ x.fst • g x.snd = f (succ n)
[PROOFSTEP]
simp only [Nat.isUnit_iff, coe_mk, ZeroHom.toFun_eq_coe, succ_ne_zero, ite_false]
[GOAL]
case h.succ
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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
⊢ (∑ x in divisorsAntidiagonal (succ n), ↑μ x.fst • if x.snd = 0 then 0 else g x.snd) = f (succ n) ↔
    ∑ x in divisorsAntidiagonal (succ n), ↑μ x.fst • g x.snd = f (succ n)
[PROOFSTEP]
rw [sum_congr rfl fun x hx => ?_]
[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' := (_ : (if 0 = 0 then 0 else f 0) = 0) }
g' : ArithmeticFunction R :=
  { toFun := fun x => if x = 0 then 0 else g x, map_zero' := (_ : (if 0 = 0 then 0 else g 0) = 0) }
n : ℕ
x : ℕ × ℕ
hx : x ∈ divisorsAntidiagonal (succ n)
⊢ (↑μ x.fst • if x.snd = 0 then 0 else g x.snd) = ↑μ x.fst • g x.snd
[PROOFSTEP]
rw [if_neg (ne_of_gt (Nat.pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)))]
[GOAL]
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
[PROOFSTEP]
rw [sum_eq_iff_sum_smul_moebius_eq]
[GOAL]
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n) ↔
    ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    a > 0 → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a ↔
      a > 0 → ∑ x in divisorsAntidiagonal a, ↑(↑μ x.fst) * g x.snd = f a
[PROOFSTEP]
refine' fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => _).congr_left
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
a : ℕ
x✝ : a > 0
x : ℕ × ℕ
_hx : x ∈ divisorsAntidiagonal a
⊢ ↑μ x.fst • g x.snd = ↑(↑μ x.fst) * g x.snd
[PROOFSTEP]
rw [zsmul_eq_mul]
[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 in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
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 => _)
[GOAL]
case refine'_1
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 in divisors n, f i = g n ↔
    n > 0 →
      (∏ i in divisors n, if h : 0 < i then Units.mk0 (f i) (_ : f i ≠ 0) else 1) =
        if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1
[PROOFSTEP]
refine' imp_congr_right fun hn => _
[GOAL]
case refine'_2
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 →
      ∏ x in divisorsAntidiagonal n, (if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst =
        if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) ↔
    n > 0 → ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
refine' imp_congr_right fun hn => _
[GOAL]
case refine'_1
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
⊢ ∏ i in divisors n, f i = g n ↔
    (∏ i in divisors n, if h : 0 < i then Units.mk0 (f i) (_ : f i ≠ 0) else 1) =
      if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
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
⊢ ∏ i in divisors n, f i = g n ↔
    (∏ i in divisors n, if h : 0 < i then Units.mk0 (f i) (_ : f i ≠ 0) else 1) =
      if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1
[PROOFSTEP]
rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0, prod_congr rfl _]
[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 : ℕ), x ∈ divisors n → f x = ↑(Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) (_ : f x ≠ 0) else 1)
[PROOFSTEP]
intro x hx
[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 ∈ divisors n
⊢ f x = ↑(Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) (_ : f x ≠ 0) else 1)
[PROOFSTEP]
rw [dif_pos (Nat.pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
[GOAL]
case refine'_2
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 in divisorsAntidiagonal n, (if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst =
      if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) ↔
    ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
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 in divisorsAntidiagonal n, (if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst =
      if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) ↔
    ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0, prod_congr rfl _]
[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 : ℕ × ℕ),
    x ∈ divisorsAntidiagonal n →
      ↑(Units.coeHom R) ((if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst) =
        g x.snd ^ ↑μ x.fst
[PROOFSTEP]
intro x hx
[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 ∈ divisorsAntidiagonal n
⊢ ↑(Units.coeHom R) ((if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst) =
    g x.snd ^ ↑μ x.fst
[PROOFSTEP]
rw [dif_pos (Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal hx)), Units.coeHom_apply,
  Units.val_zpow_eq_zpow_val, Units.val_mk0]
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n) →
    ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
⊢ ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
let G := fun (n : ℕ) => (∑ i in n.divisors, f i)
[GOAL]
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
⊢ ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
intro n hn hnP
[GOAL]
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
suffices ∑ d in n.divisors, μ (n / d) • G d = f n from
  by
  rw [Nat.sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
  intro d hd
  rw [← h d (Nat.pos_of_mem_divisors hd) $ hs d n (Nat.dvd_of_mem_divisors hd) hnP]
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d in divisors n, ↑μ (n / d) • G d = f n
⊢ ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
rw [Nat.sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d in divisors n, ↑μ (n / d) • G d = f n
⊢ ∀ (x : ℕ), x ∈ divisors n → ↑μ (n / x) • g x = ↑μ (n / x) • G x
[PROOFSTEP]
intro d hd
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d in divisors n, ↑μ (n / d) • G d = f n
d : ℕ
hd : d ∈ divisors n
⊢ ↑μ (n / d) • g d = ↑μ (n / d) • G d
[PROOFSTEP]
rw [← h d (Nat.pos_of_mem_divisors hd) $ hs d n (Nat.dvd_of_mem_divisors hd) hnP]
[GOAL]
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ d in divisors n, ↑μ (n / d) • G d = f n
[PROOFSTEP]
rw [← Nat.sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]
[GOAL]
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i in divisorsAntidiagonal n, ↑μ i.fst • G i.snd = f n
[PROOFSTEP]
apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∀ (n : ℕ), n > 0 → ∑ i in divisors n, f i = G n
[PROOFSTEP]
intro _ _
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
G : ℕ → R := fun n => ∑ i in divisors n, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
n✝ : ℕ
a✝ : n✝ > 0
⊢ ∑ i in divisors n✝, f i = G n✝
[PROOFSTEP]
rfl
[GOAL]
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n) →
    ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
⊢ ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
[PROOFSTEP]
let F := fun (n : ℕ) => ∑ x : ℕ × ℕ in n.divisorsAntidiagonal, μ x.fst • g x.snd
[GOAL]
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
⊢ ∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n
[PROOFSTEP]
intro n hn hnP
[GOAL]
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i in divisors n, f i = g n
[PROOFSTEP]
suffices ∑ d in n.divisors, F d = g n from by
  rw [← this, sum_congr rfl]
  intro d hd
  rw [← h d (Nat.pos_of_mem_divisors hd) $ hs d n (Nat.dvd_of_mem_divisors hd) hnP]
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d in divisors n, F d = g n
⊢ ∑ i in divisors n, f i = g n
[PROOFSTEP]
rw [← this, sum_congr rfl]
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d in divisors n, F d = g n
⊢ ∀ (x : ℕ), x ∈ divisors n → f x = F x
[PROOFSTEP]
intro d hd
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
this : ∑ d in divisors n, F d = g n
d : ℕ
hd : d ∈ divisors n
⊢ f d = F d
[PROOFSTEP]
rw [← h d (Nat.pos_of_mem_divisors hd) $ hs d n (Nat.dvd_of_mem_divisors hd) hnP]
[GOAL]
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ d in divisors n, F d = g n
[PROOFSTEP]
apply sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∀ (n : ℕ), n > 0 → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = F n
[PROOFSTEP]
intro _ _
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
F : ℕ → R := fun n => ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd
n : ℕ
hn : n > 0
hnP : n ∈ s
n✝ : ℕ
a✝ : n✝ > 0
⊢ ∑ x in divisorsAntidiagonal n✝, ↑μ x.fst • g x.snd = F n✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : ¬0 ∈ s
⊢ (∀ (n : ℕ), n ∈ s → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
have : ∀ P : ℕ → Prop, ((∀ n ∈ s, P n) ↔ (∀ n > 0, n ∈ s → P n)) := fun P ↦
  by
  refine' forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h _ hn⟩)
  contrapose! hs₀
  simpa [nonpos_iff_eq_zero.mp hs₀] using hn
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : ¬0 ∈ s
P : ℕ → Prop
⊢ (∀ (n : ℕ), n ∈ s → P n) ↔ ∀ (n : ℕ), n > 0 → n ∈ s → P n
[PROOFSTEP]
refine' forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h _ hn⟩)
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : ¬0 ∈ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
⊢ n > 0
[PROOFSTEP]
contrapose! hs₀
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
P : ℕ → Prop
n : ℕ
h : n > 0 → n ∈ s → P n
hn : n ∈ s
hs₀ : n ≤ 0
⊢ 0 ∈ s
[PROOFSTEP]
simpa [nonpos_iff_eq_zero.mp hs₀] using hn
[GOAL]
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : ¬0 ∈ s
this : ∀ (P : ℕ → Prop), (∀ (n : ℕ), n ∈ s → P n) ↔ ∀ (n : ℕ), n > 0 → n ∈ s → P n
⊢ (∀ (n : ℕ), n ∈ s → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n
[PROOFSTEP]
simpa only [this] using sum_eq_iff_sum_smul_moebius_eq_on s hs
[GOAL]
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ (n : ℕ), n > 0 → n ∈ s → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
[PROOFSTEP]
rw [sum_eq_iff_sum_smul_moebius_eq_on s hs]
[GOAL]
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n) ↔
    ∀ (n : ℕ), n > 0 → n ∈ s → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ ∀ (a : ℕ),
    a > 0 → a ∈ s → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a ↔
      a > 0 → a ∈ s → ∑ x in divisorsAntidiagonal a, ↑(↑μ x.fst) * g x.snd = f a
[PROOFSTEP]
intro a
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
⊢ a > 0 → a ∈ s → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a ↔
    a > 0 → a ∈ s → ∑ x in divisorsAntidiagonal a, ↑(↑μ x.fst) * g x.snd = f a
[PROOFSTEP]
refine' imp_congr_right _
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
⊢ a > 0 →
    (a ∈ s → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a ↔
      a ∈ s → ∑ x in divisorsAntidiagonal a, ↑(↑μ x.fst) * g x.snd = f a)
[PROOFSTEP]
refine' fun _ => imp_congr_right fun _ => (sum_congr rfl fun x _hx => _).congr_left
[GOAL]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
a : ℕ
x✝¹ : a > 0
x✝ : a ∈ s
x : ℕ × ℕ
_hx : x ∈ divisorsAntidiagonal a
⊢ ↑μ x.fst • g x.snd = ↑(↑μ x.fst) * g x.snd
[PROOFSTEP]
rw [zsmul_eq_mul]
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
⊢ (∀ (n : ℕ), n > 0 → n ∈ s → ∏ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), n > 0 → n ∈ s → ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
refine'
  Iff.trans
    (Iff.trans (forall_congr' fun n => _)
      (@prod_eq_iff_prod_pow_moebius_eq_on 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) s hs))
    (forall_congr' fun n => _)
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
⊢ n > 0 → n ∈ s → ∏ i in divisors n, f i = g n ↔
    n > 0 →
      n ∈ s →
        ∏ i in divisors n, (fun n => if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) i =
          (fun n => if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1) n
[PROOFSTEP]
refine' imp_congr_right fun hn => _
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
⊢ n > 0 →
      n ∈ s →
        ∏ x in divisorsAntidiagonal n,
            (fun n => if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1) x.snd ^ ↑μ x.fst =
          (fun n => if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) n ↔
    n > 0 → n ∈ s → ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
refine' imp_congr_right fun hn => _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → ∏ i in divisors n, f i = g n ↔
    n ∈ s →
      ∏ i in divisors n, (fun n => if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) i =
        (fun n => if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1) n
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s → ∏ i in divisors n, f i = g n ↔
    n ∈ s →
      (∏ i in divisors n, if h : 0 < i then Units.mk0 (f i) (_ : f i ≠ 0) else 1) =
        if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1
[PROOFSTEP]
rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0, prod_congr rfl _]
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ (x : ℕ), x ∈ divisors n → f x = ↑(Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) (_ : f x ≠ 0) else 1)
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ
hx : x ∈ divisors n
⊢ f x = ↑(Units.coeHom R) (if h : 0 < x then Units.mk0 (f x) (_ : f x ≠ 0) else 1)
[PROOFSTEP]
rw [dif_pos (Nat.pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
⊢ n ∈ s →
      ∏ x in divisorsAntidiagonal n,
          (fun n => if h : 0 < n then Units.mk0 (g n) (_ : g n ≠ 0) else 1) x.snd ^ ↑μ x.fst =
        (fun n => if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) n ↔
    n ∈ s → ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (n ∈ s →
      ∏ x in divisorsAntidiagonal n, (if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst =
        if h : 0 < n then Units.mk0 (f n) (_ : f n ≠ 0) else 1) ↔
    n ∈ s → ∏ x in divisorsAntidiagonal n, g x.snd ^ ↑μ x.fst = f n
[PROOFSTEP]
rw [dif_pos hn, ← Units.eq_iff, ← Units.coeHom_apply, map_prod, Units.val_mk0, prod_congr rfl _]
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
⊢ ∀ (x : ℕ × ℕ),
    x ∈ divisorsAntidiagonal n →
      ↑(Units.coeHom R) ((if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst) =
        g x.snd ^ ↑μ x.fst
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ (n : ℕ), n > 0 → f n ≠ 0
hg : ∀ (n : ℕ), n > 0 → g n ≠ 0
n : ℕ
hn : n > 0
x : ℕ × ℕ
hx : x ∈ divisorsAntidiagonal n
⊢ ↑(Units.coeHom R) ((if h : 0 < x.snd then Units.mk0 (g x.snd) (_ : g x.snd ≠ 0) else 1) ^ ↑μ x.fst) =
    g x.snd ^ ↑μ x.fst
[PROOFSTEP]
rw [dif_pos (Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal hx)), Units.coeHom_apply,
  Units.val_zpow_eq_zpow_val, Units.val_mk0]
