-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sum_eq_iff_sum_mul_moebius_eq_on [Ring R] {f g : ℕ → R}
    (s : Set ℕ) (hs : ∀ m n, m ∣ n → n ∈ s → m ∈ s) :
    (∀ n > 0, n ∈ s → (∑ i ∈ n.divisors, f i) = g n) ↔
      ∀ n > 0, n ∈ s →
        (∑ x ∈ n.divisorsAntidiagonal, (μ x.fst : R) * g x.snd) = f n

Proof state:
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 ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a

Tactic:
intro a

Result:
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 ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a

Proof state:
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 ∈ a.divisorsAntidiagonal
⊢ μ x.1 • g x.2 = ↑(μ x.1) * g x.2

Tactic:
rw [zsmul_eq_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
rw [sum_eq_iff_sum_smul_moebius_eq_on s hs]

Result:
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Proof state:
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 ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a

Tactic:
refine imp_congr_right ?_

Result:
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 ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a)

Proof state:
R : Type u_1
inst✝ : Ring R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
apply forall_congr'

Result:
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 ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a

Proof state:
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 ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a)

Tactic:
refine fun _ => imp_congr_right fun _ => (sum_congr rfl fun x _hx => ?_).congr_left

Result:
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 ∈ a.divisorsAntidiagonal
⊢ μ x.1 • g x.2 = ↑(μ x.1) * g x.2