/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon

! This file was ported from Lean 3 source module data.lazy_list.basic
! leanprover-community/mathlib commit 1f0096e6caa61e9c849ec2adbd227e960e9dff58
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Control.Traversable.Equiv
import Mathlib.Control.Traversable.Instances
import Mathlib.Data.LazyList

/-!
## Definitions on lazy lists

This file contains various definitions and proofs on lazy lists.

TODO: move the `LazyList.lean` file from core to mathlib.
-/


universe u

namespace Thunk

-- Porting note: `Thunk.pure` appears to do the same thing.
#align thunk.mk Thunk.pure: {α : Type u_1} → α → Thunk α
Thunk.pure

-- Porting note: Added `Thunk.ext` to get `ext` tactic to work.
@[ext]
theorem ext: ∀ {α : Type u} {a b : Thunk α}, Thunk.get a = Thunk.get b → a = b
ext {α: Type u
α : Type u: Type (u+1)
Type u} {a: Thunk α
a b: Thunk α
b : Thunk: Type ?u.7 → Type ?u.7
Thunk α: Type u
α} (eq: Thunk.get a = Thunk.get b
eq : a: Thunk α
a.get: {α : Type ?u.11} → Thunk α → α
get = b: Thunk α
b.get: {α : Type ?u.16} → Thunk α → α
get) : a: Thunk α
a = b: Thunk α
b := by
Goals accomplished! 🐙
  α: Type u

a, b: Thunk α

eq: Thunk.get a = Thunk.get b

a = bhave ⟨_⟩ := a: Thunk α
aα: Type u

a, b: Thunk α

fn✝: Unit → α

eq: Thunk.get { fn := fn✝ } = Thunk.get b

{ fn := fn✝ } = b
  α: Type u

a, b: Thunk α

eq: Thunk.get a = Thunk.get b

a = bhave ⟨_⟩ := b: Thunk α
bα: Type u

a, b: Thunk α

fn✝¹, fn✝: Unit → α

eq: Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }

{ fn := fn✝¹ } = { fn := fn✝ }
  α: Type u

a, b: Thunk α

eq: Thunk.get a = Thunk.get b

a = bcongrα: Type u

a, b: Thunk α

fn✝¹, fn✝: Unit → α

eq: Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }

e_fnfn✝¹ = fn✝
  α: Type u

a, b: Thunk α

eq: Thunk.get a = Thunk.get b

a = bexact funext: ∀ {α : Sort ?u.385} {β : α → Sort ?u.384} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun _: ?m.396
_ ↦ eq: Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }
eq
Goals accomplished! 🐙

instance: {α : Type u} → [inst : DecidableEq α] → DecidableEq (Thunk α)
instance {α: Type u
α : Type u: Type (u+1)
Type u} [DecidableEq: Sort ?u.432 → Sort (max1?u.432)
DecidableEq α: Type u
α] : DecidableEq: Sort ?u.441 → Sort (max1?u.441)
DecidableEq (Thunk: Type ?u.442 → Type ?u.442
Thunk α: Type u
α) := by
Goals accomplished! 🐙
  α: Type u

inst✝: DecidableEq α

DecidableEq (Thunk α)intro a: Thunk α
a b: Thunk α
bα: Type u

inst✝: DecidableEq α

a, b: Thunk α

Decidable (a = b)
  α: Type u

inst✝: DecidableEq α

DecidableEq (Thunk α)have : a: Thunk α
a = b: Thunk α
b ↔ a: Thunk α
a.get: {α : Type ?u.466} → Thunk α → α
get = b: Thunk α
b.get: {α : Type ?u.471} → Thunk α → α
get := ⟨α: Type u

inst✝: DecidableEq α

a, b: Thunk α

Decidable (a = b)by
Goals accomplished! 🐙 α: Type u

inst✝: DecidableEq α

a, b: Thunk α

a = b → Thunk.get a = Thunk.get bintro x: a = b
xα: Type u

inst✝: DecidableEq α

a, b: Thunk α

x: a = b

Thunk.get a = Thunk.get b;α: Type u

inst✝: DecidableEq α

a, b: Thunk α

x: a = b

Thunk.get a = Thunk.get b α: Type u

inst✝: DecidableEq α

a, b: Thunk α

a = b → Thunk.get a = Thunk.get brw [α: Type u

inst✝: DecidableEq α

a, b: Thunk α

x: a = b

Thunk.get a = Thunk.get bx: a = b
xα: Type u

inst✝: DecidableEq α

a, b: Thunk α

x: a = b

Thunk.get b = Thunk.get b]
Goals accomplished! 🐙, α: Type u

inst✝: DecidableEq α

a, b: Thunk α

Decidable (a = b)by
Goals accomplished! 🐙 α: Type u

inst✝: DecidableEq α

a, b: Thunk α

Thunk.get a = Thunk.get b → a = bintroα: Type u

inst✝: DecidableEq α

a, b: Thunk α

a✝: Thunk.get a = Thunk.get b

a = b;α: Type u

inst✝: DecidableEq α

a, b: Thunk α

a✝: Thunk.get a = Thunk.get b

a = b α: Type u

inst✝: DecidableEq α

a, b: Thunk α

Thunk.get a = Thunk.get b → a = bextα: Type u

inst✝: DecidableEq α

a, b: Thunk α

a✝: Thunk.get a = Thunk.get b

eqThunk.get a = Thunk.get b;α: Type u

inst✝: DecidableEq α

a, b: Thunk α

a✝: Thunk.get a = Thunk.get b

eqThunk.get a = Thunk.get b α: Type u

inst✝: DecidableEq α

a, b: Thunk α

Thunk.get a = Thunk.get b → a = bassumption
Goals accomplished! 🐙⟩α: Type u

inst✝: DecidableEq α

a, b: Thunk α

this: a = b ↔ Thunk.get a = Thunk.get b

Decidable (a = b)
  α: Type u

inst✝: DecidableEq α

DecidableEq (Thunk α)rw [α: Type u

inst✝: DecidableEq α

a, b: Thunk α

this: a = b ↔ Thunk.get a = Thunk.get b

Decidable (a = b)this: a = b ↔ Thunk.get a = Thunk.get b
thisα: Type u

inst✝: DecidableEq α

a, b: Thunk α

this: a = b ↔ Thunk.get a = Thunk.get b

Decidable (Thunk.get a = Thunk.get b)]α: Type u

inst✝: DecidableEq α

a, b: Thunk α

this: a = b ↔ Thunk.get a = Thunk.get b

Decidable (Thunk.get a = Thunk.get b)
  α: Type u

inst✝: DecidableEq α

DecidableEq (Thunk α)infer_instance
Goals accomplished! 🐙

end Thunk

namespace LazyList

open Function

/-- Isomorphism between strict and lazy lists. -/
def listEquivLazyList: (α : Type u_1) → List α ≃ LazyList α
listEquivLazyList (α: Type ?u.652
α : Type _: Type (?u.652+1)
Type _) : List: Type ?u.657 → Type ?u.657
List α: Type ?u.652
α ≃ LazyList: Type ?u.658 → Type ?u.658
LazyList α: Type ?u.652
α where
  toFun := LazyList.ofList: {α : Type ?u.667} → List α → LazyList α
LazyList.ofList
  invFun := LazyList.toList: {α : Type ?u.674} → LazyList α → List α
LazyList.toList
  right_inv := by
Goals accomplished! 🐙
    α: Type ?u.652

Function.RightInverse toList ofListintro xs: LazyList α
xsα: Type ?u.652

xs: LazyList α

ofList (toList xs) = xs
    α: Type ?u.652

Function.RightInverse toList ofListinduction' xs: LazyList α
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.1677 (fn✝ a)
ihα: Type ?u.652

nilofList (toList nil) = nil
α: Type ?u.652

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.1678 tl✝

consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝
α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk?m.1678 { fn := fn✝ }
    α: Type ?u.652

Function.RightInverse toList ofList·α: Type ?u.652

nilofList (toList nil) = nil α: Type ?u.652

nilofList (toList nil) = nil
α: Type ?u.652

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.1678 tl✝

consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝
α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk?m.1678 { fn := fn✝ }rfl
Goals accomplished! 🐙
    α: Type ?u.652

Function.RightInverse toList ofList·α: Type ?u.652

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.1678 tl✝

consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝ α: Type ?u.652

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.1678 tl✝

consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝
α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk?m.1678 { fn := fn✝ }simpa only [toList: {α : Type ?u.1731} → LazyList α → List α
toList, ofList: {α : Type ?u.1741} → List α → LazyList α
ofList, cons.injEq: ∀ {α : Type ?u.1757} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]
Goals accomplished! 🐙
    α: Type ?u.652

Function.RightInverse toList ofList·α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ } α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }rw [α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }Thunk.get: {α : Type ?u.1888} → Thunk α → α
Thunk.get,α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk{ fn := fun x => ofList (toList (Thunk.fn { fn := fn✝ } ())) } = { fn := fn✝ } α: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }ih: ∀ (a : Unit), ?m.1677 (fn✝ a)
ihα: Type ?u.652

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ a

mk{ fn := fun x => fn✝ () } = { fn := fn✝ }]
Goals accomplished! 🐙
  left_inv := by
Goals accomplished! 🐙
    α: Type ?u.652

LeftInverse toList ofListintro xs: List α
xsα: Type ?u.652

xs: List α

toList (ofList xs) = xs
    α: Type ?u.652

LeftInverse toList ofListinduction xs: List α
xsα: Type ?u.652

niltoList (ofList []) = []
α: Type ?u.652

head✝: α

tail✝: List α

tail_ih✝: toList (ofList tail✝) = tail✝

constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
    α: Type ?u.652

LeftInverse toList ofList·α: Type ?u.652

niltoList (ofList []) = [] α: Type ?u.652

niltoList (ofList []) = []
α: Type ?u.652

head✝: α

tail✝: List α

tail_ih✝: toList (ofList tail✝) = tail✝

constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝rfl
Goals accomplished! 🐙
    α: Type ?u.652

LeftInverse toList ofList·α: Type ?u.652

head✝: α

tail✝: List α

tail_ih✝: toList (ofList tail✝) = tail✝

constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝ α: Type ?u.652

head✝: α

tail✝: List α

tail_ih✝: toList (ofList tail✝) = tail✝

constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝simpa [ofList: {α : Type ?u.742} → List α → LazyList α
ofList, toList: {α : Type ?u.1018} → LazyList α → List α
toList]
Goals accomplished! 🐙
#align lazy_list.list_equiv_lazy_list LazyList.listEquivLazyList: (α : Type u_1) → List α ≃ LazyList α
LazyList.listEquivLazyList

-- Porting note: Added a name to make the recursion work.
instance decidableEq: {α : Type u} → [inst : DecidableEq α] → DecidableEq (LazyList α)
decidableEq {α: Type u
α : Type u: Type (u+1)
Type u} [DecidableEq: Sort ?u.2006 → Sort (max1?u.2006)
DecidableEq α: Type u
α] : DecidableEq: Sort ?u.2015 → Sort (max1?u.2015)
DecidableEq (LazyList: Type ?u.2016 → Type ?u.2016
LazyList α: Type u
α)
  | nil: {α : Type ?u.2035} → LazyList α
nil, nil: {α : Type ?u.2038} → LazyList α
nil => isTrue: {p : Prop} → p → Decidable p
isTrue rfl: ∀ {α : Sort ?u.2056} {a : α}, a = a
rfl
  | cons: {α : Type ?u.2062} → α → Thunk (LazyList α) → LazyList α
cons x: α
x xs: Thunk (LazyList α)
xs, cons: {α : Type ?u.2066} → α → Thunk (LazyList α) → LazyList α
cons y: α
y ys: Thunk (LazyList α)
ys =>
    if h: ?m.2121
h : x: α
x = y: α
y then
      match decidableEq: {α : Type u} → [inst : DecidableEq α] → DecidableEq (LazyList α)
decidableEq xs: Thunk (LazyList α)
xs.get: {α : Type ?u.2125} → Thunk α → α
get ys: Thunk (LazyList α)
ys.get: {α : Type ?u.2129} → Thunk α → α
get with
      | isFalse: {p : Prop} → ¬p → Decidable p
isFalse h2: ¬Thunk.get xs = Thunk.get ys
h2 => by
Goals accomplished! 🐙
        α: 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)apply isFalse: {p : Prop} → ¬p → Decidable p
isFalseα: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: ¬Thunk.get xs = Thunk.get ys

h¬cons x xs = cons y ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: ¬Thunk.get xs = Thunk.get ys

h¬cons x xs = cons y ys α: 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)simp only [cons.injEq: ∀ {α : Type ?u.2544} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, not_and: ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
not_and]α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: ¬Thunk.get xs = Thunk.get ys

hx = y → ¬xs = ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: ¬Thunk.get xs = Thunk.get ys

hx = y → ¬xs = ys α: 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)intro _: x = y
_ xs_ys: xs = ys
xs_ysα: 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

hFalse;α: 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

hFalse α: 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)apply h2: ¬Thunk.get xs = Thunk.get ys
h2α: 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

hThunk.get xs = Thunk.get ys;α: 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

hThunk.get xs = Thunk.get ys α: 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)rw [α: 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

hThunk.get xs = Thunk.get ysxs_ys: xs = ys
xs_ysα: 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

hThunk.get ys = Thunk.get ys]
Goals accomplished! 🐙
      | isTrue: {p : Prop} → p → Decidable p
isTrue h2: Thunk.get xs = Thunk.get ys
h2 => by
Goals accomplished! 🐙 α: 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)apply isTrue: {p : Prop} → p → Decidable p
isTrueα: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: Thunk.get xs = Thunk.get ys

hcons x xs = cons y ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: Thunk.get xs = Thunk.get ys

hcons x xs = cons y ys α: 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)congrα: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: Thunk.get xs = Thunk.get ys

h.e_tlxs = ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: Thunk.get xs = Thunk.get ys

h.e_tlxs = ys α: 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)extα: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: Thunk.get xs = Thunk.get ys

h.e_tl.eqThunk.get xs = Thunk.get ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: x = y

h2: Thunk.get xs = Thunk.get ys

h.e_tl.eqThunk.get xs = Thunk.get ys α: 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)exact h2: Thunk.get xs = Thunk.get ys
h2
Goals accomplished! 🐙
    else by
Goals accomplished! 🐙 α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

Decidable (cons x xs = cons y ys)apply isFalse: {p : Prop} → ¬p → Decidable p
isFalseα: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

h¬cons x xs = cons y ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

h¬cons x xs = cons y ys α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

Decidable (cons x xs = cons y ys)simp only [cons.injEq: ∀ {α : Type ?u.2855} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, not_and: ∀ {a b : Prop}, ¬(a ∧ b) ↔ a → ¬b
not_and]α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

hx = y → ¬xs = ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

hx = y → ¬xs = ys α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

Decidable (cons x xs = cons y ys)introα: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

a✝: x = y

h¬xs = ys;α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

a✝: x = y

h¬xs = ys α: Type u

inst✝: DecidableEq α

x: α

xs: Thunk (LazyList α)

y: α

ys: Thunk (LazyList α)

h: ¬x = y

Decidable (cons x xs = cons y ys)contradiction
Goals accomplished! 🐙
  | nil: {α : Type ?u.2278} → LazyList α
nil, cons: {α : Type ?u.2280} → α → Thunk (LazyList α) → LazyList α
cons _ _ => by
Goals accomplished! 🐙 α: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

