[GOAL]
α : Type u_1
⊢ LeftInverse toList ofList
[PROOFSTEP]
intro xs
[GOAL]
α : Type u_1
xs : List α
⊢ toList (ofList xs) = xs
[PROOFSTEP]
induction xs
[GOAL]
case nil
α : Type u_1
⊢ toList (ofList []) = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : toList (ofList tail✝) = tail✝
⊢ toList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
[PROOFSTEP]
simpa [ofList, toList]
[GOAL]
α : Type u_1
⊢ Function.RightInverse toList ofList
[PROOFSTEP]
intro xs
[GOAL]
α : Type u_1
xs : LazyList α
⊢ ofList (toList xs) = xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α : Type u_1
⊢ ofList (toList nil) = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.1024 tl✝
⊢ ofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝
[PROOFSTEP]
simpa only [toList, ofList, cons.injEq, true_and]
[GOAL]
case mk
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a
⊢ { fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }
[PROOFSTEP]
rw [Thunk.get, ih]
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
⊢ Decidable (cons x xs = cons y ys)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
⊢ ¬cons x xs = cons y ys
[PROOFSTEP]
simp only [cons.injEq, not_and]
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
⊢ x = y → ¬xs = ys
[PROOFSTEP]
intro _ xs_ys
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
a✝ : x = y
xs_ys : xs = ys
⊢ False
[PROOFSTEP]
apply h2
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : ¬Thunk.get xs = Thunk.get ys
a✝ : x = y
xs_ys : xs = ys
⊢ Thunk.get xs = Thunk.get ys
[PROOFSTEP]
rw [xs_ys]
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ Decidable (cons x xs = cons y ys)
[PROOFSTEP]
apply isTrue
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ cons x xs = cons y ys
[PROOFSTEP]
congr
[GOAL]
case h.e_tl
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ xs = ys
[PROOFSTEP]
ext
[GOAL]
case h.e_tl.eq
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : x = y
h2 : Thunk.get xs = Thunk.get ys
⊢ Thunk.get xs = Thunk.get ys
[PROOFSTEP]
exact h2
[GOAL]
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ Decidable (cons x xs = cons y ys)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ ¬cons x xs = cons y ys
[PROOFSTEP]
simp only [cons.injEq, not_and]
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ x = y → ¬xs = ys
[PROOFSTEP]
intro
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
x : α
xs : Thunk (LazyList α)
y : α
ys : Thunk (LazyList α)
h : ¬x = y
a✝ : x = y
⊢ ¬xs = ys
[PROOFSTEP]
contradiction
[GOAL]
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ Decidable (nil = cons hd✝ tl✝)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ ¬nil = cons hd✝ tl✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ Decidable (cons hd✝ tl✝ = nil)
[PROOFSTEP]
apply isFalse
[GOAL]
case h
α : Type u
inst✝ : DecidableEq α
hd✝ : α
tl✝ : Thunk (LazyList α)
⊢ ¬cons hd✝ tl✝ = nil
[PROOFSTEP]
simp
[GOAL]
⊢ LawfulTraversable LazyList
[PROOFSTEP]
apply Equiv.isLawfulTraversable' listEquivLazyList
[GOAL]
case h₀
⊢ ∀ {α β : Type ?u.19468} (f : α → β), Functor.map f = Equiv.map listEquivLazyList f
[PROOFSTEP]
intros
[GOAL]
case h₁
⊢ ∀ {α β : Type ?u.19468} (f : β), Functor.mapConst f = (Equiv.map listEquivLazyList ∘ const α) f
[PROOFSTEP]
intros
[GOAL]
case h₂
⊢ ∀ {F : Type ?u.19468 → Type ?u.19468} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type ?u.19468}
    (f : α → F β), traverse f = Equiv.traverse listEquivLazyList f
