-- Mathlib/Data/Seq/Computation.lean
theorem bind_pure (f : α → β) (s) : bind s (pure ∘ f) = map f s

Proof state:
α : Type u
β : Type v
f : α → β
s✝ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (s.bind (pure ∘ f)).destruct
    (map f s).destruct

Tactic:
apply recOn s <;> intro s

Result:
case h1
α : Type u
β : Type v
f : α → β
s✝¹ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s✝ : Computation α
s : α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) ((pure s).bind (pure ∘ f)).destruct
    (map f (pure s)).destruct

case h2
α : Type u
β : Type v
f : α → β
s✝¹ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s✝ s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (s.think.bind (pure ∘ f)).destruct
    (map f s.think).destruct

Proof state:
case h1
α : Type u
β : Type v
f : α → β
s✝¹ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s✝ : Computation α
s : α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) ((pure s).bind (pure ∘ f)).destruct
    (map f (pure s)).destruct

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂✝ : Computation β
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂✝ = map f s
c₂ : Computation β
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) c₂.destruct c₂.destruct

Tactic:
rcases destruct c₂ with b | cb <;> simp

Result:
no goals

Proof state:
case r
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1

Tactic:
exact Or.inr ⟨s, rfl, rfl⟩

Result:
no goals

Proof state:
case bisim
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s

Tactic:
intro c₁ c₂ h

Result:
case bisim
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) c₁.destruct c₂.destruct

Proof state:
case h2
α : Type u
β : Type v
f : α → β
s✝¹ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s✝ s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (s.think.bind (pure ∘ f)).destruct
    (map f s.think).destruct

Tactic:
simpa using Or.inr ⟨s, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s

Tactic:
apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s

Result:
case bisim
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s

case r
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1