awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Computation
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
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)
⊢ (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

Premises used: Exists, And, Or, Computation.eq_of_bisim, Computation.bind, Eq
-- Module: Mathlib.Data.Seq.Computation
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)
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)
⊢ 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

Tactic:
rcases destruct c₂ with b | cb

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
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 γ
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:
simp
-- Module: Mathlib.Data.Seq.Computation
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₂ 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:
simp
-- Module: Mathlib.Data.Seq.Computation
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 : α
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
⊢ 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))

Tactic:
simp only [BisimO, ret_bind]

Premises used: Computation.BisimO, Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
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 : α
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
⊢ 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:
generalize f s = fs
-- Module: Mathlib.Data.Seq.Computation
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 :
  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
⊢ 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

Tactic:
rw [ret_bind]

Premises used: Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ 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:
rcases destruct (g t) with b | cb

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Computation
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 : β
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:
simp
-- Module: Mathlib.Data.Seq.Computation
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 : β
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:
simp
-- Module: Mathlib.Data.Seq.Computation
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 : α
s_2 : Computation β
⊢ match (motive := γ ⊕ Computation γ → γ ⊕ Computation γ → Prop) (s_2.think.bind g).destruct,
    (s_2.think.bind g).destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    s = s' ∨ ∃ (s_3 : Computation α), s = (s_3.bind f).bind g ∧ s' = s_3.bind fun (x : α) ↦ (f x).bind g
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Computation
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
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
⊢ 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:
induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp

Premises used: Computation.think, Computation.pure, Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
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.think.bind f).bind g).destruct (destruct (s.think.bind fun (x : α) ↦ (f x).bind g))

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

Premises used: Computation.BisimO, Or.inr
-- Module: Mathlib.Data.Seq.Computation
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))
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))
⊢ 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))

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⟩

Premises used: Computation.think, Computation.pure, Computation.BisimO, Computation.ret_bind, Or.inr
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
s : 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
⊢ 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

Tactic:
match c₁, c₂, h with
    | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
    | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
      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⟩
-- Module: Mathlib.Data.Seq.Computation
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) ∨
    ∃ (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:
Or.inr ⟨s, rfl, rfl⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.Seq.Computation
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) ∨
    ∃ (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:
exact Or.inr ⟨s, rfl, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
m n : ℕ
h1 : s.Results a m
h2 : (f a).Results b n
⊢ a ∈ s

Tactic:
have := h1.mem
-- Module: Mathlib.Data.Seq.Computation
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
revert : ∀ {m : ℕ} (h1 : s.Results a m), (s.bind f).Results b (n + m)
⊢ (s.bind f).Results b (n + m)

Tactic:
revert m
-- Module: Mathlib.Data.Seq.Computation
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)
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)
⊢ ∀ {m : ℕ} (h1 : s.Results a m), (s.bind f).Results b (n + m)

Tactic:
apply memRecOn this _ fun s IH => _

Premises used: Computation.memRecOn
-- Module: Mathlib.Data.Seq.Computation
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
rw : (f a).Results b (n + m)
⊢ ((pure a).bind f).Results b (n + m)

Tactic:
rw [ret_bind]

Premises used: Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
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
rw : (f a).Results b (n + 0)
⊢ (f a).Results b (n + m)

Tactic:
rw [h1.len_unique (results_pure _)]

Premises used: Computation.Results.len_unique, Computation.results_pure
-- Module: Mathlib.Data.Seq.Computation
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 + 0)

Tactic:
h2
-- Module: Mathlib.Data.Seq.Computation
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 + 0)

Tactic:
exact h2
-- Module: Mathlib.Data.Seq.Computation
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)
⊢ ∀ {m : ℕ} (h1 : s_1.think.Results a m), (s_1.think.bind f).Results b (n + m)

Tactic:
_
-- Module: Mathlib.Data.Seq.Computation
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
rw : (s_1.bind f).think.Results b (n + m)
⊢ (s_1.think.bind f).Results b (n + m)

Tactic:
rw [think_bind]

