Theorem: List.Index.pi_unpi
Proof state before:
case refl
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs✝ : List α
x : α
xs : List α
ih : ∀ (k : (List.pi f xs).Index), pi k.unpi = k
k₁ : (List.pi f xs).Index
k₂ :
  (List.map
      (fun y i =>
        match i with
        | head => y
        | i.tail => k₁.val i)
      (f x)).Index
⊢ bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨pi fun i =>
          (unbind
                  (fun ys =>
                    List.map
                      (fun y i =>
                        match i with
                        | head => y
                        | i.tail => ys i)
                      (f x))
                  (bind
                    (fun ys =>
                      List.map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => ys i)
                        (f x))
                    ⟨k₁, k₂⟩)).fst.unpi
            i,
        map
          (fun y i =>
            match i with
            | head => y
            | i.tail =>
              (pi fun i =>
                    (unbind
                            (fun ys =>
                              List.map
                                (fun y i =>
                                  match i with
                                  | head => y
                                  | i.tail => ys i)
                                (f x))
                            (bind
                              (fun ys =>
                                List.map
                                  (fun y i =>
                                    match i with
                                    | head => y
                                    | i.tail => ys i)
                                  (f x))
                              ⟨k₁, k₂⟩)).fst.unpi
                      i).val
                i)
          (unmap
            (fun y i =>
              match i with
              | head => y
              | i.tail =>
                (unbind
                        (fun ys =>
                          List.map
                            (fun y i =>
                              match i with
                              | head => y
                              | i.tail => ys i)
                            (f x))
                        (bind
                          (fun ys =>
                            List.map
                              (fun y i =>
                                match i with
                                | head => y
                                | i.tail => ys i)
                              (f x))
                          ⟨k₁, k₂⟩)).fst.val
                  i)
            (unbind
                (fun ys =>
                  List.map
                    (fun y i =>
                      match i with
                      | head => y
                      | i.tail => ys i)
                    (f x))
                (bind
                  (fun ys =>
                    List.map
                      (fun y i =>
                        match i with
                        | head => y
                        | i.tail => ys i)
                      (f x))
                  ⟨k₁, k₂⟩)).snd)⟩ =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
Tactic:
rw [unbind_bind, ih, map_unmap]
Proof state after:
no goals