case h.h.h.h
α : Type u_2
β : Type u_1
as : List α
f : α → List β
⊢ List.bind as f = bindTR as f
⊢ @List.bind = @bindTR
funext α β as f
case h.h.h.h
α : Type u_2
β : Type u_1
as : List α
f : α → List β
⊢ List.bind as f = bindTR as f
case h.h.h.h
α : Type u_2
β : Type u_1
as : List α
f : α → List β
⊢ List.bind as f = bindTR as f
let rec go : ∀ as acc, bindTR.go f as acc = acc.data ++ as.bind f
  | [], acc => by simp [bindTR.go, bind]
  | x::xs, acc => by simp [bindTR.go, bind, go xs]
no goals
case h.h.h.h
α : Type u_2
β : Type u_1
as : List α
f : α → List β
⊢ List.bind as f = bindTR as f
exact (go as #[]).symm
no goals
α : Type u_2
β : Type u_1
as : List α
f : α → List β
acc : Array β
⊢ bindTR.go f [] acc = acc.data ++ List.bind [] f
simp [bindTR.go, bind]
no goals
α : Type u_2
β : Type u_1
as : List α
f : α → List β
x : α
xs : List α
acc : Array β
⊢ bindTR.go f (x :: xs) acc = acc.data ++ List.bind (x :: xs) f
simp [bindTR.go, bind, go xs]