rw [←Nat.dvd_one, ←hf]
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i