Premises used: Computation.think_bind
-- Module: Mathlib.Data.Seq.Computation
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
obtain : ∀ (m' : ℕ) (h : s_1.Results a m' ∧ m = m' + 1), (s_1.bind f).think.Results b (n + m)
⊢ (s_1.bind f).think.Results b (n + m)

Tactic:
obtain ⟨m', h⟩ := of_results_think h1

Premises used: Computation.of_results_think
-- Module: Mathlib.Data.Seq.Computation
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.Results a m'

Tactic:
obtain ⟨h1, e⟩ := h
-- Module: Mathlib.Data.Seq.Computation
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'
⊢ m = m' + 1

Tactic:
obtain ⟨h1, e⟩ := h
-- Module: Mathlib.Data.Seq.Computation
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
rw : (s_1.bind f).think.Results b (n + (m' + 1))
⊢ (s_1.bind f).think.Results b (n + m)

Tactic:
rw [e]
-- Module: Mathlib.Data.Seq.Computation
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' + 1))

Tactic:
results_think (h3 h1)

Premises used: Computation.results_think
-- Module: Mathlib.Data.Seq.Computation
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' + 1))

Tactic:
exact results_think (h3 h1)

Premises used: Computation.results_think
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : a ∈ s
h2 : b ∈ f a
⊢ b ∈ s.bind f

Tactic:
let ⟨_, h1⟩ := exists_results_of_mem h1
  let ⟨_, h2⟩ := exists_results_of_mem h2
  (results_bind h1 h2).mem

Premises used: _private.0.Computation.mem_bind.match_2, Computation.exists_results_of_mem, Membership.mem, Computation.results_bind, _private.0.Computation.mem_bind.match_1, Computation.Results.mem, Computation.bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
inst : s.Terminates
inst_1 : (f s.get).Terminates
⊢ (s.bind f).Terminates

Tactic:
terminates_of_mem (mem_bind (get_mem s) (get_mem (f (get s))))

Premises used: Computation.get_mem, Computation.terminates_of_mem, Computation.get, Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
inst : s.Terminates
inst_1 : (f s.get).Terminates
⊢ (s.bind f).get = (f s.get).get

Tactic:
get_eq_of_mem _ (mem_bind (get_mem s) (get_mem (f (get s))))

Premises used: Computation.get_mem, Computation.get_eq_of_mem, Computation.get, Computation.mem_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
_T1 : s.Terminates
_T2 : (f s.get).Terminates
⊢ (s.bind f).length = (f s.get).length + s.length

Tactic:
(results_of_terminates _).len_unique <|
    results_bind (results_of_terminates _) (results_of_terminates _)

Premises used: Computation.Results.len_unique, Computation.results_bind, Computation.results_of_terminates
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
b : β
k : ℕ
zero :
  ∀ {s : Computation α},
    (s.bind f).Results b 0 → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ 0 = n + m
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ {s : Computation α},
        (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m)
    {s : Computation α},
    (s.bind f).Results b (n + 1) →
      ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
⊢ (s.bind f).Results b k → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ k = n + m

Tactic:
induction k generalizing s with | zero | succ n IH
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
zero :
  ∀ (a : α) (h : ((pure a).bind f).Results b 0),
    ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m
zero₁ :
  ∀ (s' : Computation α) (h : (s'.think.bind f).Results b 0),
    ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m
⊢ (s.bind f).Results b 0 → ∃ (a : α), ∃ (m : ℕ), ∃ (n : ℕ), s.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
induction s using recOn with intro h | pure a | think s'

Premises used: Computation.think, Computation.pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH :
  ∀ {s : Computation α},
    (s.bind f).Results b n → ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s : Computation α
succ :
  ∀ (a : α) (h : ((pure a).bind f).Results b (n + 1)),
    ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m
succ₁ :
  ∀ (s' : Computation α) (h : (s'.think.bind f).Results b (n + 1)),
    ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
⊢ (s.bind f).Results b (n + 1) →
    ∃ (a : α), ∃ (m : ℕ), ∃ (n_1 : ℕ), s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
induction s using recOn with intro h | pure a | think s'

Premises used: Computation.think, Computation.pure
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ (f a).Results b 0

Tactic:
simp only [ret_bind] at h

Premises used: Computation.ret_bind
-- Module: Mathlib.Data.Seq.Computation
Goal:
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : (f a).Results b 0
⊢ ∃ (a_1 : α), ∃ (m : ℕ), ∃ (n : ℕ), (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m

Tactic:
⟨_, _, _, results_pure _, h, rfl⟩

Premises used: Computation.results_pure, And.intro, Exists.intro, rfl