-- Mathlib/Data/Seq/Computation.lean
theorem bind_assoc (s : Computation α) (f : α → Computation β) (g : β → Computation γ) :
    bind (bind s f) g = bind s fun x : α => bind (f x) g

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

Tactic:
apply recOn s <;> intro s

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

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

Proof state:
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
s✝ : Computation α
s : α
fs : Computation β
⊢ match (fs.bind g).destruct, (fs.bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x => (f x).bind g
  | x, x_1 => False

Tactic:
apply recOn fs <;> intro t <;> simp

Result:
case h1.h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
s✝ : Computation α
s : α
fs : Computation β
t : β
⊢ match (g t).destruct, (g t).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x => (f x).bind g
  | x, x_1 => False

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

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

Result:
no goals

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

Tactic:
intro c₁ c₂ h

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

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

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

Result:
no goals

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

Tactic:
simp only [BisimO, ret_bind]

Result:
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
s✝ : Computation α
s : α
⊢ match ((f s).bind g).destruct, ((f s).bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x => (f x).bind g
  | x, x_1 => False

Proof state:
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ (s.bind f).bind g = s.bind fun x => (f x).bind g

Tactic:
apply
  eq_of_bisim fun c₁ c₂ =>
    c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x : α => bind (f x) g

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

case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x => (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x => (f x).bind g) = s_1.bind fun x => (f x).bind g

Proof state:
case h1.h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
s✝ : Computation α
s : α
fs : Computation β
t : β
⊢ match (g t).destruct, (g t).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x => (f x).bind g
  | x, x_1 => False

Tactic:
rcases destruct (g t) with b | cb <;> simp

Result:
no goals

Proof state:
case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ ((s.bind f).bind g = s.bind fun x => (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x => (f x).bind g) = s_1.bind fun x => (f x).bind g

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

Result:
no goals

Proof state:
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
s✝ : Computation α
s : α
⊢ match ((f s).bind g).destruct, ((f s).bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x => (f x).bind g
  | x, x_1 => False

Tactic:
generalize f s = fs

Result:
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x => (f x).bind g
s✝ : Computation α
s : α
fs : Computation β
⊢ match (fs.bind g).destruct, (fs.bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = (s_1.bind f).bind g ∧ s' = s_1.bind fun x => (f x).bind g
  | x, x_1 => False