congr
case e_f.h.e_f.h
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (if d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2 then f d1 d2 d else 0) = if d = d1.lcm d2 then f d1 d2 d else 0
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)