no goals
α : Type u_1
β : Type ?u.8468
σ : α → Type u_2
l₁ : List α
l₂ : (a : α) → List (σ a)
a : α
b : σ a
⊢ { fst := a, snd := b } ∈ List.sigma l₁ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a
simp [List.sigma, mem_bind, mem_map, exists_prop, exists_and_left, and_left_comm,
  exists_eq_left, heq_iff_eq, exists_eq_right]