Decidable (nil = cons hd✝ tl✝)apply isFalse: {p : Prop} → ¬p → Decidable p
isFalseα: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

h¬nil = cons hd✝ tl✝;α: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

h¬nil = cons hd✝ tl✝ α: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

Decidable (nil = cons hd✝ tl✝)simp
Goals accomplished! 🐙
  | cons: {α : Type ?u.2312} → α → Thunk (LazyList α) → LazyList α
cons _ _, nil: {α : Type ?u.2317} → LazyList α
nil => by
Goals accomplished! 🐙 α: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

Decidable (cons hd✝ tl✝ = nil)apply isFalse: {p : Prop} → ¬p → Decidable p
isFalseα: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

h¬cons hd✝ tl✝ = nil;α: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

h¬cons hd✝ tl✝ = nil α: Type u

inst✝: DecidableEq α

hd✝: α

tl✝: Thunk (LazyList α)

Decidable (cons hd✝ tl✝ = nil)simp
Goals accomplished! 🐙

/-- Traversal of lazy lists using an applicative effect. -/
protected def traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → LazyList α → m (LazyList β)
traverse {m: Type u → Type u
m : Type u: Type (u+1)
Type u → Type u: Type (u+1)
Type u} [Applicative: (Type ?u.11375 → Type ?u.11374) → Type (max(?u.11375+1)?u.11374)
Applicative m: Type u → Type u
m] {α: Type u
α β: Type u
β : Type u: Type (u+1)
Type u} (f: α → m β
f : α: Type u
α → m: Type u → Type u
m β: Type u
β) :
    LazyList: Type ?u.11390 → Type ?u.11390
LazyList α: Type u
α → m: Type u → Type u
m (LazyList: Type ?u.11392 → Type ?u.11392
LazyList β: Type u
β)
  | LazyList.nil: {α : Type ?u.11403} → LazyList α
LazyList.nil => pure: {f : Type ?u.11413 → Type ?u.11412} → [self : Pure f] → {α : Type ?u.11413} → α → f α
pure LazyList.nil: {α : Type ?u.11430} → LazyList α
LazyList.nil
  | LazyList.cons: {α : Type ?u.11450} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x xs: Thunk (LazyList α)
xs => LazyList.cons: {α : Type ?u.11516} → α → Thunk (LazyList α) → LazyList α
LazyList.cons <$> f: α → m β
f x: α
x <*> Thunk.pure: {α : Type ?u.11569} → α → Thunk α
Thunk.pure <$> xs: Thunk (LazyList α)
xs.get: {α : Type ?u.11574} → Thunk α → α
get.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → LazyList α → m (LazyList β)
traverse f: α → m β
f
#align lazy_list.traverse LazyList.traverse: {m : Type u → Type u} → [inst : Applicative m] → {α β : Type u} → (α → m β) → LazyList α → m (LazyList β)
LazyList.traverse

instance: Traversable LazyList
instance : Traversable: (Type ?u.19645 → Type ?u.19645) → Type (?u.19645+1)
Traversable LazyList: Type ?u.19646 → Type ?u.19646
LazyList where
  map := @LazyList.traverse: {m : Type ?u.19662 → Type ?u.19662} →
  [inst : Applicative m] → {α β : Type ?u.19662} → (α → m β) → LazyList α → m (LazyList β)
LazyList.traverse Id: Type ?u.19663 → Type ?u.19663
Id _
  traverse := @LazyList.traverse: {m : Type ?u.19703 → Type ?u.19703} →
  [inst : Applicative m] → {α β : Type ?u.19703} → (α → m β) → LazyList α → m (LazyList β)
LazyList.traverse

instance: IsLawfulTraversable LazyList
instance : IsLawfulTraversable: (t : Type ?u.20080 → Type ?u.20080) → [inst : Traversable t] → Type (?u.20080+1)
IsLawfulTraversable LazyList: Type ?u.20081 → Type ?u.20081
LazyList := by
Goals accomplished! 🐙
  
IsLawfulTraversable LazyListapply Equiv.isLawfulTraversable': {t t' : Type ?u.20094 → Type ?u.20094} →
  (eqv : (α : Type ?u.20094) → t α ≃ t' α) →
    [inst : Traversable t] →
      [inst_1 : IsLawfulTraversable t] →
        [inst_2 : Traversable t'] →
          (∀ {α β : Type ?u.20094} (f : α → β), Functor.map f = Equiv.map eqv f) →
            (∀ {α β : Type ?u.20094} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ const α) f) →
              (∀ {F : Type ?u.20094 → Type ?u.20094} [inst_3 : Applicative F] [inst_4 : LawfulApplicative F]
                  {α β : Type ?u.20094} (f : α → F β), traverse f = Equiv.traverse eqv f) →
                IsLawfulTraversable t'
Equiv.isLawfulTraversable' listEquivLazyList: (α : Type ?u.20097) → List α ≃ LazyList α
listEquivLazyList
h₀∀ {α β : Type ?u.20081} (f : α → β), Functor.map f = Equiv.map listEquivLazyList f
h₁∀ {α β : Type ?u.20081} (f : β), Functor.mapConst f = (Equiv.map listEquivLazyList ∘ const α) f
h₂∀ {F : Type ?u.20081 → Type ?u.20081} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type ?u.20081}
  (f : α → F β), traverse f = Equiv.traverse listEquivLazyList f 
IsLawfulTraversable LazyList<;>
h₀∀ {α β : Type ?u.20081} (f : α → β), Functor.map f = Equiv.map listEquivLazyList f
h₁∀ {α β : Type ?u.20081} (f : β), Functor.mapConst f = (Equiv.map listEquivLazyList ∘ const α) f
h₂∀ {F : Type ?u.20081 → Type ?u.20081} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type ?u.20081}
  (f : α → F β), traverse f = Equiv.traverse listEquivLazyList f 
IsLawfulTraversable LazyListintrosF✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f✝: α✝ → F✝ β✝

h₂traverse f✝ = Equiv.traverse listEquivLazyList f✝ 
IsLawfulTraversable LazyList<;>α✝, β✝: Type ?u.20081

f✝: α✝ → β✝

h₀Functor.map f✝ = Equiv.map listEquivLazyList f✝
α✝, β✝: Type ?u.20081

f✝: β✝

h₁Functor.mapConst f✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f✝: α✝ → F✝ β✝

h₂traverse f✝ = Equiv.traverse listEquivLazyList f✝ 
IsLawfulTraversable LazyListextF✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f✝: α✝ → F✝ β✝

x✝: LazyList α✝

h₂.htraverse f✝ x✝ = Equiv.traverse listEquivLazyList f✝ x✝ 
IsLawfulTraversable LazyList<;>α✝, β✝: Type ?u.20081

f✝: α✝ → β✝

x✝: LazyList α✝

h₀.hf✝ <$> x✝ = Equiv.map listEquivLazyList f✝ x✝
α✝, β✝: Type ?u.20081

f✝: β✝

x✝: LazyList α✝

h₁.hFunctor.mapConst f✝ x✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝ x✝
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f✝: α✝ → F✝ β✝

x✝: LazyList α✝

h₂.htraverse f✝ x✝ = Equiv.traverse listEquivLazyList f✝ x✝ 
IsLawfulTraversable LazyListrename_i f: α✝ → F✝ β✝
f xs: ?α
xsF✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs
  
IsLawfulTraversable LazyList·α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

h₀.hf <$> xs = Equiv.map listEquivLazyList f xs α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

h₀.hf <$> xs = Equiv.map listEquivLazyList f xs
α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xsinduction' xs: ?α
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.20296 (fn✝ a)
ihα✝, β✝: Type ?u.20081

f: α✝ → β✝

h₀.h.nilf <$> nil = Equiv.map listEquivLazyList f nil
α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.20297 tl✝

