English
A specialized equality about mem_enum and subset relation holds for DecidableEq α.
Русский
Специализированное равенство mem_enum и отношение подмножества справедливо при DecidableEq α.
LaTeX
$$$ \\forall {α} [DecidableEq α], (s: Finset α) (xs: List α), s \\in \\mathrm{Finset.enum}(xs) \\iff \\forall x \\in s, x \\in xs. $$$
Lean4
@[simp, grind =]
theorem mem_enum [DecidableEq α] (s : Finset α) (xs : List α) : s ∈ Finset.enum xs ↔ ∀ x ∈ s, x ∈ xs := by
induction xs generalizing s with
| nil => simp [enum, eq_empty_iff_forall_notMem]
| cons x xs
ih =>
simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons, List.not_mem_nil, or_false, ih]
refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
simp only [or_iff_not_imp_left] at hs
simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]
