rw [← card_finMulAntidiagonal hn, eq_comm]
n : ℕ
hn : Squarefree n
⊢ (filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)).card =
    3 ^ ω n
n : ℕ
hn : Squarefree n
⊢ (finMulAntidiagonal 3 n).card =
    (filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)).card