-- Mathlib/Data/Seq/Computation.lean
theorem of_results_bind {s : Computation α} {f : α → Computation β} {b k} :
    Results (bind s f) b k → ∃ a m n, Results s a m ∧ Results (f a) b n ∧ k = n + m

Proof state:
α : 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 α
e : α
h : (f e).Results b (n + 1)
⊢ ∃ a m n_1, (pure e).Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
exact ⟨e, _, n + 1, results_pure _, h, rfl⟩

Result:
no goals

Proof state:
α : 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 α
e : α
h : ((pure e).bind f).Results b (n + 1)
⊢ ∃ a m n_1, (pure e).Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
simp only [ret_bind] at h

Result:
α : 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 α
e : α
h : (f e).Results b (n + 1)
⊢ ∃ a m n_1, (pure e).Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Proof state:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
e : α
h : ((pure e).bind f).Results b 0
⊢ ∃ a m n, (pure e).Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
simp only [ret_bind] at h

Result:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
e : α
h : (f e).Results b 0
⊢ ∃ a m n, (pure e).Results a m ∧ (f a).Results b n ∧ 0 = n + m

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

Tactic:
induction k generalizing s with | zero => _ | succ n IH => _
  <;> apply recOn s (fun a => _) fun s' => _ <;> intro e h

Result:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
e : α
h : ((pure e).bind f).Results b 0
⊢ ∃ a m n, (pure e).Results a m ∧ (f a).Results b n ∧ 0 = n + m

α : Type u
β : Type v
f : α → Computation β
b : β
s e : Computation α
h : (e.think.bind f).Results b 0
⊢ ∃ a m n, e.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

α : 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 α
e : α
h : ((pure e).bind f).Results b (n + 1)
⊢ ∃ a m n_1, (pure e).Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

α : 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 e : Computation α
h : (e.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, e.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Proof state:
α : 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 e : Computation α
h : (e.bind f).Results b n
a : α
m n' : ℕ
h1 : e.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m_1 n, e.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1

Tactic:
exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩

Result:
no goals

Proof state:
α : 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 e : Computation α
h : (e.bind f).Results b n
⊢ ∃ a m n_1, e.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
let ⟨a, m, n', h1, h2, e'⟩ := IH h

Result:
α : 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 e : Computation α
h : (e.bind f).Results b n
a : α
m n' : ℕ
h1 : e.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m n_1, e.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Proof state:
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
e : α
h : (f e).Results b 0
⊢ ∃ a m n, (pure e).Results a m ∧ (f a).Results b n ∧ 0 = n + m

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

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → Computation β
b : β
s e : Computation α
h : (e.think.bind f).Results b 0
this : (e.think.bind f).head = ((pure b).thinkN 0).head
⊢ ∃ a m n, e.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
contradiction

Result:
no goals

Proof state:
α : 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 e : Computation α
h : (e.bind f).Results b n
a : α
m n' : ℕ
h1 : e.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m n_1, e.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
rw [e']

Result:
α : 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 e : Computation α
h : (e.bind f).Results b n
a : α
m n' : ℕ
h1 : e.Results a m
h2 : (f a).Results b n'
e' : n = n' + m
⊢ ∃ a m_1 n, e.think.Results a m_1 ∧ (f a).Results b n ∧ n' + m + 1 = n + m_1

Proof state:
α : Type u
β : Type v
f : α → Computation β
b : β
s e : Computation α
h : (e.think.bind f).Results b 0
⊢ ∃ a m n, e.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
have := congr_arg head (eq_thinkN h)

Result:
α : Type u
β : Type v
f : α → Computation β
b : β
s e : Computation α
h : (e.think.bind f).Results b 0
this : (e.think.bind f).head = ((pure b).thinkN 0).head
⊢ ∃ a m n, e.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Proof state:
α : 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 e : Computation α
h : (e.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, e.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
simp only [think_bind, results_think_iff] at h

Result:
α : 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 e : Computation α
h : (e.bind f).Results b n
⊢ ∃ a m n_1, e.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m