simp only [mem_univ, not_true, IsEmpty.forall_iff, implies_true, ne_eq, true_and,
  Fintype.mem_piFinset, mem_divisors, Nat.isUnit_iff, mem_filter]
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m