Where should List.mem_eraseDup and List.mem_eraseDups live?

ToBatteries_EraseDup.lean

/-
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

ToStd_EraseDups.lean

/-
Author: Nicolas Rouquette with help from Github Copilot with Claude Opus 4.5
Contribution from Robin Arnez
Developed with Lean 4.26.0
-/

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

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

`eraseDups` is defined in Lean core as `eraseDupsBy (· == ·)`.

## Main Results

* `List.mem_eraseDupsBy_loop`: Loop invariant for `eraseDupsBy.loop`
* `List.mem_eraseDups`: `a ∈ l.eraseDups ↔ a ∈ l` for `LawfulBEq` types

## Implementation Notes

The proof factors out the loop invariant as a separate lemma. The key insight is that
for the accumulator-based `eraseDupsBy.loop`, membership in the result equals
membership in the remaining input OR the accumulator.

This file has no external dependencies beyond Lean core/Std. It is intended for
contribution to Std or Lean core.

## Where this should live

Suggested location: `Std/Data/List/Lemmas.lean` or a new file
`Std/Data/List/EraseDups.lean`.
-/

namespace List

/-- Loop invariant for `eraseDupsBy.loop`: membership in the result equals
membership in the remaining list or the accumulator. -/
theorem mem_eraseDupsBy_loop [BEq α] [LawfulBEq α] {a : α} {l acc : List α} :
    a ∈ eraseDupsBy.loop (· == ·) l acc ↔ a ∈ l ∨ a ∈ acc := by
  fun_induction eraseDupsBy.loop with grind

/-- Membership is preserved by `eraseDups`: an element is in the deduplicated list
iff it was in the original list. -/
@[simp]
theorem mem_eraseDups [BEq α] [LawfulBEq α] {a : α} {l : List α} :
    a ∈ l.eraseDups ↔ a ∈ l := by
  simp only [eraseDups, eraseDupsBy, mem_eraseDupsBy_loop, not_mem_nil, or_false]

end List