[PROOFSTEP]
intros
[GOAL]
case h₀
α✝ β✝ : Type ?u.19468
f✝ : α✝ → β✝
⊢ Functor.map f✝ = Equiv.map listEquivLazyList f✝
[PROOFSTEP]
ext
[GOAL]
case h₁
α✝ β✝ : Type ?u.19468
f✝ : β✝
⊢ Functor.mapConst f✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝
[PROOFSTEP]
ext
[GOAL]
case h₂
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f✝ : α✝ → F✝ β✝
⊢ traverse f✝ = Equiv.traverse listEquivLazyList f✝
[PROOFSTEP]
ext
[GOAL]
case h₀.h
α✝ β✝ : Type ?u.19468
f✝ : α✝ → β✝
x✝ : LazyList α✝
⊢ f✝ <$> x✝ = Equiv.map listEquivLazyList f✝ x✝
[PROOFSTEP]
rename_i f xs
[GOAL]
case h₁.h
α✝ β✝ : Type ?u.19468
f✝ : β✝
x✝ : LazyList α✝
⊢ Functor.mapConst f✝ x✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝ x✝
[PROOFSTEP]
rename_i f xs
[GOAL]
case h₂.h
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f✝ : α✝ → F✝ β✝
x✝ : LazyList α✝
⊢ traverse f✝ x✝ = Equiv.traverse listEquivLazyList f✝ x✝
[PROOFSTEP]
rename_i f xs
[GOAL]
case h₀.h
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
⊢ f <$> xs = Equiv.map listEquivLazyList f xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case h₀.h.nil
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
⊢ f <$> nil = Equiv.map listEquivLazyList f nil
[PROOFSTEP]
rfl
[GOAL]
case h₀.h.cons
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.19696 tl✝
⊢ f <$> cons hd✝ tl✝ = Equiv.map listEquivLazyList f (cons hd✝ tl✝)
[PROOFSTEP]
simpa only [Equiv.map, Functor.map, listEquivLazyList, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, LazyList.traverse,
  Seq.seq, toList, ofList, cons.injEq, true_and]
[GOAL]
case h₀.h.mk
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)
⊢ Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ })) =
    { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) }
[PROOFSTEP]
ext
[GOAL]
case h₀.h.mk.eq
α✝ β✝ : Type ?u.19468
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)
⊢ Thunk.get (Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) =
    Thunk.get { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) }
[PROOFSTEP]
apply ih
[GOAL]
case h₁.h
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
⊢ Functor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs
[PROOFSTEP]
simp only [Equiv.map, listEquivLazyList, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, comp, Functor.mapConst]
[GOAL]
case h₁.h
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
⊢ LazyList.traverse (const α✝ f) xs = ofList (const α✝ f <$> toList xs)
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case h₁.h.nil
α✝ β✝ : Type ?u.19468
f : β✝
⊢ LazyList.traverse (const α✝ f) nil = ofList (const α✝ f <$> toList nil)
[PROOFSTEP]
rfl
[GOAL]
case h₁.h.cons
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.21260 tl✝
⊢ LazyList.traverse (const α✝ f) (cons hd✝ tl✝) = ofList (const α✝ f <$> toList (cons hd✝ tl✝))
[PROOFSTEP]
simpa only [toList, ofList, LazyList.traverse, Seq.seq, Functor.map, cons.injEq, true_and]
[GOAL]
case h₁.h.mk
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))
⊢ Thunk.pure (LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ })) =
    { fn := fun x => ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ }))) }
[PROOFSTEP]
congr
[GOAL]
case h₁.h.mk.e_a
α✝ β✝ : Type ?u.19468
f : β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))
⊢ LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ }) =
    ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ })))
