congr with d1
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
⊢ (∑ x ∈ n.divisors, ∑ x_1 ∈ n.divisors, if x ∣ d ∧ x_1 ∣ d ∧ d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
case e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 : ℕ
⊢ (∑ x ∈ n.divisors, if d1 ∣ d ∧ x ∣ d ∧ d = d1.lcm x then f d1 x d else 0) =
    ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0