Theorem: List.Index.pi_unpi (Extra/Index/Pi.lean)

State before:
case nil
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f []).Index
⊢ pi k.unpi = k
Tactic:
cases k
State after:
case nil.head
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
⊢ pi head.unpi = head

case nil.tail
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
a✝ : [].Index
⊢ pi a✝.tail.unpi = a✝.tail

State before:
case nil.head
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
⊢ pi head.unpi = head
Tactic:
rfl
State after:
no goals

State before:
case nil.tail
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
a✝ : [].Index
⊢ pi a✝.tail.unpi = a✝.tail
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : 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 (x :: xs)).Index
⊢ pi k.unpi = k
Tactic:
match h : unbind _ k with
| ⟨k₁,k₂⟩ =>
  rw [unbind_eq_iff_eq_bind] at h
  cases h
  simp only [pi, unpi]
  rw [unbind_bind, ih, map_unmap]
State after:
no goals

State before:
α : 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 (x :: xs)).Index
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
h :
  unbind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      k =
    ⟨k₁, k₂⟩
⊢ pi k.unpi = k
Tactic:
rw [unbind_eq_iff_eq_bind] at h
State after:
α : 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 (x :: xs)).Index
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
h :
  k =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
⊢ pi k.unpi = k

State before:
α : 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 (x :: xs)).Index
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
h :
  k =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
⊢ pi k.unpi = k
Tactic:
cases h
State after:
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
⊢ pi
      (bind
          (fun ys =>
            List.map
              (fun y i =>
                match i with
                | head => y
                | i.tail => ys i)
              (f x))
          ⟨k₁, k₂⟩).unpi =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩

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
⊢ pi
      (bind
          (fun ys =>
            List.map
              (fun y i =>
                match i with
                | head => y
                | i.tail => ys i)
              (f x))
          ⟨k₁, k₂⟩).unpi =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
Tactic:
simp only [pi, unpi]
State after:
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₂⟩

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]
State after:
no goals