rw [←finMulAntidiagonal_three a ha]
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ n = a 1 * a 2 * a 0
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0