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

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

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