1. Geb
  2. Mathlib
  3. Data
  4. List
  5. NodupEquivFin
Imports
/- Copyright (c) 2026 Terence Rokop. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Rokop -/ module public import Mathlib.Data.List.Nodup public import Mathlib.Logic.Equiv.Basic public import Mathlib.Tactic.Finiteness.Attr public import Mathlib.Tactic.ToAdditive public import Mathlib.Tactic.ToDual

Choice-free inversion of a duplicate-free list

List.Nodup.getEquiv depends on Classical.choice through a single ingredient, List.idxOf_lt_length_iff. Substituting List.idxOf_lt_length_of_mem, which depends on propext alone, rebuilds it choice-free. Fin.compressEquiv renumbers the indices satisfying a Bool-valued predicate, which is what an equalizer or a coequalizer carrier needs.

Main definitions

    List.Nodup.getEquivC — the choice-free rebuild of List.Nodup.getEquiv.

    Fin.compressEquiv — the indices satisfying a predicate, renumbered.

Tags

list, nodup, equiv, choice-free

@[expose] public sectionuniverse unamespace List.Nodup

Indices of a duplicate-free list correspond to its members. Choice-free rebuild of List.Nodup.getEquiv.

def getEquivC {α : Type u} [DecidableEq α] (l : List α) (H : l.Nodup) : Fin l.length ≃ {x // x ∈ l} where toFun i := ⟨l.get i, List.get_mem _ _⟩ invFun x := ⟨l.idxOf ↑x, List.idxOf_lt_length_of_mem x.2⟩ left_inv i := α:Type uinst✝:DecidableEq αl:List αH:l.Nodupi:Fin l.length⊢ (fun x ↦ ⟨idxOf (↑x) l, ⋯⟩) ((fun i ↦ ⟨l.get i, ⋯⟩) i) = i All goals completed! 🐙 right_inv x := α:Type uinst✝:DecidableEq αl:List αH:l.Nodupx:{ x // x ∈ l }⊢ (fun i ↦ ⟨l.get i, ⋯⟩) ((fun x ↦ ⟨idxOf (↑x) l, ⋯⟩) x) = x All goals completed! 🐙
end List.Nodupnamespace Fin

The indices of Fin n satisfying p, renumbered onto an initial segment.

def compressEquiv {n : ℕ} (p : Fin n → Bool) : Fin ((List.finRange n).filter p).length ≃ {i : Fin n // p i} := (List.Nodup.getEquivC _ ((List.nodup_finRange n).filter p)).trans (Equiv.subtypeEquivRight (fun x ↦ n:ℕp:Fin n → Boolx:Fin n⊢ x ∈ List.filter p (List.finRange n) ↔ p x = true All goals completed! 🐙))
end Fin