awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val : Option (α × WSeq α)
⊢ match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    Sum.inl val, Sum.inl val with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val : Computation (Option (α × WSeq α))
⊢ match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    Sum.inr val, Sum.inr val with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c' : Computation (WSeq α)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c'.think).destruct.destruct (c'.think.bind destruct).destruct

Tactic:
simpa using Or.inr ⟨c', rfl, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
pure :
  ∀ (a : WSeq α),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
      (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct
think :
  ∀ (c' : Computation (WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
      (flatten c'.think).destruct.destruct (c'.think.bind destruct).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c).destruct.destruct (c.bind destruct).destruct

Tactic:
induction c using Computation.recOn with
      | pure a => simp; cases (destruct a).destruct <;> simp
      | think c' => simpa using Or.inr ⟨c', rfl, rfl⟩

Premises used: Stream'.pure, Stream'.WSeq.think, Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    c1.destruct c2.destruct

Tactic:
exact
    match c1, c2, h with
    | c, _, Or.inl rfl => by cases c.destruct <;> simp
    | _, _, Or.inr ⟨c, rfl, rfl⟩ => by
      induction c using Computation.recOn with
      | pure a => simp; cases (destruct a).destruct <;> simp
      | think c' => simpa using Or.inr ⟨c', rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ s.head.Terminates ↔ s.destruct.Terminates

Tactic:
terminates_map_iff _ (destruct s)

Premises used: Computation.terminates_map_iff, Stream'.WSeq.destruct, Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := WSeq α) (tail nil) nil

Tactic:
simp [tail]

Premises used: Stream'.WSeq.tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).tail = s

Tactic:
simp [tail]

Premises used: Stream'.WSeq.tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ s.think.tail = s.tail.think

Tactic:
simp [tail]

Premises used: Stream'.WSeq.tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
n : ℕ
zero : Eq.{u + 1} (α := WSeq α) (drop nil 0) nil
succ : ∀ (n : ℕ), Eq.{u + 1} (α := WSeq α) (drop nil n) nil → Eq.{u + 1} (α := WSeq α) (drop nil (n + 1)) nil
⊢ Eq.{u + 1} (α := WSeq α) (drop nil n) nil

Tactic:
induction n
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := WSeq α) (drop nil 0) nil

Tactic:
simp [*, drop]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
n : ℕ
h : Eq.{u + 1} (α := WSeq α) (drop nil n) nil
⊢ Eq.{u + 1} (α := WSeq α) (drop nil (n + 1)) nil

Tactic:
simp [*, drop]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).drop (HAdd.hAdd (α := ℕ) 0 1) = s.drop 0

Tactic:
simp [drop]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
n : ℕ
n_ih : (cons a s).drop (n + 1) = s.drop n
⊢ (cons a s).drop (n + 1 + 1) = s.drop (n + 1)

Tactic:
simp [drop, ← n_ih]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
n : ℕ
zero : (cons a s).drop (HAdd.hAdd (α := ℕ) 0 1) = s.drop 0
succ : ∀ (n : ℕ) (n_ih : (cons a s).drop (n + 1) = s.drop n), (cons a s).drop (n + 1 + 1) = s.drop (n + 1)
⊢ (cons a s).drop (n + 1) = s.drop n

Tactic:
induction n with
  | zero => simp [drop]
  | succ n n_ih =>
    simp [drop, ← n_ih]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
zero : s.think.drop 0 = (s.drop 0).think
succ : ∀ (n : ℕ), s.think.drop n = (s.drop n).think → s.think.drop (n + 1) = (s.drop (n + 1)).think
⊢ s.think.drop n = (s.drop n).think

Tactic:
induction n
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ s.think.drop 0 = (s.drop 0).think

Tactic:
simp [*, drop]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
h : s.think.drop n = (s.drop n).think
⊢ s.think.drop (n + 1) = (s.drop (n + 1)).think

Tactic:
simp [*, drop]

Premises used: Stream'.WSeq.drop
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
rw : s.tail.drop n = s.drop (1 + n)
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
rw [Nat.add_comm]

Premises used: Nat.add_comm
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
symm : s.drop (1 + n) = s.tail.drop n
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
symm
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ s.drop (1 + n) = s.tail.drop n

Tactic:
apply dropn_add

Premises used: Stream'.WSeq.dropn_add
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
m n : ℕ
⊢ s.get? (m + n) = (s.drop m).get? n

Tactic:
congr_arg head (dropn_add _ _ _)

Premises used: Stream'.WSeq.get?, congr_arg, Stream'.WSeq.dropn_add, Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.get? n = s.get? (n + 1)

Tactic:
congr_arg head (dropn_tail _ _)

Premises used: Stream'.WSeq.get?, congr_arg, Stream'.WSeq.dropn_tail, Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := WSeq α) (join nil) nil

Tactic:
Seq.join_nil

