-- Mathlib/Data/Seq/Computation.lean
theorem results_bind {s : Computation α} {f : α → Computation β} {a b m n} (h1 : Results s a m)
    (h2 : Results (f a) b n) : Results (bind s f) b (n + m)

Proof state:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)

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

Result:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, (pure a).Results a m → ((pure a).bind f).Results b (n + m)

α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)

Proof state:
case intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
m' : ℕ
h : s✝.Results a m' ∧ m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + m✝)

Tactic:
obtain ⟨h1, e⟩ := h

Result:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + m✝)

Proof state:
α : 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)

Tactic:
have := h1.mem

Result:
α : 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)

Proof state:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + (m' + 1))

Tactic:
exact results_think (h3 h1)

Result:
no goals

Proof state:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + m✝)

Tactic:
rw [e]

Result:
case intro.intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + (m' + 1))

Proof state:
α : 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✝)

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

Result:
α : 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)

Proof state:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, 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:
rw [think_bind]

Result:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
⊢ (s✝.bind f).think.Results b (n + m✝)

Proof state:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, (pure a).Results a m → ((pure a).bind f).Results b (n + m)

Tactic:
intro _ h1

Result:
α : 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✝)

Proof state:
α : 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

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
⊢ (s✝.bind f).think.Results b (n + m✝)

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

Result:
case intro
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
m' : ℕ
h : s✝.Results a m' ∧ m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + m✝)

Proof state:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)

Tactic:
intro _ h3 _ h1

Result:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, 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✝)

Proof state:
α : 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)

Tactic:
revert m

Result:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)

Proof state:
α : 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✝)

Tactic:
rw [ret_bind]

Result:
α : 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✝)