rintro rfl
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
d1 d2 : ℕ
⊢ d = d1.lcm d2 → d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2
case e_f.h.e_f.h.e_c
f : ℕ → ℕ → ℕ → ℝ
n d1 d2 : ℕ
hd : d1.lcm d2 ∣ n ∧ n ≠ 0
⊢ d1 ∣ d1.lcm d2 ∧ d2 ∣ d1.lcm d2 ∧ d1.lcm d2 = d1.lcm d2