Theorem: List.Index.prod_unprod (Extra/Index/Prod.lean)

State before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
k : (xs.prod ys).Index
⊢ prod k.unprod = k
Tactic:
simp only [prod, unprod]
State after:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
k : (xs.prod ys).Index
⊢ bind (fun x => List.map (Prod.mk x) ys)
      ⟨(unbind (fun x => List.map (Prod.mk x) ys) k).fst,
        map (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
          (unmap (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
            (unbind (fun x => List.map (Prod.mk x) ys) k).snd)⟩ =
    k

State before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
k : (xs.prod ys).Index
⊢ bind (fun x => List.map (Prod.mk x) ys)
      ⟨(unbind (fun x => List.map (Prod.mk x) ys) k).fst,
        map (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
          (unmap (Prod.mk (unbind (fun x => List.map (Prod.mk x) ys) k).fst.val)
            (unbind (fun x => List.map (Prod.mk x) ys) k).snd)⟩ =
    k
Tactic:
rw [map_unmap, bind_unbind]
State after:
no goals