Documentation

Init.Data.List.Attach

def List.pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (l : List α) (H : ∀ (a : α), a lP a) :
List β

O(n). Partial map. If f : Π a, P a → β is a partial function defined on a : α satisfying P, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy P, using the proof to apply f.

Equations
Instances For
    @[implemented_by _private.Init.Data.List.Attach.0.List.attachWithImpl]
    def List.attachWith {α : Type u_1} (l : List α) (P : αProp) (H : ∀ (x : α), x lP x) :
    List { x : α // P x }

    O(1). "Attach" a proof P x that holds for all the elements of l to produce a new list with the same elements but in the type {x // P x}.

    Equations
    Instances For
      @[inline]
      def List.attach {α : Type u_1} (l : List α) :
      List { x : α // x l }

      O(1). "Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

      Equations
      Instances For
        @[simp]
        theorem List.attach_nil {α : Type u_1} :
        [].attach = []
        @[simp]
        theorem List.attachWith_nil {α : Type u_1} {P : αProp} {H : ∀ (x : α), x []P x} :
        [].attachWith P H = []
        @[simp]
        theorem List.pmap_eq_map {α : Type u_1} {β : Type u_2} (p : αProp) (f : αβ) (l : List α) (H : ∀ (a : α), a lp a) :
        List.pmap (fun (a : α) (x : p a) => f a) l H = List.map f l
        theorem List.pmap_congr_left {α : Type u_1} {β : Type u_2} {p : αProp} {q : αProp} {f : (a : α) → p aβ} {g : (a : α) → q aβ} (l : List α) {H₁ : ∀ (a : α), a lp a} {H₂ : ∀ (a : α), a lq a} (h : ∀ (a : α), a l∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) :
        List.pmap f l H₁ = List.pmap g l H₂
        @[reducible, inline, deprecated List.pmap_congr_left]
        abbrev List.pmap_congr {α : Type u_1} {β : Type u_2} {p : αProp} {q : αProp} {f : (a : α) → p aβ} {g : (a : α) → q aβ} (l : List α) {H₁ : ∀ (a : α), a lp a} {H₂ : ∀ (a : α), a lq a} (h : ∀ (a : α), a l∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) :
        List.pmap f l H₁ = List.pmap g l H₂
        Equations
        Instances For
          theorem List.map_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : αProp} (g : βγ) (f : (a : α) → p aβ) (l : List α) (H : ∀ (a : α), a lp a) :
          List.map g (List.pmap f l H) = List.pmap (fun (a : α) (h : p a) => g (f a h)) l H
          theorem List.pmap_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {p : βProp} (g : (b : β) → p bγ) (f : αβ) (l : List α) (H : ∀ (a : β), a List.map f lp a) :
          List.pmap g (List.map f l) H = List.pmap (fun (a : α) (h : p (f a)) => g (f a) h) l
          theorem List.attach_congr {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : l₁ = l₂) :
          l₁.attach = List.map (fun (x : { x : α // x l₂ }) => x.val, ) l₂.attach
          theorem List.attachWith_congr {α : Type u_1} {l₁ : List α} {l₂ : List α} (w : l₁ = l₂) {P : αProp} {H : ∀ (x : α), x l₁P x} :
          l₁.attachWith P H = l₂.attachWith P
          @[simp]
          theorem List.attach_cons {α : Type u_1} {x : α} {xs : List α} :
          (x :: xs).attach = x, :: List.map (fun (x_1 : { x : α // x xs }) => match x_1 with | y, h => y, ) xs.attach
          @[simp]
          theorem List.attachWith_cons {α : Type u_1} {x : α} {xs : List α} {p : αProp} (h : ∀ (a : α), a x :: xsp a) :
          (x :: xs).attachWith p h = x, :: xs.attachWith p
          theorem List.pmap_eq_map_attach {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (l : List α) (H : ∀ (a : α), a lp a) :
          List.pmap f l H = List.map (fun (x : { x : α // x l }) => f x.val ) l.attach
          theorem List.attach_map_coe {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) :
          List.map (fun (i : { i : α // i l }) => f i.val) l.attach = List.map f l
          theorem List.attach_map_val {α : Type u_1} {β : Type u_2} (l : List α) (f : αβ) :
          List.map (fun (i : { x : α // x l }) => f i.val) l.attach = List.map f l
          @[simp]
          theorem List.attach_map_subtype_val {α : Type u_1} (l : List α) :
          List.map Subtype.val l.attach = l
          theorem List.attachWith_map_coe {α : Type u_1} {β : Type u_2} {p : αProp} (f : αβ) (l : List α) (H : ∀ (a : α), a lp a) :
          List.map (fun (i : { i : α // p i }) => f i.val) (l.attachWith p H) = List.map f l
          theorem List.attachWith_map_val {α : Type u_1} {β : Type u_2} {p : αProp} (f : αβ) (l : List α) (H : ∀ (a : α), a lp a) :
          List.map (fun (i : { x : α // p x }) => f i.val) (l.attachWith p H) = List.map f l
          @[simp]
          theorem List.attachWith_map_subtype_val {α : Type u_1} {p : αProp} (l : List α) (H : ∀ (a : α), a lp a) :
          List.map Subtype.val (l.attachWith p H) = l
          @[simp]
          theorem List.mem_attach {α : Type u_1} (l : List α) (x : { x : α // x l }) :
          x l.attach
          @[simp]
          theorem List.mem_pmap {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} {b : β} :
          b List.pmap f l H ∃ (a : α), ∃ (h : a l), f a = b
          theorem List.mem_pmap_of_mem {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} {a : α} (h : a l) :
          f a List.pmap f l H
          @[simp]
          theorem List.length_pmap {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} :
          (List.pmap f l H).length = l.length
          @[simp]
          theorem List.length_attach {α : Type u_1} {L : List α} :
          L.attach.length = L.length
          @[simp]
          theorem List.length_attachWith {α : Type u_1} {p : αProp} {l : List α} {H : ∀ (x : α), x lp x} :
          (l.attachWith p H).length = l.length
          @[simp]
          theorem List.pmap_eq_nil_iff {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} :
          List.pmap f l H = [] l = []
          theorem List.pmap_ne_nil_iff {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) {xs : List α} (H : ∀ (a : α), a xsP a) :
          List.pmap f xs H [] xs []
          @[simp]
          theorem List.attach_eq_nil_iff {α : Type u_1} {l : List α} :
          l.attach = [] l = []
          theorem List.attach_ne_nil_iff {α : Type u_1} {l : List α} :
          l.attach [] l []
          @[simp]
          theorem List.attachWith_eq_nil_iff {α : Type u_1} {l : List α} {P : αProp} {H : ∀ (a : α), a lP a} :
          l.attachWith P H = [] l = []
          theorem List.attachWith_ne_nil_iff {α : Type u_1} {l : List α} {P : αProp} {H : ∀ (a : α), a lP a} :
          l.attachWith P H [] l []
          @[reducible, inline, deprecated List.pmap_eq_nil_iff]
          abbrev List.pmap_eq_nil {α : Type u_1} {β : Type u_2} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} :
          List.pmap f l H = [] l = []
          Equations
          Instances For
            @[reducible, inline, deprecated List.pmap_ne_nil_iff]
            abbrev List.pmap_ne_nil {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) {xs : List α} (H : ∀ (a : α), a xsP a) :
            List.pmap f xs H [] xs []
            Equations
            Instances For
              @[reducible, inline, deprecated List.attach_eq_nil_iff]
              abbrev List.attach_eq_nil {α : Type u_1} {l : List α} :
              l.attach = [] l = []
              Equations
              Instances For
                @[reducible, inline, deprecated List.attach_ne_nil_iff]
                abbrev List.attach_ne_nil {α : Type u_1} {l : List α} :
                l.attach [] l []
                Equations
                Instances For
                  @[simp]
                  theorem List.getElem?_pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) (n : Nat) :
                  (List.pmap f l h)[n]? = Option.pmap f l[n]?
                  theorem List.get?_pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) (n : Nat) :
                  (List.pmap f l h).get? n = Option.pmap f (l.get? n)
                  @[simp]
                  theorem List.getElem_pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) {n : Nat} (hn : n < (List.pmap f l h).length) :
                  (List.pmap f l h)[n] = f l[n]
                  theorem List.get_pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) {n : Nat} (hn : n < (List.pmap f l h).length) :
                  (List.pmap f l h).get n, hn = f (l.get n, )
                  @[simp]
                  theorem List.getElem?_attachWith {α : Type u_1} {xs : List α} {i : Nat} {P : αProp} {H : ∀ (a : α), a xsP a} :
                  (xs.attachWith P H)[i]? = Option.pmap Subtype.mk xs[i]?
                  @[simp]
                  theorem List.getElem?_attach {α : Type u_1} {xs : List α} {i : Nat} :
                  xs.attach[i]? = Option.pmap Subtype.mk xs[i]?
                  @[simp]
                  theorem List.getElem_attachWith {α : Type u_1} {xs : List α} {P : αProp} {H : ∀ (a : α), a xsP a} {i : Nat} (h : i < (xs.attachWith P H).length) :
                  (xs.attachWith P H)[i] = xs[i],
                  @[simp]
                  theorem List.getElem_attach {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.attach.length) :
                  xs.attach[i] = xs[i],
                  @[simp]
                  theorem List.head?_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) :
                  (List.pmap f xs H).head? = Option.map (fun (x : { x : α // x xs }) => match x with | a, m => f a ) xs.attach.head?
                  @[simp]
                  theorem List.head_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) (h : List.pmap f xs H []) :
                  (List.pmap f xs H).head h = f (xs.head )
                  @[simp]
                  theorem List.head?_attachWith {α : Type u_1} {P : αProp} {xs : List α} (H : ∀ (a : α), a xsP a) :
                  (xs.attachWith P H).head? = xs.head?.pbind fun (a : α) (h : a xs.head?) => some a,
                  @[simp]
                  theorem List.head_attachWith {α : Type u_1} {P : αProp} {xs : List α} {H : ∀ (a : α), a xsP a} (h : xs.attachWith P H []) :
                  (xs.attachWith P H).head h = xs.head ,
                  @[simp]
                  theorem List.head?_attach {α : Type u_1} (xs : List α) :
                  xs.attach.head? = xs.head?.pbind fun (a : α) (h : a xs.head?) => some a,
                  @[simp]
                  theorem List.head_attach {α : Type u_1} {xs : List α} (h : xs.attach []) :
                  xs.attach.head h = xs.head ,
                  @[simp]
                  theorem List.tail_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) :
                  (List.pmap f xs H).tail = List.pmap f xs.tail
                  @[simp]
                  theorem List.tail_attachWith {α : Type u_1} {P : αProp} {xs : List α} {H : ∀ (a : α), a xsP a} :
                  (xs.attachWith P H).tail = xs.tail.attachWith P
                  @[simp]
                  theorem List.tail_attach {α : Type u_1} (xs : List α) :
                  xs.attach.tail = List.map (fun (x : { x : α // x xs.tail }) => match x with | x, h => x, ) xs.tail.attach
                  theorem List.foldl_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : List α) {P : αProp} (f : (a : α) → P aβ) (H : ∀ (a : α), a lP a) (g : γβγ) (x : γ) :
                  List.foldl g x (List.pmap f l H) = List.foldl (fun (acc : γ) (a : { x : α // x l }) => g acc (f a.val )) x l.attach
                  theorem List.foldr_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : List α) {P : αProp} (f : (a : α) → P aβ) (H : ∀ (a : α), a lP a) (g : βγγ) (x : γ) :
                  List.foldr g x (List.pmap f l H) = List.foldr (fun (a : { x : α // x l }) (acc : γ) => g (f a.val ) acc) x l.attach
                  theorem List.foldl_attach {α : Type u_1} {β : Type u_2} (l : List α) (f : βαβ) (b : β) :
                  List.foldl (fun (acc : β) (t : { x : α // x l }) => f acc t.val) b l.attach = List.foldl f b l

                  If we fold over l.attach with a function that ignores the membership predicate, we get the same results as folding over l directly.

                  This is useful when we need to use attach to show termination.

                  Unfortunately this can't be applied by simp because of the higher order unification problem, and even when rewriting we need to specify the function explicitly.

                  theorem List.foldr_attach {α : Type u_1} {β : Type u_2} (l : List α) (f : αββ) (b : β) :
                  List.foldr (fun (t : { x : α // x l }) (acc : β) => f t.val acc) b l.attach = List.foldr f b l

                  If we fold over l.attach with a function that ignores the membership predicate, we get the same results as folding over l directly.

                  This is useful when we need to use attach to show termination.

                  Unfortunately this can't be applied by simp because of the higher order unification problem, and even when rewriting we need to specify the function explicitly.

                  theorem List.attach_map {α : Type u_1} {β : Type u_2} {l : List α} (f : αβ) :
                  (List.map f l).attach = List.map (fun (x : { x : α // x l }) => match x with | x, h => f x, ) l.attach
                  theorem List.attachWith_map {α : Type u_1} {β : Type u_2} {l : List α} (f : αβ) {P : βProp} {H : ∀ (b : β), b List.map f lP b} :
                  (List.map f l).attachWith P H = List.map (fun (x : { x : α // (P f) x }) => match x with | x, h => f x, h) (l.attachWith (P f) )
                  theorem List.map_attachWith {α : Type u_1} {β : Type u_2} {l : List α} {P : αProp} {H : ∀ (a : α), a lP a} (f : { x : α // P x }β) :
                  List.map f (l.attachWith P H) = List.pmap (fun (a : α) (h : a l P a) => f a, ) l
                  theorem List.map_attach {α : Type u_1} {β : Type u_2} {l : List α} (f : { x : α // x l }β) :
                  List.map f l.attach = List.pmap (fun (a : α) (h : a l) => f a, h) l

                  See also pmap_eq_map_attach for writing pmap in terms of map and attach.

                  theorem List.attach_filterMap {α : Type u_1} {β : Type u_2} {l : List α} {f : αOption β} :
                  (List.filterMap f l).attach = List.filterMap (fun (x : { x : α // x l }) => match x with | x, h => (f x).pbind fun (b : β) (m : b f x) => some b, ) l.attach
                  theorem List.attach_filter {α : Type u_1} {l : List α} (p : αBool) :
                  (List.filter p l).attach = List.filterMap (fun (x : { x : α // x l }) => if w : p x.val = true then some x.val, else none) l.attach
                  theorem List.pmap_pmap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : αProp} {q : βProp} (g : (a : α) → p aβ) (f : (b : β) → q bγ) (l : List α) (H₁ : ∀ (a : α), a lp a) (H₂ : ∀ (a : β), a List.pmap g l H₁q a) :
                  List.pmap f (List.pmap g l H₁) H₂ = List.pmap (fun (a : { x : α // x l }) (h : p a.val) => f (g a.val h) ) l.attach
                  @[simp]
                  theorem List.pmap_append {ι : Type u_1} {α : Type u_2} {p : ιProp} (f : (a : ι) → p aα) (l₁ : List ι) (l₂ : List ι) (h : ∀ (a : ι), a l₁ ++ l₂p a) :
                  List.pmap f (l₁ ++ l₂) h = List.pmap f l₁ ++ List.pmap f l₂
                  theorem List.pmap_append' {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (l₁ : List α) (l₂ : List α) (h₁ : ∀ (a : α), a l₁p a) (h₂ : ∀ (a : α), a l₂p a) :
                  List.pmap f (l₁ ++ l₂) = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂
                  @[simp]
                  theorem List.attach_append {α : Type u_1} (xs : List α) (ys : List α) :
                  (xs ++ ys).attach = List.map (fun (x : { x : α // x xs }) => match x with | x, h => x, ) xs.attach ++ List.map (fun (x : { x : α // x ys }) => match x with | x, h => x, ) ys.attach
                  @[simp]
                  theorem List.attachWith_append {α : Type u_1} {P : αProp} {xs : List α} {ys : List α} {H : ∀ (a : α), a xs ++ ysP a} :
                  (xs ++ ys).attachWith P H = xs.attachWith P ++ ys.attachWith P
                  @[simp]
                  theorem List.pmap_reverse {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xs.reverseP a) :
                  List.pmap f xs.reverse H = (List.pmap f xs ).reverse
                  theorem List.reverse_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) :
                  (List.pmap f xs H).reverse = List.pmap f xs.reverse
                  @[simp]
                  theorem List.attachWith_reverse {α : Type u_1} {P : αProp} {xs : List α} {H : ∀ (a : α), a xs.reverseP a} :
                  xs.reverse.attachWith P H = (xs.attachWith P ).reverse
                  theorem List.reverse_attachWith {α : Type u_1} {P : αProp} {xs : List α} {H : ∀ (a : α), a xsP a} :
                  (xs.attachWith P H).reverse = xs.reverse.attachWith P
                  @[simp]
                  theorem List.attach_reverse {α : Type u_1} (xs : List α) :
                  xs.reverse.attach = List.map (fun (x : { x : α // x xs }) => match x with | x, h => x, ) xs.attach.reverse
                  theorem List.reverse_attach {α : Type u_1} (xs : List α) :
                  xs.attach.reverse = List.map (fun (x : { x : α // x xs.reverse }) => match x with | x, h => x, ) xs.reverse.attach
                  @[simp]
                  theorem List.getLast?_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) :
                  (List.pmap f xs H).getLast? = Option.map (fun (x : { x : α // x xs }) => match x with | a, m => f a ) xs.attach.getLast?
                  @[simp]
                  theorem List.getLast_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) (h : List.pmap f xs H []) :
                  (List.pmap f xs H).getLast h = f (xs.getLast )
                  @[simp]
                  theorem List.getLast?_attachWith {α : Type u_1} {P : αProp} {xs : List α} {H : ∀ (a : α), a xsP a} :
                  (xs.attachWith P H).getLast? = xs.getLast?.pbind fun (a : α) (h : a xs.getLast?) => some a,
                  @[simp]
                  theorem List.getLast_attachWith {α : Type u_1} {P : αProp} {xs : List α} {H : ∀ (a : α), a xsP a} (h : xs.attachWith P H []) :
                  (xs.attachWith P H).getLast h = xs.getLast ,
                  @[simp]
                  theorem List.getLast?_attach {α : Type u_1} {xs : List α} :
                  xs.attach.getLast? = xs.getLast?.pbind fun (a : α) (h : a xs.getLast?) => some a,
                  @[simp]
                  theorem List.getLast_attach {α : Type u_1} {xs : List α} (h : xs.attach []) :
                  xs.attach.getLast h = xs.getLast ,
                  @[simp]
                  theorem List.countP_attach {α : Type u_1} (l : List α) (p : αBool) :
                  List.countP (fun (a : { x : α // x l }) => p a.val) l.attach = List.countP p l
                  @[simp]
                  theorem List.countP_attachWith {α : Type u_1} {p : αProp} (l : List α) (H : ∀ (a : α), a lp a) (q : αBool) :
                  List.countP (fun (a : { x : α // p x }) => q a.val) (l.attachWith p H) = List.countP q l
                  @[simp]
                  theorem List.count_attach {α : Type u_1} [DecidableEq α] (l : List α) (a : { x : α // x l }) :
                  List.count a l.attach = List.count a.val l
                  @[simp]
                  theorem List.count_attachWith {α : Type u_1} [DecidableEq α] {p : αProp} (l : List α) (H : ∀ (a : α), a lp a) (a : { x : α // p x }) :
                  List.count a (l.attachWith p H) = List.count a.val l

                  unattach #

                  List.unattach is the (one-sided) inverse of List.attach. It is a synonym for List.map Subtype.val.

                  We use it by providing a simp lemma l.attach.unattach = l, and simp lemmas which recognize higher order functions applied to l : List { x // p x } which only depend on the value, not the predicate, and rewrite these in terms of a simpler function applied to l.unattach.

                  Further, we provide simp lemmas that push unattach inwards.

                  def List.unattach {α : Type u_1} {p : αProp} (l : List { x : α // p x }) :
                  List α

                  A synonym for l.map (·.val). Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such as map_subtype, and is ideally subsequently simplified away by unattach_attach.

                  If not, usually the right approach is simp [List.unattach, -List.map_subtype] to unfold.

                  Equations
                  • l.unattach = List.map (fun (x : { x : α // p x }) => x.val) l
                  Instances For
                    @[simp]
                    theorem List.unattach_nil {α : Type u_1} {p : αProp} :
                    [].unattach = []
                    @[simp]
                    theorem List.unattach_cons {α : Type u_1} {p : αProp} {a : { x : α // p x }} {l : List { x : α // p x }} :
                    (a :: l).unattach = a.val :: l.unattach
                    @[simp]
                    theorem List.length_unattach {α : Type u_1} {p : αProp} {l : List { x : α // p x }} :
                    l.unattach.length = l.length
                    @[simp]
                    theorem List.unattach_attach {α : Type u_1} {l : List α} :
                    l.attach.unattach = l
                    @[simp]
                    theorem List.unattach_attachWith {α : Type u_1} {p : αProp} {l : List α} {H : ∀ (a : α), a lp a} :
                    (l.attachWith p H).unattach = l

                    Recognizing higher order functions on subtypes using a function that only depends on the value. #

                    @[simp]
                    theorem List.foldl_subtype {α : Type u_1} {β : Type u_2} {p : αProp} {l : List { x : α // p x }} {f : β{ x : α // p x }β} {g : βαβ} {x : β} {hf : ∀ (b : β) (x : α) (h : p x), f b x, h = g b x} :
                    List.foldl f x l = List.foldl g x l.unattach

                    This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.

                    @[simp]
                    theorem List.foldr_subtype {α : Type u_1} {β : Type u_2} {p : αProp} {l : List { x : α // p x }} {f : { x : α // p x }ββ} {g : αββ} {x : β} {hf : ∀ (x : α) (h : p x) (b : β), f x, h b = g x b} :
                    List.foldr f x l = List.foldr g x l.unattach

                    This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.

                    @[simp]
                    theorem List.map_subtype {α : Type u_1} {β : Type u_2} {p : αProp} {l : List { x : α // p x }} {f : { x : α // p x }β} {g : αβ} {hf : ∀ (x : α) (h : p x), f x, h = g x} :
                    List.map f l = List.map g l.unattach

                    This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.

                    @[simp]
                    theorem List.filterMap_subtype {α : Type u_1} {β : Type u_2} {p : αProp} {l : List { x : α // p x }} {f : { x : α // p x }Option β} {g : αOption β} {hf : ∀ (x : α) (h : p x), f x, h = g x} :
                    @[simp]
                    theorem List.bind_subtype {α : Type u_1} {β : Type u_2} {p : αProp} {l : List { x : α // p x }} {f : { x : α // p x }List β} {g : αList β} {hf : ∀ (x : α) (h : p x), f x, h = g x} :
                    l.bind f = l.unattach.bind g
                    @[simp]
                    theorem List.unattach_filter {α : Type u_1} {p : αProp} {l : List { x : α // p x }} {f : { x : α // p x }Bool} {g : αBool} {hf : ∀ (x : α) (h : p x), f x, h = g x} :
                    (List.filter f l).unattach = List.filter g l.unattach

                    Simp lemmas pushing unattach inwards. #

                    @[simp]
                    theorem List.unattach_reverse {α : Type u_1} {p : αProp} {l : List { x : α // p x }} :
                    l.reverse.unattach = l.unattach.reverse
                    @[simp]
                    theorem List.unattach_append {α : Type u_1} {p : αProp} {l₁ : List { x : α // p x }} {l₂ : List { x : α // p x }} :
                    (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach
                    @[simp]
                    theorem List.unattach_join {α : Type u_1} {p : αProp} {l : List (List { x : α // p x })} :
                    l.join.unattach = (List.map List.unattach l).join
                    @[simp]
                    theorem List.unattach_replicate {α : Type u_1} {p : αProp} {n : Nat} {x : { x : α // p x }} :
                    (List.replicate n x).unattach = List.replicate n x.val