h₀.h.consf <$> cons hd✝ tl✝ = Equiv.map listEquivLazyList f (cons hd✝ tl✝)
α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mk?m.20297 { fn := fn✝ }
    α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

h₀.hf <$> xs = Equiv.map listEquivLazyList f xs·α✝, β✝: Type ?u.20081

f: α✝ → β✝

h₀.h.nilf <$> nil = Equiv.map listEquivLazyList f nil α✝, β✝: Type ?u.20081

f: α✝ → β✝

h₀.h.nilf <$> nil = Equiv.map listEquivLazyList f nil
α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.20297 tl✝

h₀.h.consf <$> cons hd✝ tl✝ = Equiv.map listEquivLazyList f (cons hd✝ tl✝)
α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mk?m.20297 { fn := fn✝ }rfl
Goals accomplished! 🐙
    α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

h₀.hf <$> xs = Equiv.map listEquivLazyList f xs·α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.20297 tl✝

h₀.h.consf <$> cons hd✝ tl✝ = Equiv.map listEquivLazyList f (cons hd✝ tl✝) α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.20297 tl✝

h₀.h.consf <$> cons hd✝ tl✝ = Equiv.map listEquivLazyList f (cons hd✝ tl✝)
α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mk?m.20297 { fn := fn✝ }simpa only [Equiv.map: {t t' : Type ?u.20389 → Type ?u.20389} →
  ((α : Type ?u.20389) → t α ≃ t' α) → [inst : Functor t] → {α β : Type ?u.20389} → (α → β) → t' α → t' β
Equiv.map, Functor.map: {f : Type ?u.20404 → Type ?u.20403} → [self : Functor f] → {α β : Type ?u.20404} → (α → β) → f α → f β
Functor.map, listEquivLazyList: (α : Type ?u.20414) → List α ≃ LazyList α
listEquivLazyList, Equiv.coe_fn_symm_mk: ∀ {α : Sort ?u.20417} {β : Sort ?u.20416} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
  ↑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk: ∀ {α : Sort ?u.20454} {β : Sort ?u.20453} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
  ↑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f
Equiv.coe_fn_mk,
        LazyList.traverse: {m : Type ?u.20477 → Type ?u.20477} →
  [inst : Applicative m] → {α β : Type ?u.20477} → (α → m β) → LazyList α → m (LazyList β)
LazyList.traverse, Seq.seq: {f : Type ?u.20875 → Type ?u.20874} → [self : Seq f] → {α β : Type ?u.20875} → f (α → β) → (Unit → f α) → f β
Seq.seq, toList: {α : Type ?u.20885} → LazyList α → List α
toList, ofList: {α : Type ?u.20897} → List α → LazyList α
ofList, cons.injEq: ∀ {α : Type ?u.20913} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]
Goals accomplished! 🐙
    α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

h₀.hf <$> xs = Equiv.map listEquivLazyList f xs·α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mkThunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ })) =   { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) } α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mkThunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ })) =   { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) }extα✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mk.eqThunk.get (Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) =   Thunk.get { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) };α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mk.eqThunk.get (Thunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ }))) =   Thunk.get { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) } α✝, β✝: Type ?u.20081

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), f <$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)

h₀.h.mkThunk.pure (LazyList.traverse f (Thunk.get { fn := fn✝ })) =   { fn := fun x => ofList (List.map f (toList (Thunk.get { fn := fn✝ }))) }apply ih: ∀ (a : Unit), ?m.20296 (fn✝ a)
ih
Goals accomplished! 🐙
  
IsLawfulTraversable LazyList·α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xssimp only [Equiv.map: {t t' : Type ?u.21491 → Type ?u.21491} →
  ((α : Type ?u.21491) → t α ≃ t' α) → [inst : Functor t] → {α β : Type ?u.21491} → (α → β) → t' α → t' β
Equiv.map, listEquivLazyList: (α : Type ?u.21505) → List α ≃ LazyList α
listEquivLazyList, Equiv.coe_fn_symm_mk: ∀ {α : Sort ?u.21508} {β : Sort ?u.21507} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
  ↑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk: ∀ {α : Sort ?u.21545} {β : Sort ?u.21544} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
  ↑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f
Equiv.coe_fn_mk, comp: {α : Sort ?u.21570} → {β : Sort ?u.21569} → {δ : Sort ?u.21568} → (β → δ) → (α → β) → α → δ
comp,
      Functor.mapConst: {f : Type ?u.21581 → Type ?u.21580} → [self : Functor f] → {α β : Type ?u.21581} → α → f β → f α
Functor.mapConst]α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hLazyList.traverse (const α✝ f) xs = ofList (const α✝ f <$> toList xs)
    α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xsinduction' xs: ?α
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.21859 (fn✝ a)
ihα✝, β✝: Type ?u.20081

f: β✝

h₁.h.nilLazyList.traverse (const α✝ f) nil = ofList (const α✝ f <$> toList nil)
α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.21860 tl✝

h₁.h.consLazyList.traverse (const α✝ f) (cons hd✝ tl✝) = ofList (const α✝ f <$> toList (cons hd✝ tl✝))
α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mk?m.21860 { fn := fn✝ }
    α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs·α✝, β✝: Type ?u.20081

f: β✝

h₁.h.nilLazyList.traverse (const α✝ f) nil = ofList (const α✝ f <$> toList nil) α✝, β✝: Type ?u.20081

f: β✝

h₁.h.nilLazyList.traverse (const α✝ f) nil = ofList (const α✝ f <$> toList nil)
α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.21860 tl✝

h₁.h.consLazyList.traverse (const α✝ f) (cons hd✝ tl✝) = ofList (const α✝ f <$> toList (cons hd✝ tl✝))
α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mk?m.21860 { fn := fn✝ }rfl
Goals accomplished! 🐙
    α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs·α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.21860 tl✝

h₁.h.consLazyList.traverse (const α✝ f) (cons hd✝ tl✝) = ofList (const α✝ f <$> toList (cons hd✝ tl✝)) α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.21860 tl✝

h₁.h.consLazyList.traverse (const α✝ f) (cons hd✝ tl✝) = ofList (const α✝ f <$> toList (cons hd✝ tl✝))
α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mk?m.21860 { fn := fn✝ }simpa only [toList: {α : Type ?u.21947} → LazyList α → List α
toList, ofList: {α : Type ?u.21957} → List α → LazyList α
ofList, LazyList.traverse: {m : Type ?u.21967 → Type ?u.21967} →
  [inst : Applicative m] → {α β : Type ?u.21967} → (α → m β) → LazyList α → m (LazyList β)
LazyList.traverse, Seq.seq: {f : Type ?u.22002 → Type ?u.22001} → [self : Seq f] → {α β : Type ?u.22002} → f (α → β) → (Unit → f α) → f β
Seq.seq, Functor.map: {f : Type ?u.22005 → Type ?u.22004} → [self : Functor f] → {α β : Type ?u.22005} → (α → β) → f α → f β
Functor.map, cons.injEq: ∀ {α : Type ?u.22014} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]
Goals accomplished! 🐙
    α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs·α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mkThunk.pure (LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ })) =   { fn := fun x => ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ }))) } α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mkThunk.pure (LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ })) =   { fn := fun x => ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ }))) }congrα✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mk.e_aLazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ }) =   ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ })));α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mk.e_aLazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ }) =   ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ }))) α✝, β✝: Type ?u.20081

f: β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse (const α✝ f) (fn✝ a) = ofList (const α✝ f <$> toList (fn✝ a))

h₁.h.mkThunk.pure (LazyList.traverse (const α✝ f) (Thunk.get { fn := fn✝ })) =   { fn := fun x => ofList (List.map (const α✝ f) (toList (Thunk.get { fn := fn✝ }))) }apply ih: ∀ (a : Unit), ?m.21859 (fn✝ a)
ih
Goals accomplished! 🐙
  
