refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩ <;> rw [←finMulAntidiagonal_three a ha]
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (((a 0 * a 1, a 0 * a 2).1 ∣ n ∧ n ≠ 0) ∧ (a 0 * a 1, a 0 * a 2).2 ∣ n ∧ n ≠ 0) ∧
    match (a 0 * a 1, a 0 * a 2) with
    | (x, y) => x.lcm y = n
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2

case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2