[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α : Type u_4
β : α → Type u_5
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
x✝ : Sigma β
a : α
b : β a
⊢ { fst := a, snd := b } ∈ Finset.sigma univ fun x => univ
[PROOFSTEP]
simp