IsLawfulTraversable LazyList·F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xssimp only [traverse: {t : Type ?u.22949 → Type ?u.22949} →
  [self : Traversable t] →
    {m : Type ?u.22949 → Type ?u.22949} → [inst : Applicative m] → {α β : Type ?u.22949} → (α → m β) → t α → m (t β)
traverse, Equiv.traverse: {t t' : Type ?u.22962 → Type ?u.22962} →
  ((α : Type ?u.22962) → t α ≃ t' α) →
    [inst : Traversable t] →
      {m : Type ?u.22962 → Type ?u.22962} → [inst : Applicative m] → {α β : Type ?u.22962} → (α → m β) → t' α → m (t' β)
Equiv.traverse, listEquivLazyList: (α : Type ?u.22979) → List α ≃ LazyList α
listEquivLazyList, Equiv.coe_fn_mk: ∀ {α : Sort ?u.22982} {β : Sort ?u.22981} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
  ↑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = f
Equiv.coe_fn_mk, Equiv.coe_fn_symm_mk: ∀ {α : Sort ?u.22997} {β : Sort ?u.22996} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
  ↑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = g
Equiv.coe_fn_symm_mk]F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.hLazyList.traverse f xs = ofList <$> List.traverse f (toList xs)
    F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xsinduction' xs: ?α
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ tl: Thunk (LazyList ?m.23297)
tl ih: ?m.23299 tl
ih _ ih: ∀ (a : Unit), ?m.23298 (fn✝ a)
ihF✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

h₂.h.nilLazyList.traverse f nil = ofList <$> List.traverse f (toList nil)
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih: ?m.23299 tl

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))

h₂.h.mk?m.23299 { fn := fn✝ }
    F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs·F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

h₂.h.nilLazyList.traverse f nil = ofList <$> List.traverse f (toList nil) F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

h₂.h.nilLazyList.traverse f nil = ofList <$> List.traverse f (toList nil)
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih: ?m.23299 tl

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))

h₂.h.mk?m.23299 { fn := fn✝ }simp only [List.traverse: {F : Type ?u.23323 → Type ?u.23322} →
  [inst : Applicative F] → {α : Type ?u.23321} → {β : Type ?u.23323} → (α → F β) → List α → F (List β)
List.traverse, map_pure: ∀ {f : Type ?u.23684 → Type ?u.23683} [inst : Applicative f] [self : LawfulApplicative f] {α β : Type ?u.23684}
  (g : α → β) (x : α), g <$> pure x = pure (g x)
map_pure]F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

h₂.h.nilLazyList.traverse f nil = pure (ofList []);F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

h₂.h.nilLazyList.traverse f nil = pure (ofList []) F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

h₂.h.nilLazyList.traverse f nil = ofList <$> List.traverse f (toList nil)rfl
Goals accomplished! 🐙
    F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs·F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih: ?m.23299 tl

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl)) F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih: ?m.23299 tl

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))

h₂.h.mk?m.23299 { fn := fn✝ }have : tl: Thunk (LazyList ?m.23297)
tl.get: {α : Type ?u.23932} → Thunk α → α
get.traverse: {m : Type ?u.23935 → Type ?u.23935} →
  [inst : Applicative m] → {α β : Type ?u.23935} → (α → m β) → LazyList α → m (LazyList β)
traverse f: α✝ → F✝ β✝
f = ofList: {α : Type ?u.23957} → List α → LazyList α
ofList <$> tl: Thunk (LazyList ?m.23297)
tl.get: {α : Type ?u.23962} → Thunk α → α
get.toList: {α : Type ?u.23964} → LazyList α → List α
toList.traverse: {F : Type ?u.23968 → Type ?u.23967} →
  [inst : Applicative F] → {α : Type ?u.23966} → {β : Type ?u.23968} → (α → F β) → List α → F (List β)
traverse f: α✝ → F✝ β✝
f := ih: ?m.23299 tl
ihF✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih, this: LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))
      F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih: ?m.23299 tl

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))simp only [traverse._eq_2: ∀ {m : Type ?u.24044 → Type ?u.24044} [inst : Applicative m] {α β : Type ?u.24044} (f : α → m β) (x_1 : α)
  (xs : Thunk (LazyList α)),
  LazyList.traverse f (cons x_1 xs) =     Seq.seq (cons <$> f x_1) fun x => Thunk.pure <$> LazyList.traverse f (Thunk.get xs)
traverse._eq_2, ih: ?m.23299 tl
ih, Functor.map_map: ∀ {α β γ : Type ?u.24076} {f : Type ?u.24076 → Type ?u.24075} [inst : Functor f] [inst_1 : LawfulFunctor f] (m : α → β)
  (g : β → γ) (x : f α), g <$> m <$> x = (g ∘ m) <$> x
Functor.map_map, seq_map_assoc: ∀ {α β γ : Type ?u.24097} {F : Type ?u.24097 → Type ?u.24096} [inst : Applicative F] [inst_1 : LawfulApplicative F]
  (x : F (α → β)) (f : γ → α) (y : F γ), (Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x ∘ f) <$> x) fun x => y
seq_map_assoc, toList: {α : Type ?u.24126} → LazyList α → List α
toList, List.traverse: {F : Type ?u.24141 → Type ?u.24140} →
  [inst : Applicative F] → {α : Type ?u.24139} → {β : Type ?u.24141} → (α → F β) → List α → F (List β)
List.traverse, map_seq: ∀ {α β γ : Type ?u.24176} {F : Type ?u.24176 → Type ?u.24175} [inst : Applicative F] [inst_1 : LawfulApplicative F]
  (f : β → γ) (x : F (α → β)) (y : F α), (f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <$> x) fun x => y
map_seq]F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih, this: LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))

h₂.h.cons(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))
      F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih: ?m.23299 tl

h₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <$> List.traverse f (toList (cons hd✝ tl))·F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih, this: LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))

h₂.h.cons(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)) F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

hd✝: α✝

tl: Thunk (LazyList α✝)

ih, this: LazyList.traverse f (Thunk.get tl) = ofList <$> List.traverse f (toList (Thunk.get tl))

h₂.h.cons(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))rfl
Goals accomplished! 🐙
    F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs·F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))

h₂.h.mkLazyList.traverse f (Thunk.get { fn := fn✝ }) = ofList <$> List.traverse f (toList (Thunk.get { fn := fn✝ })) F✝: Type ?u.20081 → Type ?u.20081

inst✝¹: Applicative F✝

inst✝: LawfulApplicative F✝

α✝, β✝: Type ?u.20081

f: α✝ → F✝ β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), LazyList.traverse f (fn✝ a) = ofList <$> List.traverse f (toList (fn✝ a))

h₂.h.mkLazyList.traverse f (Thunk.get { fn := fn✝ }) = ofList <$> List.traverse f (toList (Thunk.get { fn := fn✝ }))apply ih: ∀ (a : Unit), ?m.23298 (fn✝ a)
ih
Goals accomplished! 🐙

/-- `init xs`, if `xs` non-empty, drops the last element of the list.
Otherwise, return the empty list. -/
def init: {α : Type u_1} → LazyList α → LazyList α
init {α: Type ?u.25676
α} : LazyList: Type ?u.25676 → Type ?u.25676
LazyList α: ?m.25672
α → LazyList: Type ?u.25678 → Type ?u.25678
LazyList α: ?m.25672
α
  | LazyList.nil: {α : Type ?u.25685} → LazyList α
LazyList.nil => LazyList.nil: {α : Type ?u.25694} → LazyList α
LazyList.nil
  | LazyList.cons: {α : Type ?u.25696} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x xs: Thunk (LazyList α)
xs =>
    let xs': ?m.25718