[PROOFSTEP]
apply ih
[GOAL]
case h₂.h
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
⊢ traverse f xs = Equiv.traverse listEquivLazyList f xs
[PROOFSTEP]
simp only [traverse, Equiv.traverse, listEquivLazyList, Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk]
[GOAL]
case h₂.h
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
⊢ LazyList.traverse f xs = ofList <$> List.traverse f (toList xs)
[PROOFSTEP]
induction' xs using LazyList.rec with _ tl ih _ ih
[GOAL]
case h₂.h.nil
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
⊢ LazyList.traverse f nil = ofList <$> List.traverse f (toList nil)
[PROOFSTEP]
simp only [List.traverse, map_pure]
[GOAL]
case h₂.h.nil
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
⊢ LazyList.traverse f nil = pure (ofList [])
[PROOFSTEP]
rfl
[GOAL]
case h₂.h.cons
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
hd✝ : α✝
tl : Thunk (LazyList α✝)
ih : ?m.22684 tl
⊢ LazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
[PROOFSTEP]
have : tl.get.traverse f = ofList <$> tl.get.toList.traverse f := ih
[GOAL]
case h₂.h.cons
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
hd✝ : α✝
tl : Thunk (LazyList α✝)
ih this : LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))
⊢ LazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
[PROOFSTEP]
simp only [traverse._eq_2, ih, Functor.map_map, seq_map_assoc, toList, List.traverse, map_seq]
[GOAL]
case h₂.h.cons
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
hd✝ : α✝
tl : Thunk (LazyList α✝)
ih this : LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))
⊢ (Seq.seq (((fun x => x ∘ Thunk.pure ∘ ofList) ∘ cons) <$> f hd✝) fun x => List.traverse f (toList (Thunk.get tl))) =
    Seq.seq (((fun x => ofList ∘ x) ∘ List.cons) <$> f hd✝) fun x => List.traverse f (toList (Thunk.get tl))
[PROOFSTEP]
rfl
[GOAL]
case h₂.h.mk
F✝ : Type ?u.19468 → Type ?u.19468
inst✝¹ : Applicative F✝
inst✝ : LawfulApplicative F✝
α✝ β✝ : Type ?u.19468
f : α✝ → F✝ β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))
⊢ LazyList.traverse f (Thunk.get { fn := fn✝ }) = ofList <$> List.traverse f (toList (Thunk.get { fn := fn✝ }))
[PROOFSTEP]
apply ih
[GOAL]
α : Type u_1
xs : LazyList α
⊢ append xs (Thunk.pure nil) = xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α : Type u_1
⊢ append nil (Thunk.pure nil) = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
xs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.62141 tl✝
⊢ append (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝
[PROOFSTEP]
simpa only [append, cons.injEq, true_and]
[GOAL]
case mk
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α : Type u_1
xs : LazyList α
fn✝ : Unit → LazyList α
ih : ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a
⊢ Thunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ }
[PROOFSTEP]
apply ih
[GOAL]
α : 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 } }
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
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 } }
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
xs ys zs : LazyList α
hd✝ : α
tl✝ : Thunk (LazyList α)
tl_ih✝ : ?m.65384 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 } }
[PROOFSTEP]
simpa only [append, cons.injEq, true_and]
[GOAL]
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 } } }
[PROOFSTEP]
ext
[GOAL]
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 } } }
[PROOFSTEP]
apply ih
[GOAL]
α : 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 }
[PROOFSTEP]
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]
[GOAL]
α : 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 }
[PROOFSTEP]
rfl
[GOAL]
α : 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 }
[PROOFSTEP]
simp only [append, Thunk.get, LazyList.bind]
[GOAL]
α : 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 }
[PROOFSTEP]
have := append_bind xs.get ys f
[GOAL]
α : 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 }
[PROOFSTEP]
simp only [Thunk.get] at this 
[GOAL]
α : 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 }
[PROOFSTEP]
rw [this, append_assoc]
[GOAL]
⊢ ∀ {α : Type ?u.75696} (x : LazyList α), id <$> x = x
[PROOFSTEP]
intro _ xs
[GOAL]
α✝ : Type ?u.75696
xs : LazyList α✝
⊢ id <$> xs = xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α✝ : Type ?u.75696
⊢ id <$> nil = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ : Type ?u.75696
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.75815 tl✝
⊢ id <$> cons hd✝ tl✝ = cons hd✝ tl✝
[PROOFSTEP]
simpa only [Functor.map, traverse._eq_2, id_eq, Id.map_eq, Seq.seq, cons.injEq, true_and]
[GOAL]
case mk
α✝ : Type ?u.75696
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), id <$> fn✝ a = fn✝ a
⊢ Thunk.pure (LazyList.traverse id (Thunk.get { fn := fn✝ })) = { fn := fn✝ }
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α✝ : Type ?u.75696
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), id <$> fn✝ a = fn✝ a
⊢ Thunk.get (Thunk.pure (LazyList.traverse id (Thunk.get { fn := fn✝ }))) = Thunk.get { fn := fn✝ }
[PROOFSTEP]
apply ih
[GOAL]
⊢ ∀ {α β : Type ?u.75696} (x : α) (f : α → LazyList β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
α✝ β✝ : Type ?u.75696
x✝ : α✝
f✝ : α✝ → LazyList β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
simp only [bind, pure, singleton, LazyList.bind]
[GOAL]
α✝ β✝ : Type ?u.75696
x✝ : α✝
f✝ : α✝ → LazyList β✝
⊢ append (f✝ x✝) { fn := fun x => LazyList.bind (Thunk.get (Thunk.pure nil)) f✝ } = f✝ x✝
[PROOFSTEP]
apply append_nil
[GOAL]
⊢ ∀ {α β γ : Type ?u.75696} (x : LazyList α) (f : α → LazyList β) (g : β → LazyList γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intro _ _ _ xs _ _
[GOAL]
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
⊢ xs >>= f✝ >>= g✝ = xs >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α✝ β✝ γ✝ : Type ?u.75696
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
⊢ nil >>= f✝ >>= g✝ = nil >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.76333 tl✝
⊢ cons hd✝ tl✝ >>= f✝ >>= g✝ = cons hd✝ tl✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
simp only [bind, LazyList.bind, append_bind]
[GOAL]
case cons
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.76333 tl✝
⊢ append (LazyList.bind (f✝ hd✝) g✝)
      { fn := fun x => LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get tl✝) f✝ }) g✝ } =
    append (LazyList.bind (f✝ hd✝) g✝) { fn := fun x => LazyList.bind (Thunk.get tl✝) fun x => LazyList.bind (f✝ x) g✝ }
