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

State before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
⊢ (pi h).unpi = h
Tactic:
funext i
State after:
case h
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
i : xs.Index
⊢ (pi h).unpi i = h i

State before:
case h
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
i : xs.Index
⊢ (pi h).unpi i = h i
Tactic:
induction i with
| head => simp only [pi, unpi]; rw [unbind_bind, unmap_map]
| tail i ih => simp only [pi, unpi]; rw [unbind_bind, ih]
State after:
no goals

State before:
case h.head
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
x✝ : α
xs✝ : List α
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (pi h).unpi head = h head
Tactic:
simp only [pi, unpi]
State after:
case h.head
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
x✝ : α
xs✝ : List α
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ 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✝))
                    ⟨pi fun i => h i.tail,
                      map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => (pi fun i => h i.tail).val i)
                        (h head)⟩)).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✝))
            ⟨pi fun i => h i.tail,
              map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => (pi fun i => h i.tail).val i)
                (h head)⟩)).snd =
    h head

State before:
case h.head
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
x✝ : α
xs✝ : List α
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ 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✝))
                    ⟨pi fun i => h i.tail,
                      map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => (pi fun i => h i.tail).val i)
                        (h head)⟩)).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✝))
            ⟨pi fun i => h i.tail,
              map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => (pi fun i => h i.tail).val i)
                (h head)⟩)).snd =
    h head
Tactic:
rw [unbind_bind, unmap_map]
State after:
no goals

State before:
case h.tail
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : ∀ (h : (i : xs✝.Index) → (f i.val).Index), (pi h).unpi i = h i
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (pi h).unpi i.tail = h i.tail
Tactic:
simp only [pi, unpi]
State after:
case h.tail
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : ∀ (h : (i : xs✝.Index) → (f i.val).Index), (pi h).unpi i = h i
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (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✝))
              ⟨pi fun i => h i.tail,
                map
                  (fun y i =>
                    match i with
                    | head => y
                    | i.tail => (pi fun i => h i.tail).val i)
                  (h head)⟩)).fst.unpi
      i =
    h i.tail

State before:
case h.tail
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : ∀ (h : (i : xs✝.Index) → (f i.val).Index), (pi h).unpi i = h i
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (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✝))
              ⟨pi fun i => h i.tail,
                map
                  (fun y i =>
                    match i with
                    | head => y
                    | i.tail => (pi fun i => h i.tail).val i)
                  (h head)⟩)).fst.unpi
      i =
    h i.tail
Tactic:
rw [unbind_bind, ih]
State after:
no goals