apply sum_congr rfl
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) =
    ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
f : ℕ → ℕ → ℕ → ℝ
n : ℕ
⊢ ∀ x ∈ n.divisors,
    (∑ d1 ∈ x.divisors, ∑ d2 ∈ x.divisors, if x = d1.lcm d2 then f d1 d2 x else 0) =
      ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if x = d1.lcm d2 then f d1 d2 x else 0