Premises used: Stream'.WSeq.join, Stream'.Seq.map, Stream'.Seq.nil, Stream'.map, Stream'.WSeq, Stream'.WSeq.nil, Stream'.Seq.join_nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
⊢ Eq (α := WSeq α)
    (Seq.join
      (Seq.map
        (fun (o : Option (WSeq α)) ↦
          match (motive := Option (WSeq α) → Seq1 (Option α)) o with
          | none => Seq1.ret none
          | some s => (none, s))
        (Seq.cons none S)))
    (Seq.cons none
      (Seq.join
        (Seq.map
          (fun (o : Option (WSeq α)) ↦
            match (motive := Option (WSeq α) → Seq1 (Option α)) o with
            | none => Seq1.ret none
            | some s => (none, s))
          S)))

Tactic:
simp [Seq1.ret]

Premises used: Stream'.Seq1.ret
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ Seq.join
      (Seq.map
        (fun (o : Option (WSeq α)) ↦
          match (motive := Option (WSeq α) → Seq1 (Option α)) o with
          | none => Seq1.ret none
          | some s => (none, s))
        (cons s S)) =
    Seq.cons none
      (s.append
        (Seq.join
          (Seq.map
            (fun (o : Option (WSeq α)) ↦
              match (motive := Option (WSeq α) → Seq1 (Option α)) o with
              | none => Seq1.ret none
              | some s => (none, s))
            S)))

Tactic:
simp [cons, append]

Premises used: Stream'.WSeq.cons, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ append nil s = s

Tactic:
Seq.nil_append _

Premises used: Stream'.WSeq, Stream'.WSeq.nil, Stream'.Seq.nil_append, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s t : WSeq α
⊢ (cons a s).append t = cons a (s.append t)

Tactic:
Seq.cons_append _ _ _

Premises used: Stream'.WSeq.cons, Stream'.WSeq, Stream'.Seq.cons_append, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t : WSeq α
⊢ s.think.append t = (s.append t).think

Tactic:
Seq.cons_append _ _ _

Premises used: Stream'.WSeq.think, Stream'.WSeq, Stream'.Seq.cons_append, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ s.append nil = s

Tactic:
Seq.append_nil _

Premises used: Stream'.Seq.append_nil, Stream'.WSeq, Stream'.WSeq.nil, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t u : WSeq α
⊢ (s.append t).append u = s.append (t.append u)

Tactic:
Seq.append_assoc _ _ _

Premises used: Stream'.Seq.append_assoc, Stream'.WSeq, Stream'.WSeq.append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
simp :
  (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o) <$>
        s.destruct >>=
      destruct =
    s.destruct >>= tail.aux
⊢ s.tail.destruct = s.destruct >>= tail.aux

Tactic:
simp only [tail, destruct_flatten]

Premises used: Stream'.WSeq.tail, Stream'.WSeq.destruct_flatten
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
rw :
  (s.destruct >>= fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α)))) =
    s.destruct >>= tail.aux
⊢ (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o) <$>
        s.destruct >>=
      destruct =
    s.destruct >>= tail.aux

Tactic:
rw [← bind_pure_comp, LawfulMonad.bind_assoc]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
h :
  Eq.{u + 1} (α := (x : Option (α × WSeq α)) → Computation (Option (α × WSeq α)))
    (fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α))))
    tail.aux
⊢ (s.destruct >>= fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α)))) =
    s.destruct >>= tail.aux

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
h :
  Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
    (Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))))
    (tail.aux none)
h₁ :
  ∀ (a : α) (s : WSeq α),
    Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α))) =
      tail.aux (some (a, s))
⊢ Eq.{u + 1} (α := (x : Option (α × WSeq α)) → Computation (Option (α × WSeq α)))
    (fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α))))
    tail.aux

Tactic:
ext1 (_ | ⟨a, s⟩)
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
apply :
  Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (tail.aux none)
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
    (Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))))
    (tail.aux none)

Tactic:
apply (@pure_bind Computation _ _ _ _ _ _).trans _

Premises used: LawfulMonad.pure_bind, Eq.trans
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
a : α
s : WSeq α
apply :
  destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) =
    tail.aux (some (a, s))
⊢ Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))) =
    tail.aux (some (a, s))

Tactic:
apply (@pure_bind Computation _ _ _ _ _ _).trans _

Premises used: LawfulMonad.pure_bind, Eq.trans
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (tail.aux none)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
a : α
s : WSeq α
⊢ destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) =
    tail.aux (some (a, s))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
n : ℕ
rw : Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (aux n none) (Computation.pure none)
rw₁ rw₂ : Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (Computation.pure none) (Computation.pure none)
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (Computation.bind (Computation.pure none) (aux n))
    (Computation.pure none)

Tactic:
rw [ret_bind, drop.aux_none n]

