simp only [mem_finMulAntidiagonal, and_true, mem_singleton]
case a
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal 1 ↔ f ∈ {fun x => 1}
case a
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1