no goals
α : Type u_1
β : Type u_2
xs : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
⊢ LazyList.bind (append xs ys) f = append (LazyList.bind xs f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
match xs with
| LazyList.nil => rfl
| LazyList.cons x xs =>
  simp only [append, Thunk.get, LazyList.bind]
  have := append_bind xs.get ys f
  simp only [Thunk.get] at this
  rw [this, append_assoc]
no goals
α : Type u_1
β : Type u_2
xs : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
⊢ LazyList.bind (append nil ys) f = append (LazyList.bind nil f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
rfl
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ LazyList.bind (append (cons x xs) ys) f =
    append (LazyList.bind (cons x xs) f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
simp only [append, Thunk.get, LazyList.bind]
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  LazyList.bind (append (Thunk.get xs) ys) f =
    append (LazyList.bind (Thunk.get xs) f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
have := append_bind xs.get ys f
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  LazyList.bind (append (Thunk.fn xs ()) ys) f =
    append (LazyList.bind (Thunk.fn xs ()) f) { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  LazyList.bind (append (Thunk.get xs) ys) f =
    append (LazyList.bind (Thunk.get xs) f) { fn := fun x => LazyList.bind (Thunk.get ys) f }
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
simp only [Thunk.get] at this
no goals
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  LazyList.bind (append (Thunk.fn xs ()) ys) f =
    append (LazyList.bind (Thunk.fn xs ()) f) { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
⊢ append (f x) { fn := fun x => LazyList.bind (append (Thunk.fn xs ()) ys) f } =
    append (append (f x) { fn := fun x => LazyList.bind (Thunk.fn xs ()) f })
      { fn := fun x => LazyList.bind (Thunk.fn ys ()) f }
rw [this, append_assoc]