awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a, s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct

Tactic:
⟨_, om⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a, s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct

Tactic:
exact ⟨_, om⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ s.head.Terminates

Tactic:
let ⟨_, h⟩ := exists_get?_of_mem h
  head_terminates_of_get?_terminates ⟨⟨_, h⟩⟩

Premises used: Computation.Terminates.mk, Stream'.WSeq.exists_get?_of_mem, Option.some, Computation.Terminates, _private.0.Stream'.WSeq.exists_dropn_of_mem.match_1, Exists.intro, Stream'.WSeq.head, Stream'.WSeq.head_terminates_of_get?_terminates
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s₁ s₂ : WSeq α
a : α
⊢ a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂

Tactic:
Seq.of_mem_append

Premises used: Stream'.Seq.of_mem_append, Stream'.WSeq.append, Stream'.WSeq.Mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s₁ s₂ : WSeq α
a : α
⊢ a ∈ s₁ → a ∈ s₁.append s₂

Tactic:
Seq.mem_append_left

Premises used: Stream'.Seq.mem_append_left, Stream'.WSeq.append, Stream'.WSeq.Mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
let :
  ∀ (o : Option α) (om : o ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
    (oe : Option.map f o = some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b

Tactic:
let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
o : Option α
om : o ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
oe : Option.map f o = Option.some b
none :
  ∀ (om : Option.none ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
    (oe : Option.map f Option.none = Option.some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
some :
  ∀ (a : α) (om : Option.some a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
    (oe : Option.map f (Option.some a) = Option.some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b

Tactic:
rcases o with - | a
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
om : none ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
oe : Option.map f none = some b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b

Tactic:
injection oe
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
a : α
om : some a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
oe : Option.map f (some a) = some b
⊢ f a = b

Tactic:
injection oe with h'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
a : α
om : some a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
h' : f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b

Tactic:
⟨a, om, h'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
a : α
om : some a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
h' : f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b

Tactic:
exact ⟨a, om, h'⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := WSeq α) (↑[] : WSeq α) nil

Tactic:
rfl

Premises used: Stream'.WSeq.ofList, Stream'.Seq.map, Stream'.WSeq.ofSeq, Stream'.Seq.nil, Stream'.map, Stream'.WSeq.nil, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
l : List α
⊢ Seq.map some (↑(a :: l) : Seq α) = Seq.cons (some a) (Seq.map some (↑l : Seq α))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
⊢ Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, nil) =
    Computation.pure l.reverse

Tactic:
destruct_eq_pure rfl

Premises used: Computation.destruct_eq_pure, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s : WSeq α
a : α
⊢ Eq (α := List α ⊕ Computation (List α))
    (Computation.destruct
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, cons a s)))
    (Sum.inr
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (a :: l, s)))

Tactic:
simp [cons]

Premises used: Stream'.WSeq.cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s : WSeq α
⊢ Eq (α := List α ⊕ Computation (List α))
    (Computation.destruct
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s.think)))
    (Sum.inr
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l, s)))

Tactic:
simp [think]

Premises used: Stream'.WSeq.think
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s : WSeq α
⊢ Eq (α := Computation (List α))
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, s))
    ((fun (x : List α) ↦ l.reverse ++ x) <$> s.toList)

Tactic:
Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l' : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨l, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a::l, s')) (l' ++ l, s) ∧
            c2 = Computation.map (l.reverse ++ ·) (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l', s)))
      ?_ ⟨[], s, rfl, rfl⟩

Premises used: Computation.corec, Exists, Prod.mk, And, Computation.map, And.intro, Exists.intro, List.reverse, Computation.eq_of_bisim, Eq, HAppend.hAppend, rfl, List.nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s : WSeq α
c1 :
  Computation.IsBisimulation.{u} (α := List α) fun (c1 c2 : Computation (List α)) ↦
    ∃ (l' : List α) (s : WSeq α),
      c1 =
          Computation.corec
            (fun (x : List α × WSeq α) ↦
              match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
              | (l, s) =>
                match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l' ++ l, s) ∧
        c2 =
          Computation.map (fun (x : List α) ↦ l.reverse ++ x)
            (Computation.corec
              (fun (x : List α × WSeq α) ↦
                match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                | (l, s) =>
                  match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                  | none => Sum.inl l.reverse
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l', s))
⊢ Eq (α := Computation (List α))
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, s))
    ((fun (x : List α) ↦ l.reverse ++ x) <$> s.toList)

Tactic:
refine
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l' : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨l, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a::l, s')) (l' ++ l, s) ∧
            c2 = Computation.map (l.reverse ++ ·) (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l', s)))
      ?_ ⟨[], s, rfl, rfl⟩

Premises used: Computation.corec, Exists, Prod.mk, And, Computation.map, And.intro, Exists.intro, List.reverse, Computation.eq_of_bisim, Eq, HAppend.hAppend, rfl, List.nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s_1 : WSeq α
s1 s2 : Computation (List α)
l' : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s) ∧
    s2 =
      Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))
⊢ Eq (α := Computation (List α))
    (Computation.tail
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s)))
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (a :: l' ++ l, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s_1 : WSeq α
s1 s2 : Computation (List α)
l' : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s) ∧
    s2 =
      Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))
⊢ Eq (α := Computation (List α))
    (Computation.tail
      (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))))
    (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (a :: l', s)))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s_1 : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s.think) ∧
    s2 =
      Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s.think))
⊢ Eq (α := Computation (List α))
    (Computation.tail
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s.think)))
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l' ++ l, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
l : List α
s_1 : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s.think) ∧
    s2 =
      Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s.think))
⊢ Eq (α := Computation (List α))
    (Computation.tail
      (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s.think))))
    (Computation.map (fun (x : List α) ↦ l.reverse ++ x)
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l', s)))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
simp :
  Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1.reverse
        | some (none, s') => Sum.inr (x.1, s')
        | some (some a, s') => Sum.inr (a :: x.1, s'))
      ([a], s) =
    List.cons a <$>
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        ([], s)
⊢ Computation.destruct
      (Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
          | (l, s) =>
            match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        ([], cons a s)) =
    Sum.inr
      (List.cons a <$>
        Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          ([], s))

Tactic:
simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]

Premises used: Sum.inr.injEq, Stream'.WSeq.toList'_cons, Computation.destruct_think
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
rw :
  (fun (x : List α) ↦ [a].reverse ++ x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        ([], s)
⊢ Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1.reverse
        | some (none, s') => Sum.inr (x.1, s')
        | some (some a, s') => Sum.inr (a :: x.1, s'))
      ([a], s) =
    List.cons a <$>
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        ([], s)

Tactic:
rw [toList'_map]

Premises used: Stream'.WSeq.toList'_map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
⊢ (fun (x : List α) ↦ a :: x) <$> s.toList =
    List.cons a <$>
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        ([], s)

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Computation (List α)) (toList nil) (Computation.pure [])

Tactic:
destruct_eq_pure rfl

Premises used: Computation.destruct_eq_pure, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Membership.mem (γ := Computation (List α)) (toList (↑[] : WSeq α)) []

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
l : List α
IH : l ∈ (↑l : WSeq α).toList
⊢ a :: l ∈ (↑(a :: l) : WSeq α).toList

Tactic:
simpa [ret_mem] using think_mem (Computation.mem_map _ IH)

Premises used: Computation.think_mem, Computation.mem_map, Computation.ret_mem