awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
h₁ : ∀ (s : WSeq α) (sS : s ∈ S) (as : a ∈ s), ∃ s ∈ S.think, a ∈ s
⊢ ∃ s ∈ S.think, a ∈ s

Tactic:
rcases (IH nil S (by simp) (by simp [m])).resolve_left (notMem_nil _) with ⟨s, sS, as⟩

Premises used: Or.resolve_left, Stream'.WSeq.notMem_nil, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ s ∈ S.think

Tactic:
simp [sS]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
s : WSeq α
sS : s ∈ S
as : a ∈ s
⊢ ∃ s ∈ S.think, a ∈ s

Tactic:
exact ⟨s, by simp [sS], as⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq (WSeq α)
m : a ∈ append nil s.think.join
IH : ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
ej : s.join.think = s.join.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1

Tactic:
case think S =>
      apply Or.inr
      replace m : a ∈ S.join := by simpa using m
      rcases (IH nil S (by simp) (by simp [m])).resolve_left (notMem_nil _) with ⟨s, sS, as⟩
      exact ⟨s, by simp [sS], as⟩

Premises used: Stream'.WSeq.think, Or.inr
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
h2 : ∀ (m : a ∈ s.append S.join), a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp only [think_append, mem_think] at m IH ⊢

Premises used: Stream'.WSeq.mem_think, Stream'.WSeq.think_append
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
m : a ∈ s.append S.join
⊢ a ∈ s ∨ ∃ s ∈ S, a ∈ s

Tactic:
apply IH _ _ rfl m

Premises used: rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
s : WSeq α
f : α → WSeq β
b : β
h : b ∈ s.bind f
t : WSeq β
tm : t ∈ map f s
bt : b ∈ t
a : α
as : a ∈ s
e : f a = t
rwa rwa₁ rwa₂ rwa₃ : b ∈ t
⊢ b ∈ f a

Tactic:
rwa [e]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
bisim :
  Computation.IsBisimulation.{v} (α := Option (β × WSeq β)) fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
    ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
r :
  ∃ (s_1 : WSeq α),
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct
⊢ (map f s).destruct = Computation.map (Option.map (Prod.map f (map f))) s.destruct

Tactic:
apply
    Computation.eq_of_bisim fun c1 c2 =>
      ∃ s,
        c1 = destruct (map f s) ∧
          c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)

Premises used: Stream'.WSeq.destruct, Exists, Prod.map, Option.map, And, Computation.map, Stream'.WSeq.map, Computation.eq_of_bisim, Eq
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
bisim :
  ∀ (s : WSeq α) (h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      c1.destruct c2.destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct

Tactic:
obtain ⟨s, h⟩ := h
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
bisim :
  BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct

Tactic:
rw [h.left, h.right]

Premises used: And.right, And.left
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
induction :
  ∀ (h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct nil)),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct nil)).destruct
induction₁ :
  ∀ (x : α) (s : WSeq α)
    (h : c1 = (map f (cons x s)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x s).destruct),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      (map f (cons x s)).destruct.destruct
      (Computation.map (Option.map (Prod.map f (map f))) (cons x s).destruct).destruct
bisim :
  ∀ (s : WSeq α)
    (h : c1 = (map f s.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.think.destruct),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      (map f s.think).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.think.destruct).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct nil)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct nil)).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
x : α
s_1 : WSeq α
h : c1 = (map f (cons x s_1)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x s_1).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f (cons x s_1)).destruct.destruct
    (Computation.map (Option.map (Prod.map f (map f))) (cons x s_1).destruct).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.think.destruct
⊢ (map f s.think).destruct.tail = (map f s).destruct ∧
    (Computation.map (Option.map (Prod.map f (map f))) s.think.destruct).tail =
      Computation.map (Option.map (Prod.map f (map f))) s.destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.think.destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s.think).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.think.destruct).destruct

Tactic:
exact ⟨s, by simp⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ (s_1 : WSeq α),
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct

Tactic:
⟨s, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ (s_1 : WSeq α),
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct

Tactic:
exact ⟨s, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t : WSeq α
c1 :
  Computation.IsBisimulation.{u} (α := Option (α × WSeq α)) fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ (s.append t).destruct = s.destruct.bind (destruct_append.aux t)

Tactic:
apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ s t, c1 = destruct (append s t) ∧ c2 = (destruct s).bind (destruct_append.aux t))
      _ ⟨s, t, rfl, rfl⟩

