R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ (n : ℕ), 0 < n → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n) ↔
    ∀ (n : ℕ), 0 < n → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ (n : ℕ), 0 < n → ∑ i in divisors n, f i = g n) ↔
    ∀ (n : ℕ), 0 < n → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
rw [sum_eq_iff_sum_smul_moebius_eq]
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    0 < a → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a ↔
      0 < a → ∑ x in divisorsAntidiagonal a, ↑(↑μ x.fst) * g x.snd = f a
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ (∀ (n : ℕ), 0 < n → ∑ x in divisorsAntidiagonal n, ↑μ x.fst • g x.snd = f n) ↔
    ∀ (n : ℕ), 0 < n → ∑ x in divisorsAntidiagonal n, ↑(↑μ x.fst) * g x.snd = f n
apply forall_congr'
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
a : ℕ
x✝ : 0 < a
x : ℕ × ℕ
_hx : x ∈ divisorsAntidiagonal a
⊢ ↑μ x.fst • g x.snd = ↑(↑μ x.fst) * g x.snd
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    0 < a → ∑ x in divisorsAntidiagonal a, ↑μ x.fst • g x.snd = f a ↔
      0 < a → ∑ x in divisorsAntidiagonal a, ↑(↑μ x.fst) * g x.snd = f a
refine' fun a => imp_congr_right fun _ => (sum_congr rfl fun x _hx => _).congr_left
no goals
case h
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
a : ℕ
x✝ : 0 < a
x : ℕ × ℕ
_hx : x ∈ divisorsAntidiagonal a
⊢ ↑μ x.fst • g x.snd = ↑(↑μ x.fst) * g x.snd
rw [zsmul_eq_mul]