case nil
α : Type u_1
ys zs : LazyList α
⊢ append (append nil { fn := fun x => ys }) { fn := fun x => zs } =
    append nil { fn := fun x => append ys { fn := fun x => zs } }

case cons
α : Type u_1
xs ys zs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.66098 tl✝
⊢ append (append (cons hd✝ tl✝) { fn := fun x => ys }) { fn := fun x => zs } =
    append (cons hd✝ tl✝) { fn := fun x => append ys { fn := fun x => zs } }

case mk
α : Type u_1
xs ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    append (append (fn✝ a) { fn := fun x => ys }) { fn := fun x => zs } =
      append (fn✝ a) { fn := fun x => append ys { fn := fun x => zs } }
⊢ ?m.66098 { fn := fn✝ }
α : Type u_1
xs ys zs : LazyList α
⊢ append (append xs { fn := fun x => ys }) { fn := fun x => zs } =
    append xs { fn := fun x => append ys { fn := fun x => zs } }
induction' xs using LazyList.rec with _ _ _ _ ih
no goals
case nil
α : Type u_1
ys zs : LazyList α
⊢ append (append nil { fn := fun x => ys }) { fn := fun x => zs } =
    append nil { fn := fun x => append ys { fn := fun x => zs } }
rfl
no goals
case cons
α : Type u_1
xs ys zs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.66098 tl✝
⊢ append (append (cons hd✝ tl✝) { fn := fun x => ys }) { fn := fun x => zs } =
    append (cons hd✝ tl✝) { fn := fun x => append ys { fn := fun x => zs } }
simpa only [append, cons.injEq, true_and]
case mk.eq
α : Type u_1
xs ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    append (append (fn✝ a) { fn := fun x => ys }) { fn := fun x => zs } =
      append (fn✝ a) { fn := fun x => append ys { fn := fun x => zs } }
⊢ Thunk.get
      {
        fn := fun x =>
          append (Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => ys } })
            { fn := fun x => zs } } =
    Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => append ys { fn := fun x => zs } } }
case mk
α : Type u_1
xs ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    append (append (fn✝ a) { fn := fun x => ys }) { fn := fun x => zs } =
      append (fn✝ a) { fn := fun x => append ys { fn := fun x => zs } }
⊢ {
      fn := fun x =>
        append (Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => ys } })
          { fn := fun x => zs } } =
    { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => append ys { fn := fun x => zs } } }
ext
no goals
case mk.eq
α : Type u_1
xs ys zs : LazyList α
fn✝ : Unit → LazyList α
ih :
  ∀ (a : Unit),
    append (append (fn✝ a) { fn := fun x => ys }) { fn := fun x => zs } =
      append (fn✝ a) { fn := fun x => append ys { fn := fun x => zs } }
⊢ Thunk.get
      {
        fn := fun x =>
          append (Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => ys } })
            { fn := fun x => zs } } =
    Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) { fn := fun x => append ys { fn := fun x => zs } } }
apply ih