[PROOFSTEP]
congr
[GOAL]
case mk
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), fn✝ a >>= f✝ >>= g✝ = fn✝ a >>= fun x => f✝ x >>= g✝
⊢ { fn := fun x => LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) f✝ }) g✝ } =
    { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) fun x => LazyList.bind (f✝ x) g✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.e_fn
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), fn✝ a >>= f✝ >>= g✝ = fn✝ a >>= fun x => f✝ x >>= g✝
⊢ (fun x => LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) f✝ }) g✝) = fun x =>
    LazyList.bind (Thunk.get { fn := fn✝ }) fun x => LazyList.bind (f✝ x) g✝
[PROOFSTEP]
funext
[GOAL]
case mk.e_fn.h
α✝ β✝ γ✝ : Type ?u.75696
xs : LazyList α✝
f✝ : α✝ → LazyList β✝
g✝ : β✝ → LazyList γ✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), fn✝ a >>= f✝ >>= g✝ = fn✝ a >>= fun x => f✝ x >>= g✝
x✝ : Unit
⊢ LazyList.bind (Thunk.get { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) f✝ }) g✝ =
    LazyList.bind (Thunk.get { fn := fn✝ }) fun x => LazyList.bind (f✝ x) g✝
[PROOFSTEP]
apply ih
[GOAL]
⊢ ∀ {α β : Type ?u.75696} (f : α → β) (x : LazyList α),
    (do
        let y ← x
        pure (f y)) =
      f <$> x
[PROOFSTEP]
intro _ _ f xs
[GOAL]
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
⊢ (do
      let y ← xs
      pure (f y)) =
    f <$> xs
