Theorem: List.Index.bind_unbind (Extra/Index/Bind.lean)

State before:
α : Type u_1
β : Type u_2
f : α → List β
xs : List α
k : (xs.bind f).Index
⊢ bind f (unbind f k) = k
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  rw [unbind]
  split
  next h => rw [bind, append_inl, ←h, append_unappend]
  next h => rw [bind, append_inr, ih, ←h, append_unappend]
State after:
no goals

State before:
case nil
α : Type u_1
β : Type u_2
f : α → List β
k : ([].bind f).Index
⊢ bind f (unbind f k) = k
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
⊢ bind f (unbind f k) = k
Tactic:
rw [unbind]
State after:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
⊢ bind f
      (match k.unappend with
      | Sum.inl j => ⟨head, j⟩
      | Sum.inr k => ⟨(unbind f k).fst.tail, (unbind f k).snd⟩) =
    k

State before:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
⊢ bind f
      (match k.unappend with
      | Sum.inl j => ⟨head, j⟩
      | Sum.inr k => ⟨(unbind f k).fst.tail, (unbind f k).snd⟩) =
    k
Tactic:
split
State after:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
j✝ : (f x).Index
heq✝ : k.unappend = Sum.inl j✝
⊢ bind f ⟨head, j✝⟩ = k

case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k

State before:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
j✝ : (f x).Index
heq✝ : k.unappend = Sum.inl j✝
⊢ bind f ⟨head, j✝⟩ = k

case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Tactic:
next h => rw [bind, append_inl, ←h, append_unappend]
State after:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k

State before:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Tactic:
next h => rw [bind, append_inr, ih, ←h, append_unappend]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
j✝ : (f x).Index
h : k.unappend = Sum.inl j✝
⊢ bind f ⟨head, j✝⟩ = k
Tactic:
rw [bind, append_inl, ←h, append_unappend]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
h : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Tactic:
rw [bind, append_inr, ih, ←h, append_unappend]
State after:
no goals