Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Simon Hudon

! This file was ported from Lean 3 source module data.lazy_list.basic
! 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 = bext {α: Type uα : Type u: Type (u+1)Type u} {a: Thunk αa b: Thunk αb : Thunk: Type ?u.7 → Type ?u.7Thunk α: Type uα} (eq: Thunk.get a = Thunk.get beq : a: Thunk αa.get: {α : Type ?u.11} → Thunk α → αget = b: Thunk αb.get: {α : Type ?u.16} → Thunk α → αget) : a: Thunk αa = b: Thunk αb := byGoals accomplished! 🐙
α: Type ua, b: Thunk αeq: Thunk.get a = Thunk.get ba = bhave ⟨_⟩ := a: Thunk αaα: Type ua, b: Thunk αfn✝: Unit → αeq: Thunk.get { fn := fn✝ } = Thunk.get b{ fn := fn✝ } = b
α: Type ua, b: Thunk αeq: Thunk.get a = Thunk.get ba = bhave ⟨_⟩ := b: Thunk αbα: Type ua, b: Thunk αfn✝¹, fn✝: Unit → αeq: Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }{ fn := fn✝¹ } = { fn := fn✝ }
α: Type ua, b: Thunk αeq: Thunk.get a = Thunk.get ba = bcongrα: Type ua, b: Thunk αfn✝¹, fn✝: Unit → αeq: Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }e_fnfn✝¹ = fn✝
α: Type ua, b: Thunk αeq: Thunk.get a = Thunk.get ba = bexact funext: ∀ {α : Sort ?u.385} {β : α → Sort ?u.384} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext fun _: ?m.396_ ↦ eq: Thunk.get { fn := fn✝¹ } = Thunk.get { fn := fn✝ }eqGoals 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.442Thunk α: Type uα) := byGoals accomplished! 🐙
α: Type uinst✝: DecidableEq αDecidableEq (Thunk α)intro a: Thunk αa b: Thunk αbα: Type uinst✝: DecidableEq αa, b: Thunk αDecidable (a = b)
α: Type uinst✝: 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 uinst✝: DecidableEq αa, b: Thunk αDecidable (a = b)byGoals accomplished! 🐙 α: Type uinst✝: DecidableEq αa, b: Thunk αa = b → Thunk.get a = Thunk.get bintro x: a = bxα: Type uinst✝: DecidableEq αa, b: Thunk αx: a = bThunk.get a = Thunk.get b;α: Type uinst✝: DecidableEq αa, b: Thunk αx: a = bThunk.get a = Thunk.get b α: Type uinst✝: DecidableEq αa, b: Thunk αa = b → Thunk.get a = Thunk.get brw [α: Type uinst✝: DecidableEq αa, b: Thunk αx: a = bThunk.get a = Thunk.get bx: a = bxα: Type uinst✝: DecidableEq αa, b: Thunk αx: a = bThunk.get b = Thunk.get b]Goals accomplished! 🐙, α: Type uinst✝: DecidableEq αa, b: Thunk αDecidable (a = b)byGoals accomplished! 🐙 α: Type uinst✝: DecidableEq αa, b: Thunk αThunk.get a = Thunk.get b → a = bintroα: Type uinst✝: DecidableEq αa, b: Thunk αa✝: Thunk.get a = Thunk.get ba = b;α: Type uinst✝: DecidableEq αa, b: Thunk αa✝: Thunk.get a = Thunk.get ba = b α: Type uinst✝: DecidableEq αa, b: Thunk αThunk.get a = Thunk.get b → a = bextα: Type uinst✝: DecidableEq αa, b: Thunk αa✝: Thunk.get a = Thunk.get beqThunk.get a = Thunk.get b;α: Type uinst✝: DecidableEq αa, b: Thunk αa✝: Thunk.get a = Thunk.get beqThunk.get a = Thunk.get b α: Type uinst✝: DecidableEq αa, b: Thunk αThunk.get a = Thunk.get b → a = bassumptionGoals accomplished! 🐙⟩α: Type uinst✝: DecidableEq αa, b: Thunk αthis: a = b ↔ Thunk.get a = Thunk.get bDecidable (a = b)
α: Type uinst✝: DecidableEq αDecidableEq (Thunk α)rw [α: Type uinst✝: DecidableEq αa, b: Thunk αthis: a = b ↔ Thunk.get a = Thunk.get bDecidable (a = b)this: a = b ↔ Thunk.get a = Thunk.get bthisα: Type uinst✝: DecidableEq αa, b: Thunk αthis: a = b ↔ Thunk.get a = Thunk.get bDecidable (Thunk.get a = Thunk.get b)]α: Type uinst✝: DecidableEq αa, b: Thunk αthis: a = b ↔ Thunk.get a = Thunk.get bDecidable (Thunk.get a = Thunk.get b)
α: Type uinst✝: DecidableEq αDecidableEq (Thunk α)infer_instanceGoals 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.657List α: Type ?u.652α ≃ LazyList: Type ?u.658 → Type ?u.658LazyList α: 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 := byGoals accomplished! 🐙
α: Type ?u.652Function.RightInverse toList ofListintro xs: LazyList αxsα: Type ?u.652xs: LazyList αofList (toList xs) = xs
α: Type ?u.652Function.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 tLazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.1677 (fn✝ a)ihα: Type ?u.652nilofList (toList nil) = nilα: Type ?u.652xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.1678 tl✝consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk?m.1678 { fn := fn✝ }
α: Type ?u.652Function.RightInverse toList ofList·α: Type ?u.652nilofList (toList nil) = nil α: Type ?u.652nilofList (toList nil) = nilα: Type ?u.652xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.1678 tl✝consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk?m.1678 { fn := fn✝ }rflGoals accomplished! 🐙
α: Type ?u.652Function.RightInverse toList ofList·α: Type ?u.652xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.1678 tl✝consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝ α: Type ?u.652xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.1678 tl✝consofList (toList (cons hd✝ tl✝)) = cons hd✝ tl✝α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk?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) = ptrue_and]Goals accomplished! 🐙
α: Type ?u.652Function.RightInverse toList ofList·α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ } α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }rw [α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }Thunk.get: {α : Type ?u.1888} → Thunk α → αThunk.get,α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk{ fn := fun x => ofList (toList (Thunk.fn { fn := fn✝ } ())) } = { fn := fn✝ } α: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk{ fn := fun x => ofList (toList (Thunk.get { fn := fn✝ })) } = { fn := fn✝ }ih: ∀ (a : Unit), ?m.1677 (fn✝ a)ihα: Type ?u.652xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), ofList (toList (fn✝ a)) = fn✝ amk{ fn := fun x => fn✝ () } = { fn := fn✝ }]Goals accomplished! 🐙
left_inv := byGoals accomplished! 🐙
α: Type ?u.652LeftInverse toList ofListintro xs: List αxsα: Type ?u.652xs: List αtoList (ofList xs) = xs
α: Type ?u.652LeftInverse toList ofListinduction xs: List αxsα: Type ?u.652niltoList (ofList []) = []α: Type ?u.652head✝: αtail✝: List αtail_ih✝: toList (ofList tail✝) = tail✝constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝
α: Type ?u.652LeftInverse toList ofList·α: Type ?u.652niltoList (ofList []) = [] α: Type ?u.652niltoList (ofList []) = []α: Type ?u.652head✝: αtail✝: List αtail_ih✝: toList (ofList tail✝) = tail✝constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝rflGoals accomplished! 🐙
α: Type ?u.652LeftInverse toList ofList·α: Type ?u.652head✝: αtail✝: List αtail_ih✝: toList (ofList tail✝) = tail✝constoList (ofList (head✝ :: tail✝)) = head✝ :: tail✝ α: Type ?u.652head✝: α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.2016LazyList α: Type uα)
| nil: {α : Type ?u.2035} → LazyList αnil, nil: {α : Type ?u.2038} → LazyList αnil => isTrue: {p : Prop} → p → Decidable pisTrue rfl: ∀ {α : Sort ?u.2056} {a : α}, a = arfl
| 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.2121h : 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 pisFalse h2: ¬Thunk.get xs = Thunk.get ysh2 => byGoals accomplished! 🐙
α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)apply isFalse: {p : Prop} → ¬p → Decidable pisFalseα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysh¬cons x xs = cons y ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysh¬cons x xs = cons y ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysDecidable (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 → ¬bnot_and]α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get yshx = y → ¬xs = ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get yshx = y → ¬xs = ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)intro _: x = y_ xs_ys: xs = ysxs_ysα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysa✝: x = yxs_ys: xs = yshFalse;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysa✝: x = yxs_ys: xs = yshFalse α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)apply h2: ¬Thunk.get xs = Thunk.get ysh2α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysa✝: x = yxs_ys: xs = yshThunk.get xs = Thunk.get ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysa✝: x = yxs_ys: xs = yshThunk.get xs = Thunk.get ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)rw [α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysa✝: x = yxs_ys: xs = yshThunk.get xs = Thunk.get ysxs_ys: xs = ysxs_ysα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: ¬Thunk.get xs = Thunk.get ysa✝: x = yxs_ys: xs = yshThunk.get ys = Thunk.get ys]Goals accomplished! 🐙
| isTrue: {p : Prop} → p → Decidable pisTrue h2: Thunk.get xs = Thunk.get ysh2 => byGoals accomplished! 🐙 α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)apply isTrue: {p : Prop} → p → Decidable pisTrueα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get yshcons x xs = cons y ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get yshcons x xs = cons y ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)congrα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysh.e_tlxs = ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysh.e_tlxs = ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)extα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysh.e_tl.eqThunk.get xs = Thunk.get ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysh.e_tl.eqThunk.get xs = Thunk.get ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: x = yh2: Thunk.get xs = Thunk.get ysDecidable (cons x xs = cons y ys)exact h2: Thunk.get xs = Thunk.get ysh2Goals accomplished! 🐙
else byGoals accomplished! 🐙 α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yDecidable (cons x xs = cons y ys)apply isFalse: {p : Prop} → ¬p → Decidable pisFalseα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yh¬cons x xs = cons y ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yh¬cons x xs = cons y ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yDecidable (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 → ¬bnot_and]α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yhx = y → ¬xs = ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yhx = y → ¬xs = ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yDecidable (cons x xs = cons y ys)introα: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = ya✝: x = yh¬xs = ys;α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = ya✝: x = yh¬xs = ys α: Type uinst✝: DecidableEq αx: αxs: Thunk (LazyList α)y: αys: Thunk (LazyList α)h: ¬x = yDecidable (cons x xs = cons y ys)contradictionGoals accomplished! 🐙
| nil: {α : Type ?u.2278} → LazyList αnil, cons: {α : Type ?u.2280} → α → Thunk (LazyList α) → LazyList αcons _ _ => byGoals accomplished! 🐙 α: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)Decidable (nil = cons hd✝ tl✝)apply isFalse: {p : Prop} → ¬p → Decidable pisFalseα: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)h¬nil = cons hd✝ tl✝;α: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)h¬nil = cons hd✝ tl✝ α: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)Decidable (nil = cons hd✝ tl✝)simpGoals accomplished! 🐙
| cons: {α : Type ?u.2312} → α → Thunk (LazyList α) → LazyList αcons _ _, nil: {α : Type ?u.2317} → LazyList αnil => byGoals accomplished! 🐙 α: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)Decidable (cons hd✝ tl✝ = nil)apply isFalse: {p : Prop} → ¬p → Decidable pisFalseα: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)h¬cons hd✝ tl✝ = nil;α: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)h¬cons hd✝ tl✝ = nil α: Type uinst✝: DecidableEq αhd✝: αtl✝: Thunk (LazyList α)Decidable (cons hd✝ tl✝ = nil)simpGoals 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 um : 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 um] {α: Type uα β: Type uβ : Type u: Type (u+1)Type u} (f: α → m βf : α: Type uα → m: Type u → Type um β: Type uβ) :
LazyList: Type ?u.11390 → Type ?u.11390LazyList α: Type uα → m: Type u → Type um (LazyList: Type ?u.11392 → Type ?u.11392LazyList β: 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 LazyListinstance : Traversable: (Type ?u.19645 → Type ?u.19645) → Type (?u.19645+1)Traversable LazyList: Type ?u.19646 → Type ?u.19646LazyList 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.19663Id _
traverse := @LazyList.traverse: {m : Type ?u.19703 → Type ?u.19703} →
[inst : Applicative m] → {α β : Type ?u.19703} → (α → m β) → LazyList α → m (LazyList β)LazyList.traverse

instance: IsLawfulTraversable LazyListinstance : IsLawfulTraversable: (t : Type ?u.20080 → Type ?u.20080) → [inst : Traversable t] → Type (?u.20080+1)IsLawfulTraversable LazyList: Type ?u.20081 → Type ?u.20081LazyList := byGoals 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 αlistEquivLazyListh₀∀ {α β : Type ?u.20081} (f : α → β), Functor.map f = Equiv.map listEquivLazyList fh₁∀ {α β : Type ?u.20081} (f : β), Functor.mapConst f = (Equiv.map listEquivLazyList ∘ const α) fh₂∀ {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 fh₁∀ {α β : Type ?u.20081} (f : β), Functor.mapConst f = (Equiv.map listEquivLazyList ∘ const α) fh₂∀ {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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f✝: α✝ → F✝ β✝h₂traverse f✝ = Equiv.traverse listEquivLazyList f✝ IsLawfulTraversable LazyList<;>α✝, β✝: Type ?u.20081f✝: α✝ → β✝h₀Functor.map f✝ = Equiv.map listEquivLazyList f✝α✝, β✝: Type ?u.20081f✝: β✝h₁Functor.mapConst f✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f✝: α✝ → F✝ β✝h₂traverse f✝ = Equiv.traverse listEquivLazyList f✝ IsLawfulTraversable LazyListextF✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f✝: α✝ → F✝ β✝x✝: LazyList α✝h₂.htraverse f✝ x✝ = Equiv.traverse listEquivLazyList f✝ x✝ IsLawfulTraversable LazyList<;>α✝, β✝: Type ?u.20081f✝: α✝ → β✝x✝: LazyList α✝h₀.hf✝ <\$> x✝ = Equiv.map listEquivLazyList f✝ x✝α✝, β✝: Type ?u.20081f✝: β✝x✝: LazyList α✝h₁.hFunctor.mapConst f✝ x✝ = (Equiv.map listEquivLazyList ∘ const α✝) f✝ x✝F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f✝: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs
IsLawfulTraversable LazyList·α✝, β✝: Type ?u.20081f: α✝ → β✝xs: LazyList α✝h₀.hf <\$> xs = Equiv.map listEquivLazyList f xs α✝, β✝: Type ?u.20081f: α✝ → β✝xs: LazyList α✝h₀.hf <\$> xs = Equiv.map listEquivLazyList f xsα✝, β✝: Type ?u.20081f: β✝xs: LazyList α✝h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xsF✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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 tLazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.20296 (fn✝ a)ihα✝, β✝: Type ?u.20081f: α✝ → β✝h₀.h.nilf <\$> nil = Equiv.map listEquivLazyList f nilα✝, β✝: Type ?u.20081f: α✝ → β✝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.20081f: α✝ → β✝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.20081f: α✝ → β✝xs: LazyList α✝h₀.hf <\$> xs = Equiv.map listEquivLazyList f xs·α✝, β✝: Type ?u.20081f: α✝ → β✝h₀.h.nilf <\$> nil = Equiv.map listEquivLazyList f nil α✝, β✝: Type ?u.20081f: α✝ → β✝h₀.h.nilf <\$> nil = Equiv.map listEquivLazyList f nilα✝, β✝: Type ?u.20081f: α✝ → β✝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.20081f: α✝ → β✝xs: LazyList α✝fn✝: Unit → LazyList α✝ih: ∀ (a : Unit), f <\$> fn✝ a = Equiv.map listEquivLazyList f (fn✝ a)h₀.h.mk?m.20297 { fn := fn✝ }rflGoals accomplished! 🐙
α✝, β✝: Type ?u.20081f: α✝ → β✝xs: LazyList α✝h₀.hf <\$> xs = Equiv.map listEquivLazyList f xs·α✝, β✝: Type ?u.20081f: α✝ → β✝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.20081f: α✝ → β✝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.20081f: α✝ → β✝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 = gEquiv.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 } = fEquiv.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) = ptrue_and]Goals accomplished! 🐙
α✝, β✝: Type ?u.20081f: α✝ → β✝xs: LazyList α✝h₀.hf <\$> xs = Equiv.map listEquivLazyList f xs·α✝, β✝: Type ?u.20081f: α✝ → β✝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.20081f: α✝ → β✝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.20081f: α✝ → β✝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.20081f: α✝ → β✝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.20081f: α✝ → β✝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)ihGoals accomplished! 🐙
IsLawfulTraversable LazyList·α✝, β✝: Type ?u.20081f: β✝xs: LazyList α✝h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs α✝, β✝: Type ?u.20081f: β✝xs: LazyList α✝h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xsF✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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 = gEquiv.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 } = fEquiv.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.20081f: β✝xs: LazyList α✝h₁.hLazyList.traverse (const α✝ f) xs = ofList (const α✝ f <\$> toList xs)
α✝, β✝: Type ?u.20081f: β✝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 tLazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.21859 (fn✝ a)ihα✝, β✝: Type ?u.20081f: β✝h₁.h.nilLazyList.traverse (const α✝ f) nil = ofList (const α✝ f <\$> toList nil)α✝, β✝: Type ?u.20081f: β✝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.20081f: β✝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.20081f: β✝xs: LazyList α✝h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs·α✝, β✝: Type ?u.20081f: β✝h₁.h.nilLazyList.traverse (const α✝ f) nil = ofList (const α✝ f <\$> toList nil) α✝, β✝: Type ?u.20081f: β✝h₁.h.nilLazyList.traverse (const α✝ f) nil = ofList (const α✝ f <\$> toList nil)α✝, β✝: Type ?u.20081f: β✝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.20081f: β✝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✝ }rflGoals accomplished! 🐙
α✝, β✝: Type ?u.20081f: β✝xs: LazyList α✝h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs·α✝, β✝: Type ?u.20081f: β✝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.20081f: β✝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.20081f: β✝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) = ptrue_and]Goals accomplished! 🐙
α✝, β✝: Type ?u.20081f: β✝xs: LazyList α✝h₁.hFunctor.mapConst f xs = (Equiv.map listEquivLazyList ∘ const α✝) f xs·α✝, β✝: Type ?u.20081f: β✝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.20081f: β✝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.20081f: β✝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.20081f: β✝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.20081f: β✝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)ihGoals accomplished! 🐙
IsLawfulTraversable LazyList·F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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 } = fEquiv.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 = gEquiv.coe_fn_symm_mk]F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝h₂.hLazyList.traverse f xs = ofList <\$> List.traverse f (toList xs)
F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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 tLazyList.rec with _ tl: Thunk (LazyList ?m.23297)tl ih: ?m.23299 tlih _ ih: ∀ (a : Unit), ?m.23298 (fn✝ a)ihF✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝h₂.h.nilLazyList.traverse f nil = ofList <\$> List.traverse f (toList nil)F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝hd✝: α✝tl: Thunk (LazyList α✝)ih: ?m.23299 tlh₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <\$> List.traverse f (toList (cons hd✝ tl))F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs·F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝h₂.h.nilLazyList.traverse f nil = ofList <\$> List.traverse f (toList nil) F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝h₂.h.nilLazyList.traverse f nil = ofList <\$> List.traverse f (toList nil)F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝hd✝: α✝tl: Thunk (LazyList α✝)ih: ?m.23299 tlh₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <\$> List.traverse f (toList (cons hd✝ tl))F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝h₂.h.nilLazyList.traverse f nil = pure (ofList []);F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝h₂.h.nilLazyList.traverse f nil = pure (ofList []) F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝h₂.h.nilLazyList.traverse f nil = ofList <\$> List.traverse f (toList nil)rflGoals accomplished! 🐙
F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs·F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝hd✝: α✝tl: Thunk (LazyList α✝)ih: ?m.23299 tlh₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <\$> List.traverse f (toList (cons hd✝ tl)) F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝hd✝: α✝tl: Thunk (LazyList α✝)ih: ?m.23299 tlh₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <\$> List.traverse f (toList (cons hd✝ tl))F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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 tlihF✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝hd✝: α✝tl: Thunk (LazyList α✝)ih: ?m.23299 tlh₂.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 tlih, 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) <\$> xFunctor.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 => yseq_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 => ymap_seq]F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝hd✝: α✝tl: Thunk (LazyList α✝)ih: ?m.23299 tlh₂.h.consLazyList.traverse f (cons hd✝ tl) = ofList <\$> List.traverse f (toList (cons hd✝ tl))·F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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))rflGoals accomplished! 🐙
F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → F✝ β✝xs: LazyList α✝h₂.htraverse f xs = Equiv.traverse listEquivLazyList f xs·F✝: Type ?u.20081 → Type ?u.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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.20081inst✝¹: Applicative F✝inst✝: LawfulApplicative F✝α✝, β✝: Type ?u.20081f: α✝ → 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)ihGoals 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.25676LazyList α: ?m.25672α → LazyList: Type ?u.25678 → Type ?u.25678LazyList α: ?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.25718xs' := xs: Thunk (LazyList α)xs.get: {α : Type ?u.25719} → Thunk α → αget
match xs': ?m.25718xs' 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.25718xs')
#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: α → Propp : α: ?m.34566α → Prop: TypeProp) [DecidablePred: {α : Sort ?u.34573} → (α → Prop) → Sort (max1?u.34573)DecidablePred p: α → Propp] : LazyList: Type ?u.34584 → Type ?u.34584LazyList α: ?m.34566α → Option: Type ?u.34586 → Type ?u.34586Option α: ?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: α → Propp 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: α → Propp
#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.42510LazyList α: ?m.42506α → LazyList: Type ?u.42513 → Type ?u.42513LazyList α: ?m.42506α → LazyList: Type ?u.42515 → Type ?u.42515LazyList α: ?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.52566List (LazyList: Type ?u.52567 → Type ?u.52567LazyList α: ?m.52562α) → LazyList: Type ?u.52569 → Type ?u.52569LazyList α: ?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.52848LazyList α: ?m.52841α → (α: ?m.52841α → LazyList: Type ?u.52853 → Type ?u.52853LazyList β: ?m.52844β) → LazyList: Type ?u.52855 → Type ?u.52855LazyList β: ?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.61945LazyList α: ?m.61942α) : LazyList: Type ?u.61948 → Type ?u.61948LazyList α: ?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 LazyListinstance : Monad: (Type ?u.61990 → Type ?u.61989) → Type (max(?u.61990+1)?u.61989)Monad LazyList: Type ?u.61991 → Type ?u.61991LazyList 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) = xsappend_nil {α: Type u_1α} (xs: LazyList αxs : LazyList: Type ?u.62778 → Type ?u.62778LazyList α: ?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 := byGoals accomplished! 🐙
α: Type u_1xs: 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 tLazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.62824 (fn✝ a)ihα: Type u_1nilappend nil (Thunk.pure nil) = nilα: Type u_1xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.62825 tl✝consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk?m.62825 { fn := fn✝ }
α: Type u_1xs: LazyList αappend xs (Thunk.pure nil) = xs·α: Type u_1nilappend nil (Thunk.pure nil) = nil α: Type u_1nilappend nil (Thunk.pure nil) = nilα: Type u_1xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.62825 tl✝consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk?m.62825 { fn := fn✝ }rflGoals accomplished! 🐙
α: Type u_1xs: LazyList αappend xs (Thunk.pure nil) = xs·α: Type u_1xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.62825 tl✝consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝ α: Type u_1xs: LazyList αhd✝: αtl✝: Thunk (LazyList α)tl_ih✝: ?m.62825 tl✝consappend (cons hd✝ tl✝) (Thunk.pure nil) = cons hd✝ tl✝α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk?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) = ptrue_and]Goals accomplished! 🐙
α: Type u_1xs: LazyList αappend xs (Thunk.pure nil) = xs·α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk{ fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ } α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk{ fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }extα: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk.eqThunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ };α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk.eqThunk.get { fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = Thunk.get { fn := fn✝ } α: Type u_1xs: LazyList αfn✝: Unit → LazyList αih: ∀ (a : Unit), append (fn✝ a) (Thunk.pure nil) = fn✝ amk{ fn := fun x => append (Thunk.get { fn := fn✝ }) (Thunk.pure nil) } = { fn := fn✝ }apply ih: ∀ (a : Unit), ?m.62824 (fn✝ a)ihGoals accomplished! 🐙
#align lazy_list.append_nil LazyList.append_nil: ∀ {α : Type u_1} (xs : LazyList α), append xs (Thunk.pure nil) = xsLazyList.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.63490LazyList α: ?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) := byGoals accomplished! 🐙
α: Type u_1xs, 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 tLazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.66087 (fn✝ a)ihα: Type u_1ys, 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_1xs, 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_1xs, 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_1xs, 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_1ys, 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_1ys, 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_1xs, 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_1xs, 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✝ }rflGoals accomplished! 🐙
α: Type u_1xs, 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_1xs, 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_1xs, 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_1xs, 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) = ptrue_and]Goals accomplished! 🐙
α: Type u_1xs, 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_1xs, 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_1xs, 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_1xs, 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_1xs, 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_1xs, 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)ihGoals 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.66434LazyList α: ?m.66428α) (ys: Thunk (LazyList α)ys : Thunk: Type ?u.66437 → Type ?u.66437Thunk (LazyList: Type ?u.66438 → Type ?u.66438LazyList α: ?m.66428α)) (f: α → LazyList βf : α: ?m.66428α → LazyList: Type ?u.66443 → Type ?u.66443LazyList β: ?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) := byGoals accomplished! 🐙
α: Type u_1β: Type u_2xs: 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_2xs: 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_2xs: 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_2xs: 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 }rflGoals accomplished! 🐙
α: Type u_1β: Type u_2xs: 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_2xs✝: 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_2xs: 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_2xs✝: 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_2xs✝: 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_2xs✝: 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_2xs✝: 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.68299thisα: Type u_1β: Type u_2xs✝: 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_2xs✝: 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_2xs✝: 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_2xs✝: 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_2xs✝: 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_2xs✝: 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 LazyListinstance : LawfulMonad: (m : Type ?u.76376 → Type ?u.76375) → [inst : Monad m] → PropLawfulMonad LazyList: Type ?u.76377 → Type ?u.76377LazyList := 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✝⁴ →
(bind_pure_comp := byGoals 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.76377f: α✝ → β✝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.76377f: α✝ → β✝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 tLazyList.rec with _ _ _ _ ih: ∀ (a : Unit), ?m.77773 (fn✝ a)ihα✝, β✝: Type ?u.76377f: α✝ → β✝nil(LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nilα✝, β✝: Type ?u.76377f: α✝ → β✝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.76377f: α✝ → β✝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.76377f: α✝ → β✝nil(LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nil α✝, β✝: Type ?u.76377f: α✝ → β✝nil(LazyList.bind nil fun y => cons (f y) (Thunk.pure nil)) = LazyList.traverse f nilα✝, β✝: Type ?u.76377f: α✝ → β✝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.76377f: α✝ → β✝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✝ }rflGoals accomplished! 🐙
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
(do
let y ← x
pure (f y)) =     f <\$> x·α✝, β✝: Type ?u.76377f: α✝ → β✝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.76377f: α✝ → β✝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.76377f: α✝ → β✝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 xId.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) = ptrue_and]α✝, β✝: Type ?u.76377f: α✝ → β✝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.76377f: α✝ → β✝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.76377f: α✝ → β✝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✝)congrGoals accomplished! 🐙
∀ {α β : Type ?u.76377} (f : α → β) (x : LazyList α),
(do
let y ← x
pure (f y)) =     f <\$> x·α✝, β✝: Type ?u.76377f: α✝ → β✝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.76377f: α✝ → β✝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.76377f: α✝ → β✝xs: LazyList α✝fn✝: Unit → LazyList α✝ih: ∀ (a : Unit), (LazyList.bind (fn✝ a) fun y => cons (f y) (Thunk.pure nil)<```