Theorem: Nat.card_lcm_eq (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

State before:
n : ℕ
hn : Squarefree n
⊢ (filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)).card =
    3 ^ ω n
Tactic:
rw [← card_finMulAntidiagonal hn, eq_comm]
State after:
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

State before:
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
Tactic:
exact Finset.card_bij f (f_img hn) f_inj (f_surj hn.ne_zero)
State after:
no goals