rw [Set.setOf_set, Fintype.card_eq_nat_card, ←Set.Nat.card_coe_set_eq]
α : 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 }
b : { x // B x }
⊢ {a | f a = b}.ncard = Fintype.card { a // f a = b }
α : 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 }
b : { x // B x }
⊢ (Nat.card ↑fun a => f a = b) = Nat.card { a // f a = b }