rw [mem_filter, Finset.mem_product, mem_divisors, mem_divisors, Nat.f]
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)
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