xs' := xs: Thunk (LazyList α)
xs.get: {α : Type ?u.25719} → Thunk α → α
get
    match xs': ?m.25718
xs' with
    | LazyList.nil: {α : Type ?u.25725} → LazyList α
LazyList.nil => LazyList.nil: {α : Type ?u.25733} → LazyList α
LazyList.nil
    | LazyList.cons: {α : Type ?u.25735} → α → Thunk (LazyList α) → LazyList α
LazyList.cons _ _ => LazyList.cons: {α : Type ?u.25757} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x (init: {α : Type ?u.25676} → LazyList α → LazyList α
init xs': ?m.25718
xs')
#align lazy_list.init LazyList.init: {α : Type u_1} → LazyList α → LazyList α
LazyList.init

/-- Return the first object contained in the list that satisfies
predicate `p` -/
def find: {α : Type ?u.34584} → (p : α → Prop) → [inst : DecidablePred p] → LazyList α → Option α
find {α: ?m.34566
α} (p: α → Prop
p : α: ?m.34566
α → Prop: Type
Prop) [DecidablePred: {α : Sort ?u.34573} → (α → Prop) → Sort (max1?u.34573)
DecidablePred p: α → Prop
p] : LazyList: Type ?u.34584 → Type ?u.34584
LazyList α: ?m.34566
α → Option: Type ?u.34586 → Type ?u.34586
Option α: ?m.34566
α
  | nil: {α : Type ?u.34596} → LazyList α
nil => none: {α : Type ?u.34605} → Option α
none
  | cons: {α : Type ?u.34608} → α → Thunk (LazyList α) → LazyList α
cons h: α
h t: Thunk (LazyList α)
t => if p: α → Prop
p h: α
h then some: {α : Type ?u.34639} → α → Option α
some h: α
h else t: Thunk (LazyList α)
t.get: {α : Type ?u.34641} → Thunk α → α
get.find: {α : Type ?u.34584} → (p : α → Prop) → [inst : DecidablePred p] → LazyList α → Option α
find p: α → Prop
p
#align lazy_list.find LazyList.find: {α : Type u_1} → (p : α → Prop) → [inst : DecidablePred p] → LazyList α → Option α
LazyList.find

/-- `interleave xs ys` creates a list where elements of `xs` and `ys` alternate. -/
def interleave: {α : Type u_1} → LazyList α → LazyList α → LazyList α
interleave {α: ?m.42506
α} : LazyList: Type ?u.42510 → Type ?u.42510
LazyList α: ?m.42506
α → LazyList: Type ?u.42513 → Type ?u.42513
LazyList α: ?m.42506
α → LazyList: Type ?u.42515 → Type ?u.42515
LazyList α: ?m.42506
α
  | LazyList.nil: {α : Type ?u.42525} → LazyList α
LazyList.nil, xs: LazyList α
xs => xs: LazyList α
xs
  | a: LazyList α
a@(LazyList.cons: {α : Type ?u.42543} → α → Thunk (LazyList α) → LazyList α
LazyList.cons _ _), LazyList.nil: {α : Type ?u.42548} → LazyList α
LazyList.nil => a: LazyList α
a
  | LazyList.cons: {α : Type ?u.42598} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x xs: Thunk (LazyList α)
xs, LazyList.cons: {α : Type ?u.42602} → α → Thunk (LazyList α) → LazyList α
LazyList.cons y: α
y ys: Thunk (LazyList α)
ys =>
    LazyList.cons: {α : Type ?u.42639} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x (LazyList.cons: {α : Type ?u.42641} → α → Thunk (LazyList α) → LazyList α
LazyList.cons y: α
y (interleave: {α : Type ?u.42510} → LazyList α → LazyList α → LazyList α
interleave xs: Thunk (LazyList α)
xs.get: {α : Type ?u.42644} → Thunk α → α
get ys: Thunk (LazyList α)
ys.get: {α : Type ?u.42648} → Thunk α → α
get))
#align lazy_list.interleave LazyList.interleave: {α : Type u_1} → LazyList α → LazyList α → LazyList α
LazyList.interleave

/-- `interleaveAll (xs::ys::zs::xss)` creates a list where elements of `xs`, `ys`
and `zs` and the rest alternate. Every other element of the resulting list is taken from
`xs`, every fourth is taken from `ys`, every eighth is taken from `zs` and so on. -/
def interleaveAll: {α : Type ?u.52567} → List (LazyList α) → LazyList α
interleaveAll {α: ?m.52562
α} : List: Type ?u.52566 → Type ?u.52566
List (LazyList: Type ?u.52567 → Type ?u.52567
LazyList α: ?m.52562
α) → LazyList: Type ?u.52569 → Type ?u.52569
LazyList α: ?m.52562
α
  | [] => LazyList.nil: {α : Type ?u.52585} → LazyList α
LazyList.nil
  | x: LazyList α
x :: xs: List (LazyList α)
xs => interleave: {α : Type ?u.52608} → LazyList α → LazyList α → LazyList α
interleave x: LazyList α
x (interleaveAll: {α : Type ?u.52567} → List (LazyList α) → LazyList α
interleaveAll xs: List (LazyList α)
xs)
#align lazy_list.interleave_all LazyList.interleaveAll: {α : Type u_1} → List (LazyList α) → LazyList α
LazyList.interleaveAll

/-- Monadic bind operation for `LazyList`. -/
protected def bind: {α : Type u_1} → {β : Type u_2} → LazyList α → (α → LazyList β) → LazyList β
bind {α: Type ?u.52848
α β: ?m.52844
β} : LazyList: Type ?u.52848 → Type ?u.52848
LazyList α: ?m.52841
α → (α: ?m.52841
α → LazyList: Type ?u.52853 → Type ?u.52853
LazyList β: ?m.52844
β) → LazyList: Type ?u.52855 → Type ?u.52855
LazyList β: ?m.52844
β
  | LazyList.nil: {α : Type ?u.52868} → LazyList α
LazyList.nil, _ => LazyList.nil: {α : Type ?u.52888} → LazyList α
LazyList.nil
  | LazyList.cons: {α : Type ?u.52891} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x xs: Thunk (LazyList α)
xs, f: α → LazyList β
f => (f: α → LazyList β
f x: α
x).append: {α : Type ?u.52926} → LazyList α → Thunk (LazyList α) → LazyList α
append (xs: Thunk (LazyList α)
xs.get: {α : Type ?u.52931} → Thunk α → α
get.bind: {α : Type ?u.52848} → {β : Type ?u.52853} → LazyList α → (α → LazyList β) → LazyList β
bind f: α → LazyList β
f)
#align lazy_list.bind LazyList.bind: {α : Type u_1} → {β : Type u_2} → LazyList α → (α → LazyList β) → LazyList β
LazyList.bind

/-- Reverse the order of a `LazyList`.
It is done by converting to a `List` first because reversal involves evaluating all
the list and if the list is all evaluated, `List` is a better representation for
it than a series of thunks. -/
def reverse: {α : Type ?u.61945} → LazyList α → LazyList α
reverse {α: ?m.61942
α} (xs: LazyList α
xs : LazyList: Type ?u.61945 → Type ?u.61945
LazyList α: ?m.61942
α) : LazyList: Type ?u.61948 → Type ?u.61948
LazyList α: ?m.61942
α :=
  ofList: {α : Type ?u.61952} → List α → LazyList α
ofList xs: LazyList α
xs.toList: {α : Type ?u.61955} → LazyList α → List α
toList.reverse: {α : Type ?u.61957} → List α → List α
reverse
#align lazy_list.reverse LazyList.reverse: {α : Type u_1} → LazyList α → LazyList α
LazyList.reverse

instance: Monad LazyList
instance : Monad: (Type ?u.61990 → Type ?u.61989) → Type (max(?u.61990+1)?u.61989)
Monad LazyList: Type ?u.61991 → Type ?u.61991
LazyList where
  pure := @LazyList.singleton: {α : Type ?u.62028} → α → LazyList α
LazyList.singleton
  bind := @LazyList.bind: {α : Type ?u.62121} → {β : Type ?u.62120} → LazyList α → (α → LazyList β) → LazyList β
LazyList.bind

-- Porting note: Added `Thunk.pure` to definition.
theorem append_nil: ∀ {α : Type u_1} (xs : LazyList α), append xs (Thunk.pure nil) = xs
append_nil {α: Type u_1
α} (xs: LazyList α
xs : LazyList: Type ?u.62778 → Type ?u.62778
LazyList α: ?m.62775
α) : xs: LazyList α
xs.append: {α : Type ?u.62782} → LazyList α → Thunk (LazyList α) → LazyList α
append (Thunk.pure: {α : Type ?u.62788} → α → Thunk α
Thunk.pure LazyList.nil: {α : Type ?u.62791} → LazyList α
LazyList.nil) = xs: LazyList α
xs := by
Goals accomplished! 🐙
  α: Type u_1

xs: LazyList α

append xs (Thunk.pure nil) = xsinduction' xs: LazyList α
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.62824 (fn✝ a)
ihα: Type u_1

nilappend nil (Thunk.pure nil) = nil
α: Type u_1

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.62825 tl✝

consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝
α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk?m.62825 { fn := fn✝ }
  α: Type u_1

xs: LazyList α

append xs (Thunk.pure nil) = xs·α: Type u_1

nilappend nil (Thunk.pure nil) = nil α: Type u_1

nilappend nil (Thunk.pure nil) = nil
α: Type u_1

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.62825 tl✝

consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝
α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk?m.62825 { fn := fn✝ }rfl
Goals accomplished! 🐙
  α: Type u_1

xs: LazyList α

append xs (Thunk.pure nil) = xs·α: Type u_1

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.62825 tl✝

consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝ α: Type u_1

xs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.62825 tl✝

consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝
α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk?m.62825 { fn := fn✝ }simpa only [append: {α : Type ?u.62865} → LazyList α → Thunk (LazyList α) → LazyList α
append, cons.injEq: ∀ {α : Type ?u.63287} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]
Goals accomplished! 🐙
  α: Type u_1

xs: LazyList α

append xs (Thunk.pure nil) = xs·α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk{ fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ } α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk{ fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }extα: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk.eqThunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ };α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk.eqThunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ } α: Type u_1

