have h4 :
  ∀ b1 ∈ (Finset.univ (α := ↑B)),
    ∀ b2 ∈ (Finset.univ (α := ↑B)),
      b1 ≠ b2 →
        Disjoint
          (Finset.filter { a | f a = b1 } (Finset.univ (α := ↑A)))
          (Finset.filter { a | f a = b2 } (Finset.univ (α := ↑A))) := by
  intro b1 _ b2 _ hb12
  rw [Finset.disjoint_filter]
  intro x _ hx2 hx3
  rw [Set.setOf_app_iff] at hx2 hx3
  rw [hx2] at hx3
  exact hb12 hx3
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
⊢ B.ncard * n = A.ncard
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ B.ncard * n = A.ncard