/-
Author: Nicolas Rouquette with help from Github Copilot with Claude Opus 4.5
Contribution from Vlad Tsyrklevich (vlad902)
Developed with Lean 4.26.0 and Batteries 4.26.0
-/
import Batteries.Data.List.Pairwise
import Batteries.Data.List.Basic

/-!
# Membership lemma for `List.eraseDup`

This file provides `List.mem_eraseDup`, proving that membership is preserved by
`eraseDup` for types with `LawfulBEq`.

## Main Results

* `List.mem_eraseDup`: `a ∈ l.eraseDup ↔ a ∈ l` for `LawfulBEq` types

## Implementation Notes

`eraseDup` is defined as `pwFilter (· != ·)`. The proof uses:
- `pwFilter_subset` for the forward direction
- Induction with `pwFilter_cons_of_pos/neg` for the reverse direction

Unlike `eraseDups` (which uses an accumulator-based loop), `pwFilter` processes
front-to-back keeping elements that are distinct from all later kept elements.
This makes the proof structure inherently different - there's no simple loop
invariant to factor out.

This file is intended for contribution to Batteries. It has no Mathlib dependencies.

## Where this should live

Suggested location: `Batteries/Data/List/Pairwise.lean` or a new file
`Batteries/Data/List/EraseDup.lean` that imports `Pairwise`.
-/

namespace List

/-- Membership is preserved by `eraseDup`: an element is in the deduplicated list
iff it was in the original list. This is the `BEq`/`LawfulBEq` analogue of
Mathlib's `List.mem_dedup` which requires `DecidableEq`. -/
@[simp]
theorem mem_eraseDup [BEq α] [LawfulBEq α] {a : α} {l : List α} :
    a ∈ l.eraseDup ↔ a ∈ l := by
  constructor
  · intro h; exact pwFilter_subset l h
  · intro h
    induction l with
    | nil => exact h
    | cons x xs ih =>
      simp only [mem_cons] at h
      -- Split once: does `x` survive the pwFilter step?
      by_cases hx : ∀ y ∈ xs.eraseDup, (x != y) = true
      · -- x kept: eraseDup (x::xs) = x :: eraseDup xs
        rw [eraseDup, pwFilter_cons_of_pos hx, mem_cons]
        rcases h with rfl | hxs
        · left; rfl
        · right; exact ih hxs
      · -- x dropped: eraseDup (x::xs) = eraseDup xs
        rw [eraseDup, pwFilter_cons_of_neg hx]
        rcases h with rfl | hxs
        · simp_all [eraseDup]  -- extracts witness showing a ∈ xs.eraseDup
        · exact ih hxs

end List