dsimp only
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
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2