Premises used: Computation.ret_bind
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
rw : (s.destruct >>= fun (x : Option (α × WSeq α)) ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)
⊢ (s.drop (n + 1)).destruct = s.destruct >>= drop.aux (n + 1)

Tactic:
rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]

Premises used: LawfulMonad.bind_assoc, Stream'.WSeq.dropn_tail, Stream'.WSeq.destruct_tail
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun (x : Option (α × WSeq α)) ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
rcases : ∀ (a : Option (α × WSeq α)) (h : a ∈ s.tail.destruct), s.destruct.Terminates
⊢ s.destruct.Terminates

Tactic:
rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩

Premises used: Stream'.WSeq.head_terminates_iff, Iff.mp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ Membership.mem (γ := Computation (Option (α × WSeq α)))
    (do
      let a ← s.destruct
      destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
    a

Tactic:
simp only [tail, destruct_flatten, bind_map_left] at h

Premises used: bind_map_left, Stream'.WSeq.tail, Stream'.WSeq.destruct_flatten
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ Membership.mem (γ := Computation (Option (α × WSeq α)))
    (do
      let a ← s.destruct
      destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
    a

Tactic:
simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h

Premises used: bind_map_left, Stream'.WSeq.tail, Stream'.WSeq.destruct_flatten
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (do
      let a ← s.destruct
      destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
    a
rcases :
  ∀ (s' : Option (α × WSeq α)) (h1 : s' ∈ s.destruct),
    Membership.mem (γ := Computation (Option (α × WSeq α)))
        (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd s')) a →
      s.destruct.Terminates
⊢ s.destruct.Terminates

Tactic:
rcases exists_of_mem_bind h with ⟨s', h1, _⟩

Premises used: Computation.exists_of_mem_bind
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (do
      let a ← s.destruct
      destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
    a
s' : Option (α × WSeq α)
h1 : s' ∈ s.destruct
right :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd s')) a
⊢ s.destruct.Terminates

Tactic:
terminates_of_mem h1

Premises used: Computation.terminates_of_mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (do
      let a ← s.destruct
      destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
    a
s' : Option (α × WSeq α)
h1 : s' ∈ s.destruct
right :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd s')) a
⊢ s.destruct.Terminates

Tactic:
exact terminates_of_mem h1

Premises used: Computation.terminates_of_mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct
      (flatten
        ((Applicative.toFunctor : Functor Computation).1
          (fun (o : Option (α × WSeq α)) ↦
            Option.recOn (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) o nil Prod.snd)
          s.destruct)))
    (some a)
⊢ Membership.mem (γ := Computation (Option (α × WSeq α)))
    ((Applicative.toFunctor : Functor Computation).1
        (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
        s.destruct >>=
      destruct)
    (some a)

Tactic:
simp only [destruct_flatten] at h

Premises used: Stream'.WSeq.destruct_flatten
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    ((Applicative.toFunctor : Functor Computation).1
        (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
        s.destruct >>=
      destruct)
    (some a)
rcases :
  ∀ (t : WSeq α)
    (tm :
      Membership.mem (γ := Computation (WSeq α))
        ((Applicative.toFunctor : Functor Computation).1
          (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
          s.destruct)
        t)
    (td : some a ∈ t.destruct), ∃ (a' : α × WSeq α), some a' ∈ s.destruct
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct

Tactic:
rcases exists_of_mem_bind h with ⟨t, tm, td⟩

Premises used: Computation.exists_of_mem_bind
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm :
  Membership.mem (γ := Computation (WSeq α))
    ((Applicative.toFunctor : Functor Computation).1
      (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      s.destruct)
    t
td : some a ∈ t.destruct
rcases :
  ∀ (t' : Option (α × WSeq α)) (ht' : t' ∈ s.destruct)
    (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd t' = t),
    ∃ (a' : α × WSeq α), some a' ∈ s.destruct
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct

Tactic:
rcases Computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : Option.some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd t' = t
none :
  ∀ (ht' : Option.none ∈ s.destruct)
    (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd Option.none = t),
    ∃ (a' : α × WSeq α), Option.some a' ∈ s.destruct
some :
  ∀ (t' : α × WSeq α) (ht' : Option.some t' ∈ s.destruct)
    (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (Option.some t') = t),
    ∃ (a' : α × WSeq α), Option.some a' ∈ s.destruct
⊢ ∃ (a' : α × WSeq α), Option.some a' ∈ s.destruct

Tactic:
rcases t' with - | t'
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
⊢ Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (some a)

Tactic:
rw [← ht2] at td
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
td₁ :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (some a)
⊢ none ∈ s.destruct

Tactic:
rw [← ht2] at td
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
td₁ :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (some a)
ht'₁ : none ∈ s.destruct
⊢ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t

Tactic:
rw [← ht2] at td
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : α × WSeq α
ht' : some t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t
⊢ Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t'))) (some a)

Tactic:
rw [← ht2] at td