awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
a : α
f : α → Computation β
c₁ c₂ : Computation β
h : c₁ = (pure a).bind f ∧ c₂ = f a ∨ c₁ = corec (Bind.f f) (Sum.inr c₂)
c : Computation β
inl :
  ∀ (b : β),
    match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
      match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (Sum.inl b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (corec (Bind.f f) b),
      Sum.inl b with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
    | x, x_1 => False
⊢ match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g c.destruct with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    c.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
have inr : ∀ (cb : Computation β),
  match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := β ⊕ Sum.{u, v} (Computation α) (Computation β) → β ⊕ Computation β) Bind.g (Sum.inr cb) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec (Bind.f f) b),
    Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = (pure a).bind f ∧ s' = f a ∨ s = corec (Bind.f f) (Sum.inr s')
  | x, x_1 => False
Tactic: rcases destruct c with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
⊢ s.bind (pure ∘ f) = map f s
have bisim : IsBisimulation.{v} (α := β) fun (c₁ c₂ : Computation β) ↦
  c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
Tactic: apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
bisim :
  IsBisimulation.{v} (α := β) fun (c₁ c₂ : Computation β) ↦
    c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
⊢ s.bind (pure ∘ f) = map f s
have r : s.bind (pure ∘ f) = map f s ∨ ∃ (s_1 : Computation α), s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1
Tactic: apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s (pure ∘ f) ∧ c₂ = map f s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂_1 : Computation β
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂_1 = map f s
c₂ : Computation β
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    c₂.destruct c₂.destruct
have inl : ∀ (b : β),
  BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    (Sum.inl b) (Sum.inl b)
Tactic: rcases destruct c₂ with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : Computation α
c₁ c₂_1 : Computation β
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂_1 = map f s
c₂ : Computation β
inl :
  ∀ (b : β),
    BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
      (Sum.inl b) (Sum.inl b)
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    c₂.destruct c₂.destruct
have inr : ∀ (cb : Computation β),
  BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    (Sum.inr cb) (Sum.inr cb)
Tactic: rcases destruct c₂ with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : Computation α
⊢ BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    (s.bind (pure ∘ f)).destruct (map f s).destruct
have pure : ∀ (s : α),
  BisimO (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s)
    ((pure s).bind (pure ∘ f)).destruct (map f (pure s)).destruct
Tactic: induction s using recOn with
      | pure s => simp
      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s
s : Computation α
pure :
  ∀ (s : α),
    BisimO
      (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s)
      ((Computation.pure s).bind (Computation.pure ∘ f)).destruct (map f (Computation.pure s)).destruct
⊢ BisimO
    (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s)
    (s.bind (Computation.pure ∘ f)).destruct (map f s).destruct
have think : ∀ (s : Computation α),
  BisimO
    (fun (c₁ c₂ : Computation β) ↦ c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = s.bind (Computation.pure ∘ f) ∧ c₂ = map f s)
    (s.think.bind (Computation.pure ∘ f)).destruct (map f s.think).destruct
Tactic: induction s using recOn with
      | pure s => simp
      | think s => simpa using Or.inr ⟨s, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : 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
have bisim : IsBisimulation.{w} (α := γ) fun (c₁ c₂ : Computation γ) ↦
  c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = 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
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
bisim :
  IsBisimulation.{w} (α := γ) fun (c₁ c₂ : Computation γ) ↦
    c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
