English
For a : α and xs : List (Sigma β), a ∈ xs.toFinmap iff ∃ b : β(a), Sigma.mk a b ∈ xs.
Русский
Для a : α и xs : List (Sigma β), a ∈ xs.toFinmap тогда и только тогда, когда ∃ b : β(a), Sigma.mk a b ∈ xs.
LaTeX
$$$ a ∈ xs.toFinmap \iff \exists b : \beta\ a, \ Sigma\mk a b \in xs $$$
Lean4
theorem mem_list_toFinmap (a : α) (xs : List (Sigma β)) : a ∈ xs.toFinmap ↔ ∃ b : β a, Sigma.mk a b ∈ xs := by
induction xs with
| nil => simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]
| cons x xs =>
obtain ⟨fst_i, snd_i⟩ := x
simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
refine (or_congr_left <| and_iff_left_of_imp ?_).symm
rintro rfl
simp only [exists_eq, heq_iff_eq]