Premises used: Stream'.WSeq.destruct, Exists, Stream'.WSeq.destruct_append.aux, And, And.intro, Exists.intro, Computation.eq_of_bisim, Computation.bind, Eq, Stream'.WSeq.append, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
rcases :
  ∀ (s t : WSeq α) (h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      c1.destruct c2.destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct

Tactic:
rcases h with ⟨s, t, h⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
rw :
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct

Tactic:
rw [h.left, h.right]

Premises used: And.right, And.left
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
induction :
  ∀ (h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct
induction₁ :
  ∀ (x : α) (s : WSeq α)
    (h : c1 = ((cons x s).append t).destruct ∧ c2 = (cons x s).destruct.bind (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      ((cons x s).append t).destruct.destruct ((cons x s).destruct.bind (destruct_append.aux t)).destruct
think :
  ∀ (s : WSeq α) (h : c1 = (s.think.append t).destruct ∧ c2 = s.think.destruct.bind (destruct_append.aux t)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (s.think.append t).destruct.destruct (s.think.destruct.bind (destruct_append.aux t)).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.append t).destruct.destruct (s.destruct.bind (destruct_append.aux t)).destruct

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
induction :
  ∀ (h : c1 = destruct (append nil nil) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux nil)),
    BisimO.{u} (α := Option (α × WSeq α))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (Computation.destruct (destruct (append nil nil)))
      (Computation.destruct (Computation.bind (destruct nil) (destruct_append.aux nil)))
induction₁ :
  ∀ (x : α) (s : WSeq α)
    (h : c1 = (append nil (cons x s)).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux (cons x s))),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (append nil (cons x s)).destruct.destruct
      (Computation.bind (destruct nil) (destruct_append.aux (cons x s))).destruct
think :
  ∀ (s : WSeq α)
    (h : c1 = (append nil s.think).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux s.think)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
      (append nil s.think).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux s.think)).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct

Tactic:
induction t using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = destruct (append nil nil) ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux nil)
⊢ BisimO.{u} (α := Option (α × WSeq α))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (Computation.destruct (destruct (append nil nil)))
    (Computation.destruct (Computation.bind (destruct nil) (destruct_append.aux nil)))

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
x : α
s_1 : WSeq α
h : c1 = (append nil (cons x s_1)).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux (cons x s_1))
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil (cons x s_1)).destruct.destruct
    (Computation.bind (destruct nil) (destruct_append.aux (cons x s_1))).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t.think).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t.think)
⊢ (append nil t.think).destruct.tail = (append nil t).destruct ∧
    (Computation.bind (destruct nil) (destruct_append.aux t.think)).tail =
      Computation.bind (destruct nil) (destruct_append.aux t)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t.think).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t.think)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t.think).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t.think)).destruct

Tactic:
exact ⟨nil, t, by simp⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (append nil t).destruct ∧ c2 = Computation.bind (destruct nil) (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (append nil t).destruct.destruct (Computation.bind (destruct nil) (destruct_append.aux t)).destruct

Tactic:
case nil =>
    induction t using WSeq.recOn
    case nil | cons => simp
    case think t => exact ⟨nil, t, by simp⟩

Premises used: Stream'.WSeq.cons, Stream'.WSeq.think, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
x : α
s_1 : WSeq α
h : c1 = ((cons x s_1).append t).destruct ∧ c2 = (cons x s_1).destruct.bind (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x s_1).append t).destruct.destruct ((cons x s_1).destruct.bind (destruct_append.aux t)).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
x : α
s_1 : WSeq α
h : c1 = ((cons x s_1).append t).destruct ∧ c2 = (cons x s_1).destruct.bind (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x s_1).append t).destruct.destruct ((cons x s_1).destruct.bind (destruct_append.aux t)).destruct

Tactic:
case cons => simp

Premises used: Stream'.WSeq.cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s : WSeq α
h : c1 = (s.think.append t).destruct ∧ c2 = s.think.destruct.bind (destruct_append.aux t)
⊢ (s.think.append t).destruct.tail = (s.append t).destruct ∧
    (s.think.destruct.bind (destruct_append.aux t)).tail = s.destruct.bind (destruct_append.aux t)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 t_1 : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s : WSeq α
h : c1 = (s.think.append t).destruct ∧ c2 = s.think.destruct.bind (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (s.think.append t).destruct.destruct (s.think.destruct.bind (destruct_append.aux t)).destruct

Tactic:
exact ⟨s, t, by simp⟩
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 :
  Computation.IsBisimulation.{u} (α := Option (α × WSeq α)) fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
⊢ S.join.destruct = S.destruct.bind destruct_join.aux

Tactic:
apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux)
      _ (Or.inr ⟨S, rfl, rfl⟩)

Premises used: Stream'.WSeq.destruct_join.aux, Stream'.WSeq.join, Stream'.WSeq.destruct, Exists, And, And.intro, Exists.intro, Or, Computation.eq_of_bisim, Computation.bind, Eq, Or.inr, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
c : Computation (Option (α × WSeq α))
inl :
  ∀ (val : Option (α × WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
      (Sum.inl val) (Sum.inl val)
inr :
  ∀ (val : Computation (Option (α × WSeq α))),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
      (Sum.inr val) (Sum.inr val)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    c.destruct c.destruct

Tactic:
cases c.destruct

Premises used: Computation.destruct
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
c : Computation (Option (α × WSeq α))
val : Option (α × WSeq α)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (Sum.inl val) (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
c val : Computation (Option (α × WSeq α))
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (S : WSeq (WSeq α)), c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (Sum.inr val) (Sum.inr val)

Tactic:
simp