-- Mathlib/.lake/packages/batteries/Batteries/Data/LazyList.lean
theorem append_bind {α β} (xs : LazyList α) (ys : Thunk (LazyList α)) (f : α → LazyList β) :
    (xs.append ys).bind f = (xs.bind f).append (ys.get.bind f)

Proof state:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ ((cons x xs).append ys).bind f = ((cons x xs).bind f).append { fn := fun x => ys.get.bind f }

Tactic:
simp only [append, Thunk.get, LazyList.bind]

Result:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ (f x).append { fn := fun x => ((Thunk.fn✝ xs ()).append ys).bind f } =
    ((f x).append { fn := fun x => (Thunk.fn✝ xs ()).bind f }).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }

Proof state:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this : (xs.get.append ys).bind f = (xs.get.bind f).append { fn := fun x => ys.get.bind f }
⊢ (f x).append { fn := fun x => ((Thunk.fn✝ xs ()).append ys).bind f } =
    ((f x).append { fn := fun x => (Thunk.fn✝ xs ()).bind f }).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }

Tactic:
simp only [Thunk.get] at this

Result:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  ((Thunk.fn✝ xs ()).append ys).bind f = ((Thunk.fn✝ xs ()).bind f).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }
⊢ (f x).append { fn := fun x => ((Thunk.fn✝ xs ()).append ys).bind f } =
    ((f x).append { fn := fun x => (Thunk.fn✝ xs ()).bind f }).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }

Proof state:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this :
  ((Thunk.fn✝ xs ()).append ys).bind f = ((Thunk.fn✝ xs ()).bind f).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }
⊢ (f x).append { fn := fun x => ((Thunk.fn✝ xs ()).append ys).bind f } =
    ((f x).append { fn := fun x => (Thunk.fn✝ xs ()).bind f }).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }

Tactic:
rw [this, append_assoc]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
⊢ (f x).append { fn := fun x => ((Thunk.fn✝ xs ()).append ys).bind f } =
    ((f x).append { fn := fun x => (Thunk.fn✝ xs ()).bind f }).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }

Tactic:
have := append_bind xs.get ys f

Result:
α : Type u_1
β : Type u_2
xs✝ : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
x : α
xs : Thunk (LazyList α)
this : (xs.get.append ys).bind f = (xs.get.bind f).append { fn := fun x => ys.get.bind f }
⊢ (f x).append { fn := fun x => ((Thunk.fn✝ xs ()).append ys).bind f } =
    ((f x).append { fn := fun x => (Thunk.fn✝ xs ()).bind f }).append { fn := fun x => (Thunk.fn✝ ys ()).bind f }

Proof state:
α : Type u_1
β : Type u_2
xs : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
⊢ (nil.append ys).bind f = (nil.bind f).append { fn := fun x => ys.get.bind f }

Tactic:
simp only [append, Thunk.get, LazyList.bind]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
xs : LazyList α
ys : Thunk (LazyList α)
f : α → LazyList β
⊢ (xs.append ys).bind f = (xs.bind f).append { fn := fun x => ys.get.bind f }

Tactic:
match xs with
| LazyList.nil =>
  simp only [append, Thunk.get, LazyList.bind]
| 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]

Result:
no goals