-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_flatten (c : Computation (WSeq α)) : destruct (flatten c) = c >>= destruct

Proof state:
α : Type u
c : Computation (WSeq α)
⊢ (flatten c).destruct = c >>= destruct

Tactic:
refine
  Computation.eq_of_bisim
    (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct) ?_
    (Or.inr ⟨c, rfl, rfl⟩)

Result:
α : Type u
c : Computation (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct

Proof state:
α : Type u
c : Computation (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct

Tactic:
intro c1 c2 h

Result:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1.destruct
    c2.destruct

Proof state:
case h1
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ match a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
cases (destruct a).destruct <;> simp

Result:
no goals

Proof state:
case h2
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c' : Computation (WSeq α)
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, 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⟩

Result:
no goals

Proof state:
α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c.destruct
    c.destruct

Tactic:
cases c.destruct <;> simp

Result:
no goals

Proof state:
case h1
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct

Tactic:
simp

Result:
case h1
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ match a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Proof state:
α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c).destruct.destruct (c.bind destruct).destruct

Tactic:
induction' c using Computation.recOn with a c'

Result:
case h1
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct

case h2
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c' : Computation (WSeq α)
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c'.think).destruct.destruct (c'.think.bind destruct).destruct