-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sum_eq_iff_sum_smul_moebius_eq [AddCommGroup R] {f g : ℕ → R} :
    (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
      ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd = f n

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • if x.2 = 0 then 0 else g x.2) = f (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g x.2 = f (n + 1)

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

Result:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
x : ℕ × ℕ
hx : x ∈ (n + 1).divisorsAntidiagonal
⊢ (μ x.1 • if x.2 = 0 then 0 else g x.2) = μ x.1 • g x.2

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ↑ζ • f' = g'

Tactic:
rw [ArithmeticFunction.ext_iff]

Result:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ (x : ℕ), (↑ζ • f') x = g' x

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (∑ x ∈ (n + 1).divisors, if x = 0 then 0 else f x) = g (n + 1)

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

Result:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n x : ℕ
hx : x ∈ (n + 1).divisors
⊢ f x = if x = 0 then 0 else f x

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
h : μ • g' = f'
⊢ ↑ζ • f' = g'

Tactic:
rw [← h, ← mul_smul, coe_zeta_mul_moebius, one_smul]

Result:
no goals

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ ∀ (a : ℕ), a > 0 → ∑ i ∈ a.divisors, f i = g a ↔ (↑ζ • f') a = g' a

Tactic:
intro n

Result:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n > 0 → ∑ i ∈ n.divisors, f i = g n ↔ (↑ζ • f') n = g' n

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n > 0 → ∑ i ∈ n.divisors, f i = g n ↔ (↑ζ • f') n = g' n

Tactic:
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 [f', g', coe_mk, succ_ne_zero, ite_false]
  rw [sum_congr rfl fun x hx => ?_]
  rw [if_neg (Nat.pos_of_mem_divisors hx).ne']

Result:
no goals

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ ∑ i ∈ (n + 1).divisors, f' i = g' (n + 1)

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

Result:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (∑ x ∈ (n + 1).divisors, if x = 0 then 0 else f x) = g (n + 1)

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n x : ℕ
hx : x ∈ (n + 1).divisors
⊢ f x = if x = 0 then 0 else f x

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

Result:
no goals

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ (↑ζ • f') (n + 1) = g' (n + 1)

Tactic:
rw [coe_zeta_smul_apply]

Result:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ n + 1 > 0 → ∑ i ∈ (n + 1).divisors, f i = g (n + 1) ↔ ∑ i ∈ (n + 1).divisors, f' i = g' (n + 1)

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
let f' : ArithmeticFunction R := ⟨fun x => if x = 0 then 0 else f x, if_pos rfl⟩

Result:
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' := ⋯ }
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Proof state:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
x : ℕ × ℕ
hx : x ∈ (n + 1).divisorsAntidiagonal
⊢ (μ x.1 • if x.2 = 0 then 0 else g x.2) = μ x.1 • g x.2

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

Result:
no goals

Proof state:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g' x.2 = f' (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g x.2 = f (n + 1)

Tactic:
simp only [f', g', Nat.isUnit_iff, coe_mk, ZeroHom.toFun_eq_coe, succ_ne_zero, ite_false]

Result:
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' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x => if x = 0 then 0 else g x, map_zero' := ⋯ }
n : ℕ
⊢ (∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • if x.2 = 0 then 0 else g x.2) = f (n + 1) ↔
    ∑ x ∈ (n + 1).divisorsAntidiagonal, μ x.1 • g x.2 = f (n + 1)