[PROOFSTEP]
simp only [bind, Functor.map, pure, singleton]
[GOAL]
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
⊢ (LazyList.bind xs fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f xs
[PROOFSTEP]
induction' xs using LazyList.rec with _ _ _ _ ih
[GOAL]
case nil
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
⊢ (LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.77095 tl✝
⊢ (LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝)
[PROOFSTEP]
simp only [bind._eq_2, append, traverse._eq_2, Id.map_eq, cons.injEq, true_and]
[GOAL]
case cons
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
hd✝ : α✝
tl✝ : Thunk (LazyList α✝)
tl_ih✝ : ?m.77095 tl✝
⊢ cons (f hd✝)
      {
        fn := fun x =>
          append (Thunk.get (Thunk.pure nil))
            { fn := fun x => LazyList.bind (Thunk.get tl✝) fun y => cons (f y) (Thunk.pure nil) } } =
    Seq.seq (cons (f hd✝)) fun x => Thunk.pure (LazyList.traverse f (Thunk.get tl✝))
[PROOFSTEP]
congr
[GOAL]
case mk
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), (LazyList.bind (fn✝ a) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (fn✝ a)
⊢ {
      fn := fun x =>
        append (Thunk.get (Thunk.pure nil))
          { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) fun y => cons (f y) (Thunk.pure nil) } } =
    (fun x => Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) ()
[PROOFSTEP]
ext
[GOAL]
case mk.eq
α✝ β✝ : Type ?u.75696
f : α✝ → β✝
xs : LazyList α✝
fn✝ : Unit → LazyList α✝
ih : ∀ (a : Unit), (LazyList.bind (fn✝ a) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (fn✝ a)
⊢ Thunk.get
      {
        fn := fun x =>
          append (Thunk.get (Thunk.pure nil))
            { fn := fun x => LazyList.bind (Thunk.get { fn := fn✝ }) fun y => cons (f y) (Thunk.pure nil) } } =
    Thunk.get ((fun x => Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) ())
[PROOFSTEP]
apply ih
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x : α
⊢ Decidable (x ∈ nil)
[PROOFSTEP]
apply Decidable.isFalse
[GOAL]
case h
α : Type ?u.93639
inst✝ : DecidableEq α
x : α
⊢ ¬x ∈ nil
[PROOFSTEP]
simp [Membership.mem, LazyList.Mem]
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : x = y
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
apply Decidable.isTrue
[GOAL]
case h
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : x = y
⊢ x ∈ cons y ys
[PROOFSTEP]
simp only [Membership.mem, LazyList.Mem]
[GOAL]
case h
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : x = y
⊢ x = y ∨ LazyList.Mem x (Thunk.get ys)
[PROOFSTEP]
exact Or.inl h
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
have := Mem.decidable x ys.get
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
this : Decidable (x ∈ Thunk.get ys)
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
have : (x ∈ ys.get) ↔ (x ∈ cons y ys) := by simp [(· ∈ ·), LazyList.Mem, h]
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
this : Decidable (x ∈ Thunk.get ys)
⊢ x ∈ Thunk.get ys ↔ x ∈ cons y ys
[PROOFSTEP]
simp [(· ∈ ·), LazyList.Mem, h]
[GOAL]
α : Type ?u.93639
inst✝ : DecidableEq α
x y : α
ys : Thunk (LazyList α)
h : ¬x = y
this✝ : Decidable (x ∈ Thunk.get ys)
this : x ∈ Thunk.get ys ↔ x ∈ cons y ys
⊢ Decidable (x ∈ cons y ys)
[PROOFSTEP]
exact decidable_of_decidable_of_iff this
[GOAL]
α : Type u_1
x y : α
ys : Thunk (LazyList α)
⊢ x ∈ cons y ys ↔ x = y ∨ x ∈ Thunk.get ys
[PROOFSTEP]
simp [Membership.mem, LazyList.Mem]
[GOAL]
α : Type u_1
p : α → Prop
a : α
l : Thunk (LazyList α)
⊢ (∀ (x : α), x ∈ cons a l → p x) ↔ p a ∧ ∀ (x : α), x ∈ Thunk.get l → p x
[PROOFSTEP]
simp only [Membership.mem, LazyList.Mem, or_imp, forall_and, forall_eq]
