simp only [piFinTwoEquiv_apply, mem_image, mem_finMulAntidiagonal, Fin.prod_univ_two, ne_eq,
  mem_divisorsAntidiagonal]
case a
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) ↔ x ∈ n.divisorsAntidiagonal
case a
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) ↔ x.1 * x.2 = n ∧ ¬n = 0