xs: LazyList α

fn✝: Unit → LazyList α

ih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ a

mk{ fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }apply ih: ∀ (a : Unit), ?m.62824 (fn✝ a)
ih
Goals accomplished! 🐙
#align lazy_list.append_nil LazyList.append_nil: ∀ {α : Type u_1} (xs : LazyList α), append xs (Thunk.pure nil) = xs
LazyList.append_nil

theorem append_assoc: ∀ {α : 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 } }
append_assoc {α: Type u_1
α} (xs: LazyList α
xs ys: LazyList α
ys zs: LazyList α
zs : LazyList: Type ?u.63490 → Type ?u.63490
LazyList α: ?m.63484
α) :
    (xs: LazyList α
xs.append: {α : Type ?u.63497} → LazyList α → Thunk (LazyList α) → LazyList α
append ys: LazyList α
ys).append: {α : Type ?u.64408} → LazyList α → Thunk (LazyList α) → LazyList α
append zs: LazyList α
zs = xs: LazyList α
xs.append: {α : Type ?u.65226} → LazyList α → Thunk (LazyList α) → LazyList α
append (ys: LazyList α
ys.append: {α : Type ?u.65231} → LazyList α → Thunk (LazyList α) → LazyList α
append zs: LazyList α
zs) := by
Goals accomplished! 🐙
  α: 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: LazyList α
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.66087 (fn✝ a)
ihα: Type u_1

ys, zs: LazyList α

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

xs, ys, zs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.66088 tl✝

consappend (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 } }
α: 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 } }

mk?m.66088 { 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 } }·α: Type u_1

ys, zs: LazyList α

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

ys, zs: LazyList α

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

xs, ys, zs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.66088 tl✝

consappend (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 } }
α: 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 } }

mk?m.66088 { fn := fn✝ }rfl
Goals accomplished! 🐙
  α: 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 } }·α: Type u_1

xs, ys, zs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.66088 tl✝

consappend (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 } } α: Type u_1

xs, ys, zs: LazyList α

hd✝: α

tl✝: Thunk (LazyList α)

tl_ih✝: ?m.66088 tl✝

consappend (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 } }
α: 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 } }

mk?m.66088 { fn := fn✝ }simpa only [append: {α : Type ?u.66201} → LazyList α → Thunk (LazyList α) → LazyList α
append, cons.injEq: ∀ {α : Type ?u.66222} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]
Goals accomplished! 🐙
  α: 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 } }·α: 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 } }

mk{
    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 } } } α: 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 } }

mk{
    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α: 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 } }

mk.eqThunk.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 } } };α: 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 } }

mk.eqThunk.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 } } } α: 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 } }

mk{
    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 } } }apply ih: ∀ (a : Unit), ?m.66087 (fn✝ a)
ih
Goals accomplished! 🐙
#align lazy_list.append_assoc LazyList.append_assoc: ∀ {α : 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 } }
LazyList.append_assoc

-- Porting note: Rewrote proof of `append_bind`.
theorem append_bind: ∀ {α : 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 }
append_bind {α: Type u_1
α β: Type u_2
β} (xs: LazyList α
xs : LazyList: Type ?u.66434 → Type ?u.66434
LazyList α: ?m.66428
α) (ys: Thunk (LazyList α)
ys : Thunk: Type ?u.66437 → Type ?u.66437
Thunk (LazyList: Type ?u.66438 → Type ?u.66438
LazyList α: ?m.66428
α)) (f: α → LazyList β
f : α: ?m.66428
α → LazyList: Type ?u.66443 → Type ?u.66443
LazyList β: ?m.66431
β) :
    (xs: LazyList α
xs.append: {α : Type ?u.66447} → LazyList α → Thunk (LazyList α) → LazyList α
append ys: Thunk (LazyList α)
ys).bind: {α : Type ?u.66455} → {β : Type ?u.66454} → LazyList α → (α → LazyList β) → LazyList β
bind f: α → LazyList β
f = (xs: LazyList α
xs.bind: {α : Type ?u.66468} → {β : Type ?u.66467} → LazyList α → (α → LazyList β) → LazyList β
bind f: α → LazyList β
f).append: {α : Type ?u.66479} → LazyList α → Thunk (LazyList α) → LazyList α
append (ys: Thunk (LazyList α)
ys.get: {α : Type ?u.66484} → Thunk α → α
get.bind: {α : Type ?u.66487} → {β : Type ?u.66486} → LazyList α → (α → LazyList β) → LazyList β
bind f: α → LazyList β
f) := by
Goals accomplished! 🐙
  α: 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: LazyList α
xs with
  α: 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 }| LazyList.nil: {α : Type ?u.67413} → LazyList α
LazyList.nil =>α: 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 } α: 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 }rfl
Goals accomplished! 🐙
  α: 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 }| LazyList.cons: {α : Type ?u.67426} → α → Thunk (LazyList α) → LazyList α
LazyList.cons x: α
x xs: Thunk (LazyList α)
xs =>α: 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 }
    α: 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 }simp only [append: {α : Type ?u.67590} → LazyList α → Thunk (LazyList α) → LazyList α
append, Thunk.get: {α : Type ?u.67611} → Thunk α → α
Thunk.get, LazyList.bind: {α : Type ?u.67622} → {β : Type ?u.67621} → LazyList α → (α → LazyList β) → LazyList β
LazyList.bind]α: 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 }have := append_bind: ∀ {α : 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 }
append_bind xs: Thunk (LazyList α)
xs.get: {α : Type ?u.68302} → Thunk α → α
get ys: Thunk (LazyList α)
ys f: α → LazyList β
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 }
    α: 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 [Thunk.get: {α : Type ?u.68328} → Thunk α → α
Thunk.get] at this: ?m.68299
thisα: 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 α)

