-- 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:
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) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
trans (ζ : ArithmeticFunction ℤ) • f' = g'

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) ↔ ↑ζ • f' = g'

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

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

Tactic:
apply forall_congr'

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' := ⋯ }
⊢ ∀ (a : ℕ), a > 0 → ∑ i ∈ a.divisors, f i = g a ↔ (↑ζ • f') a = g' a

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

Tactic:
simp

Result:
no goals

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

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

Tactic:
apply forall_congr'

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

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

Tactic:
rw [← h, ← mul_smul, moebius_mul_coe_zeta, 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' := ⋯ }
n : ℕ
⊢ (μ • g') n = f' n ↔ n > 0 → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

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

Result:
no goals

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

Tactic:
trans μ • g' = f'

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' := ⋯ }
⊢ ↑ζ • f' = g' ↔ μ • g' = f'

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' := ⋯ }
⊢ μ • g' = f' ↔ ∀ 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' := ⋯ }
⊢ ↑ζ • f' = g' ↔ μ • g' = f'

Tactic:
constructor <;> intro h

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

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'