have h3' : ∀ b ∈ Finset.univ (α := ↑B), (Finset.filter {a | f a = b } (Finset.univ (α := ↑A))).card = n := by
  intro b _
  rw [← @Fintype.card_subtype]
  rw [← h1
      b, h2,
      Set.setOf_set, Fintype.card_eq_nat_card,
      Mathlib.Tactic.Zify.natCast_eq, Fintype.card_eq_nat_card]
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
⊢ B.ncard * n = A.ncard
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
⊢ B.ncard * n = A.ncard