-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_map (f : α → β) (s : WSeq α) :
    destruct (map f s) = Computation.map (Option.map (Prod.map f (map f))) (destruct s)

Proof state:
case bisim.intro
α : Type u
β : Type v
f : α → β
s✝ : 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
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, 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 with a s s <;> simp

Result:
case bisim.intro.h3
α : Type u
β : Type v
f : α → β
s✝ : 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
⊢ ∃ s_1,
    (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

Proof state:
case bisim.intro.h3
α : Type u
β : Type v
f : α → β
s✝ : 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
⊢ ∃ s_1,
    (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⟩

Result:
no goals

Proof state:
case bisim.intro
α : Type u
β : Type v
f : α → β
s✝ : 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
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, 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]

Result:
case bisim.intro
α : Type u
β : Type v
f : α → β
s✝ : 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
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, 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

Proof state:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, 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

Result:
case bisim.intro
α : Type u
β : Type v
f : α → β
s✝ : 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
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct

Proof state:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (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)

Result:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct

case r
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ s_1,
    (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

Proof state:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct

Tactic:
intro c1 c2 h

Result:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct

Proof state:
case r
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ s_1,
    (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⟩

Result:
no goals