rw [mem_finMulAntidiagonal]
case a.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiagonal m
case a.mpr
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0