-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_append (s t : WSeq α) :
    destruct (append s t) = (destruct s).bind (destruct_append.aux t)

Proof state:
case intro.intro
α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ Computation.BisimO (fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct

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

Result:
case intro.intro
α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ Computation.BisimO (fun c1 c2 => ∃ s t, 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

Proof state:
case intro.intro.h1.h3
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t.think)
⊢ ∃ s t_1, t.destruct = (s.append t_1).destruct ∧ t.destruct = s.destruct.bind (destruct_append.aux t_1)

Tactic:
refine ⟨nil, t, ?_, ?_⟩ <;> simp

Result:
no goals

Proof state:
case intro.intro.h1
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t)
⊢ match t.destruct.destruct, t.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => ∃ s_1 t, s = (s_1.append t).destruct ∧ s' = s_1.destruct.bind (destruct_append.aux t)
  | x, x_1 => False

Tactic:
induction' t using WSeq.recOn with b t t <;> simp

Result:
case intro.intro.h1.h3
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t.think)
⊢ ∃ s t_1, t.destruct = (s.append t_1).destruct ∧ t.destruct = s.destruct.bind (destruct_append.aux t_1)

Proof state:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ Computation.BisimO (fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct

Tactic:
rcases h with ⟨s, t, h⟩

Result:
case intro.intro
α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ Computation.BisimO (fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct

Proof state:
case intro.intro
α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
s t : WSeq α
h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ Computation.BisimO (fun c1 c2 => ∃ s t, 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 with a s s <;> simp

Result:
case intro.intro.h1
α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t)
⊢ match t.destruct.destruct, t.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => ∃ s_1 t, s = (s_1.append t).destruct ∧ s' = s_1.destruct.bind (destruct_append.aux t)
  | x, x_1 => False

case intro.intro.h3
α : Type u
s✝ t✝ : 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_1 t_1,
    (s.append t).destruct = (s_1.append t_1).destruct ∧
      s.destruct.bind (destruct_append.aux t) = s_1.destruct.bind (destruct_append.aux t_1)

Proof state:
α : Type u
s t : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)

Tactic:
intro c1 c2 h

Result:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ Computation.BisimO (fun c1 c2 => ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct

Proof state:
case intro.intro.h3
α : Type u
s✝ t✝ : 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_1 t_1,
    (s.append t).destruct = (s_1.append t_1).destruct ∧
      s.destruct.bind (destruct_append.aux t) = s_1.destruct.bind (destruct_append.aux t_1)

Tactic:
exact ⟨s, t, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
s t : WSeq α
⊢ (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⟩

Result:
α : Type u
s t : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)