simp_rw [mem_finMulAntidiagonal]
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiagonal n, a i = k
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a, (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k