simp only [mem_image, ne_eq, mem_divisors, Nat.isUnit_iff]
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiagonal n) ↔ k ∈ n.divisors
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) ↔ k ∣ n ∧ ¬n = 0