rw [hx2] at 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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : f x = b1
hx3 : f x = b2
⊢ False
α : 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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : f x = b1
hx3 : b1 = b2
⊢ False