⊢ (s.bind f).bind g = s.bind fun (x : α) ↦ (f x).bind g
have r : ((s.bind f).bind g = s.bind fun (x : α) ↦ (f x).bind g) ∨
  ∃ (s_1 : Computation α),
    (s.bind f).bind g = (s_1.bind f).bind g ∧
      Eq.{w + 1} (α := Computation γ) (s.bind fun (x : α) ↦ (f x).bind g) (s_1.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
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂_1 : Computation γ
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂_1 = s.bind fun (x : α) ↦ (f x).bind g
c₂ : Computation γ
⊢ BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    c₂.destruct c₂.destruct
have inl : ∀ (b : γ),
  BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    (Sum.inl b) (Sum.inl b)
Tactic: rcases destruct c₂ with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂_1 : Computation γ
h : c₁ = c₂_1 ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂_1 = s.bind fun (x : α) ↦ (f x).bind g
c₂ : Computation γ
inl :
  ∀ (b : γ),
    BisimO
      (fun (c₁ c₂ : Computation γ) ↦
        c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
      (Sum.inl b) (Sum.inl b)
⊢ BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    c₂.destruct c₂.destruct
have inr : ∀ (cb : Computation γ),
  BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    (Sum.inr cb) (Sum.inr cb)
Tactic: rcases destruct c₂ with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
⊢ BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    (((pure s).bind f).bind g).destruct (destruct ((pure s).bind fun (x : α) ↦ (f x).bind g))
have pure : match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) ((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_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
| x, x_1 => False
Tactic: simp only [BisimO, ret_bind]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) ((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_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
have pure : ∀ (fs : Computation β),
  match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (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_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
Tactic: generalize f s = fs
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
t : β
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) ((pure t).bind g).destruct,
    ((pure t).bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
have pure : match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (g t).destruct, (g t).destruct with
| Sum.inl a, Sum.inl a' => a = a'
| Sum.inr s, Sum.inr s' =>
  s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
| x, x_1 => False
Tactic: rw [ret_bind]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
t : β
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (g t).destruct, (g t).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
have pure : ∀ (b : γ),
  match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) Sum.inl b, Sum.inl b with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
Tactic: rcases destruct (g t) with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
t : β
pure :
  ∀ (b : γ),
    match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) Sum.inl b, Sum.inl b with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' =>
      s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
    | x, x_1 => False
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (g t).destruct, (g t).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
have pure₁ : ∀ (cb : Computation γ),
  match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) Sum.inr cb, Sum.inr cb with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
Tactic: rcases destruct (g t) with b | cb
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
fs : Computation β
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (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_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
have pure : ∀ (t : β),
  match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) ((pure t).bind g).destruct,
    ((pure t).bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
Tactic: induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
Cleared hypotheses: fs
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : α
fs : Computation β
pure :
  ∀ (t : β),
    match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) ((Computation.pure t).bind g).destruct,
      ((Computation.pure t).bind g).destruct with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' =>
      s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
    | x, x_1 => False
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (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_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
have pure₁ : ∀ (s : Computation β),
  match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (s.think.bind g).destruct,
    (s.think.bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_2 : Computation α), s = (s_2.bind f).bind g ∧ s' = s_2.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False
Tactic: induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
Cleared hypotheses: fs
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : Computation α
⊢ BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    ((s.bind f).bind g).destruct (destruct (s.bind fun (x : α) ↦ (f x).bind g))
have pure : ∀ (s : α),
  BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    (((pure s).bind f).bind g).destruct (destruct ((pure s).bind fun (x : α) ↦ (f x).bind g))
Tactic: induction s using recOn with
      | pure s =>
        simp only [BisimO, ret_bind]; generalize f s = fs
        induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
s_1 : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g
s : Computation α
pure :
  ∀ (s : α),
    BisimO
      (fun (c₁ c₂ : Computation γ) ↦
        c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
      (((Computation.pure s).bind f).bind g).destruct (destruct ((Computation.pure s).bind fun (x : α) ↦ (f x).bind g))
⊢ BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    ((s.bind f).bind g).destruct (destruct (s.bind fun (x : α) ↦ (f x).bind g))
have think : ∀ (s : Computation α),
  BisimO
    (fun (c₁ c₂ : Computation γ) ↦
      c₁ = c₂ ∨ ∃ (s : Computation α), c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun (x : α) ↦ (f x).bind g)
    ((s.think.bind f).bind g).destruct (destruct (s.think.bind fun (x : α) ↦ (f x).bind g))
Tactic: induction s using recOn with
      | pure s =>
        simp only [BisimO, ret_bind]; generalize f s = fs
        induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : s.Results a m
h2 : (f a).Results b n
⊢ (s.bind f).Results b (n + m)
have this : a ∈ s
Tactic: have := h1.mem
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : s.Results a m
h2 : (f a).Results b n
this : a ∈ s
⊢ (s.bind f).Results b (n + m)
have revert : ∀ {m : ℕ} (h1 : s.Results a m), (s.bind f).Results b (n + m)
Tactic: revert m
Cleared hypotheses: m, h1
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ} (h1 : s.Results a m), (s.bind f).Results b (n + m)
have apply : ∀ {m : ℕ} (h1 : (pure a).Results a m), ((pure a).bind f).Results b (n + m)
Tactic: apply memRecOn this _ fun s IH => _
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
apply : ∀ {m : ℕ} (h1 : (pure a).Results a m), ((pure a).bind f).Results b (n + m)
⊢ ∀ {m : ℕ} (h1 : s.Results a m), (s.bind f).Results b (n + m)
have apply₁ : ∀ (s : Computation α) (IH : ∀ {m : ℕ} (h1 : s.Results a m), (s.bind f).Results b (n + m)) {m : ℕ}
  (h1 : s.think.Results a m), (s.think.bind f).Results b (n + m)
Tactic: apply memRecOn this _ fun s IH => _
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
m : ℕ
h1 : (pure a).Results a m
⊢ ((pure a).bind f).Results b (n + m)
have rw : (f a).Results b (n + m)
Tactic: rw [ret_bind]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
m : ℕ
h1 : (pure a).Results a m
⊢ (f a).Results b (n + m)
have rw : (f a).Results b (n + 0)
Tactic: rw [h1.len_unique (results_pure _)]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s_1 : Computation α
h3 : ∀ {m : ℕ} (h1 : s_1.Results a m), (s_1.bind f).Results b (n + m)
m : ℕ
h1 : s_1.think.Results a m
⊢ (s_1.think.bind f).Results b (n + m)
have rw : (s_1.bind f).think.Results b (n + m)
Tactic: rw [think_bind]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s_1 : Computation α
h3 : ∀ {m : ℕ} (h1 : s_1.Results a m), (s_1.bind f).Results b (n + m)
m : ℕ
h1 : s_1.think.Results a m
⊢ (s_1.bind f).think.Results b (n + m)
have obtain : ∀ (m' : ℕ) (h : s_1.Results a m' ∧ m = m' + 1), (s_1.bind f).think.Results b (n + m)
Tactic: obtain ⟨m', h⟩ := of_results_think h1
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s_1 : Computation α
h3 : ∀ {m : ℕ} (h1 : s_1.Results a m), (s_1.bind f).Results b (n + m)
m : ℕ
h1 : s_1.think.Results a m
m' : ℕ
h : s_1.Results a m' ∧ m = m' + 1
⊢ (s_1.bind f).think.Results b (n + m)
have h1₁ : s_1.Results a m'
Tactic: obtain ⟨h1, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (hypothesis)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s_1 : Computation α
h3 : ∀ {m : ℕ} (h1 : s_1.Results a m), (s_1.bind f).Results b (n + m)
m : ℕ
h1 : s_1.think.Results a m
m' : ℕ
h : s_1.Results a m' ∧ m = m' + 1
h1₁ : s_1.Results a m'
⊢ (s_1.bind f).think.Results b (n + m)
have e : m = m' + 1
Tactic: obtain ⟨h1, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s_1 : Computation α
h3 : ∀ {m : ℕ} (h1 : s_1.Results a m), (s_1.bind f).Results b (n + m)
m : ℕ
h1_1 : s_1.think.Results a m
m' : ℕ
h1 : s_1.Results a m'
e : m = m' + 1
⊢ (s_1.bind f).think.Results b (n + m)
have rw : (s_1.bind f).think.Results b (n + (m' + 1))
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Data.Seq.Computation (goal)
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
b : β
k : ℕ
⊢ (s.bind f).Results b k → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ k = n + m
have zero : ∀ {s : Computation α},
  (s.bind f).Results b 0 → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ 0 = n + m
Tactic: induction k generalizing s with | zero | succ n IH
Cleared hypotheses: s, k