LazyList.bind (append (cons x xs) ys) f =   append (LazyList.bind (cons x xs) f) { fn := fun x => LazyList.bind (Thunk.get ys) f }rw [α: 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 }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 }
this,α: 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 => append (LazyList.bind (Thunk.fn xs ()) f) { fn := fun x => LazyList.bind (Thunk.fn 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.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 }append_assoc: ∀ {α : Type ?u.68371} (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 } }
append_assocα: 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 => append (LazyList.bind (Thunk.fn xs ()) f) { fn := fun x => LazyList.bind (Thunk.fn ys ()) f } } =   append (f x)
    { fn := fun x => append (LazyList.bind (Thunk.fn xs ()) f) { fn := fun x => LazyList.bind (Thunk.fn ys ()) f } }]
Goals accomplished! 🐙
#align lazy_list.append_bind LazyList.append_bind: ∀ {α : 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 }
LazyList.append_bind

instance: LawfulMonad LazyList
instance : LawfulMonad: (m : Type ?u.76376 → Type ?u.76375) → [inst : Monad m] → Prop
LawfulMonad LazyList: Type ?u.76377 → Type ?u.76377
LazyList := LawfulMonad.mk': ∀ (m : Type ?u.76390 → Type ?u.76389) [inst : Monad m],
  (∀ {α : Type ?u.76390} (x : m α), id <$> x = x) →
    (∀ {α β : Type ?u.76390} (x : α) (f : α → m β), pure x >>= f = f x) →
      (∀ {α β γ : Type ?u.76390} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
        autoParam (∀ {α β : Type ?u.76390} (x : α) (y : m β), Functor.mapConst x y = const β x <$> y) _auto✝ →
          autoParam
              (∀ {α β : Type ?u.76390} (x : m α) (y : m β),
                (SeqLeft.seqLeft x fun x => y) = do
                  let a ← x
                  let _ ← y
                  pure a)
              _auto✝¹ →
            autoParam
                (∀ {α β : Type ?u.76390} (x : m α) (y : m β),
                  (SeqRight.seqRight x fun x => y) = do
                    let _ ← x
                    y)
                _auto✝² →
              autoParam
                  (∀ {α β : Type ?u.76390} (f : α → β) (x : m α),
                    (do
                        let y ← x
                        pure (f y)) =                       f <$> x)
                  _auto✝³ →
                autoParam
                    (∀ {α β : Type ?u.76390} (f : m (α → β)) (x : m α),
                      (do
                          let x_1 ← f
                          x_1 <$> x) =                         Seq.seq f fun x_1 => x)
                    _auto✝⁴ →
                  LawfulMonad m
LawfulMonad.mk'
  (bind_pure_comp := by
Goals accomplished! 🐙
    
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
  (do
      let y ← x
      pure (f y)) =     f <$> xintro _: Type ?u.76377
_ _: Type ?u.76377
_ f: α✝ → β✝
f xs: LazyList α✝
xsα✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

(do
    let y ← xs
    pure (f y)) =   f <$> xs
    
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
  (do
      let y ← x
      pure (f y)) =     f <$> xsimp only [bind: {m : Type ?u.77695 → Type ?u.77694} → [self : Bind m] → {α β : Type ?u.77695} → m α → (α → m β) → m β
bind, Functor.map: {f : Type ?u.77698 → Type ?u.77697} → [self : Functor f] → {α β : Type ?u.77698} → (α → β) → f α → f β
Functor.map, pure: {f : Type ?u.77701 → Type ?u.77700} → [self : Pure f] → {α : Type ?u.77701} → α → f α
pure, singleton: {α : Type ?u.77703} → α → LazyList α
singleton]α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

(LazyList.bind xs fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f xs
    
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
  (do
      let y ← x
      pure (f y)) =     f <$> xinduction' xs: LazyList α✝
xs using LazyList.rec: {α : Type u} →
  {motive_1 : LazyList α → Sort u_1} →
    {motive_2 : Thunk (LazyList α) → Sort u_1} →
      motive_1 nil →
        ((hd : α) → (tl : Thunk (LazyList α)) → motive_2 tl → motive_1 (cons hd tl)) →
          ((fn : Unit → LazyList α) → ((a : Unit) → motive_1 (fn a)) → motive_2 { fn := fn }) →
            (t : LazyList α) → motive_1 t
LazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.77773 (fn✝ a)
ihα✝, β✝: Type ?u.76377

f: α✝ → β✝

nil(LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nil
α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

cons(LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝)
α✝, β✝: Type ?u.76377

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)

mk?m.77774 { fn := fn✝ }
    
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
  (do
      let y ← x
      pure (f y)) =     f <$> x·α✝, β✝: Type ?u.76377

f: α✝ → β✝

nil(LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nil α✝, β✝: Type ?u.76377

f: α✝ → β✝

nil(LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nil
α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

cons(LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝)
α✝, β✝: Type ?u.76377

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)

mk?m.77774 { fn := fn✝ }rfl
Goals accomplished! 🐙
    
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
  (do
      let y ← x
      pure (f y)) =     f <$> x·α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

cons(LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝) α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

cons(LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝)
α✝, β✝: Type ?u.76377

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)

mk?m.77774 { fn := fn✝ }simp only [bind._eq_2: ∀ {α : Type ?u.77822} {β : Type ?u.77821} (x : α → LazyList β) (x_2 : α) (xs : Thunk (LazyList α)),
  LazyList.bind (cons x_2 xs) x = append (x x_2) { fn := fun x_1 => LazyList.bind (Thunk.get xs) x }
bind._eq_2, append: {α : Type ?u.77834} → LazyList α → Thunk (LazyList α) → LazyList α
append, traverse._eq_2: ∀ {m : Type ?u.77852 → Type ?u.77852} [inst : Applicative m] {α β : Type ?u.77852} (f : α → m β) (x_1 : α)
  (xs : Thunk (LazyList α)),
  LazyList.traverse f (cons x_1 xs) =     Seq.seq (cons <$> f x_1) fun x => Thunk.pure <$> LazyList.traverse f (Thunk.get xs)
traverse._eq_2, Id.map_eq: ∀ {α β : Type ?u.77868} (x : Id α) (f : α → β), f <$> x = f x
Id.map_eq, cons.injEq: ∀ {α : Type ?u.77878} (hd : α) (tl : Thunk (LazyList α)) (hd_1 : α) (tl_1 : Thunk (LazyList α)),
  (cons hd tl = cons hd_1 tl_1) = (hd = hd_1 ∧ tl = tl_1)
cons.injEq, true_and: ∀ (p : Prop), (True ∧ p) = p
true_and]α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

conscons (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✝));α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

conscons (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✝)) α✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

hd✝: α✝

tl✝: Thunk (LazyList α✝)

tl_ih✝: ?m.77774 tl✝

cons(LazyList.bind (cons hd✝ tl✝) fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f (cons hd✝ tl✝)congr
Goals accomplished! 🐙
    
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
  (do
      let y ← x
      pure (f y)) =     f <$> x·α✝, β✝: Type ?u.76377

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)

mk{
    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✝ }))) () α✝, β✝: Type ?u.76377

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)

mk{
    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✝ }))) ()extα✝, β✝: Type ?u.76377

f: α✝ → β✝

xs: LazyList α✝

fn✝: Unit → LazyList α✝

ih: ∀ (a : Unit), (LazyList.bind (fn✝ a) fun y => cons (f y) (Thunk.pure nil)<