-- Mathlib/Data/Seq/Computation.lean
theorem eq_thinkN {s : Computation α} {a n} (h : Results s a n) : s = thinkN (pure a) n

Proof state:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
⊢ s.Results a (n + 1) → s = (pure a).thinkN (n + 1)

Tactic:
apply recOn s (fun a' => _) fun s => _

Result:
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
⊢ ∀ (a' : α), (pure a').Results a (n + 1) → pure a' = (pure a).thinkN (n + 1)

α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
⊢ ∀ (s : Computation α), s.think.Results a (n + 1) → s.think = (pure a).thinkN (n + 1)

Proof state:
α : Type u
a✝ : α
s a : Computation α
h : a.think.Results a✝ 0
⊢ a.think = (pure a✝).thinkN 0

Tactic:
obtain ⟨n, h⟩ := of_results_think h

Result:
case intro
α : Type u
a✝ : α
s a : Computation α
h✝ : a.think.Results a✝ 0
n : ℕ
h : a.Results a✝ n ∧ 0 = n + 1
⊢ a.think = (pure a✝).thinkN 0

Proof state:
case intro
α : Type u
a✝ : α
s a : Computation α
h✝ : a.think.Results a✝ 0
n : ℕ
h : a.Results a✝ n ∧ 0 = n + 1
⊢ a.think = (pure a✝).thinkN 0

Tactic:
cases h

Result:
case intro.intro
α : Type u
a✝ : α
s a : Computation α
h : a.think.Results a✝ 0
n : ℕ
left✝ : a.Results a✝ n
right✝ : 0 = n + 1
⊢ a.think = (pure a✝).thinkN 0

Proof state:
α : Type u
a : α
n : ℕ
⊢ ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n

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

Result:
α : Type u
a✝ : α
s : Computation α
a : α
h : (pure a).Results a✝ 0
⊢ pure a = (pure a✝).thinkN 0

α : Type u
a✝ : α
s a : Computation α
h : a.think.Results a✝ 0
⊢ a.think = (pure a✝).thinkN 0

α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s : Computation α
a : α
h : (pure a).Results a✝ (n + 1)
⊢ pure a = (pure a✝).thinkN (n + 1)

α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s a : Computation α
h : a.think.Results a✝ (n + 1)
⊢ a.think = (pure a✝).thinkN (n + 1)

Proof state:
α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s a : Computation α
h : a.think.Results a✝ (n + 1)
⊢ a.think = (pure a✝).thinkN (n + 1)

Tactic:
rw [IH (results_think_iff.1 h)]

Result:
α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s a : Computation α
h : a.think.Results a✝ (n + 1)
⊢ ((pure a✝).thinkN n).think = (pure a✝).thinkN (n + 1)

Proof state:
case intro.intro
α : Type u
a✝ : α
s a : Computation α
h : a.think.Results a✝ 0
n : ℕ
left✝ : a.Results a✝ n
right✝ : 0 = n + 1
⊢ a.think = (pure a✝).thinkN 0

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s = (pure a).thinkN n

Tactic:
revert s

Result:
α : Type u
a : α
n : ℕ
⊢ ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n

Proof state:
α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s a : Computation α
h : a.think.Results a✝ (n + 1)
⊢ ((pure a✝).thinkN n).think = (pure a✝).thinkN (n + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
⊢ ∀ {s : Computation α}, s.Results a (n + 1) → s = (pure a).thinkN (n + 1)

Tactic:
intro s

Result:
case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
⊢ s.Results a (n + 1) → s = (pure a).thinkN (n + 1)

Proof state:
α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s : Computation α
a : α
h : (pure a).Results a✝ (n + 1)
⊢ pure a = (pure a✝).thinkN (n + 1)

Tactic:
have := h.len_unique (results_pure _)

Result:
α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s : Computation α
a : α
h : (pure a).Results a✝ (n + 1)
this : n + 1 = 0
⊢ pure a = (pure a✝).thinkN (n + 1)

Proof state:
α : Type u
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a✝ n → s = (pure a✝).thinkN n
s : Computation α
a : α
h : (pure a).Results a✝ (n + 1)
this : n + 1 = 0
⊢ pure a = (pure a✝).thinkN (n + 1)

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
a✝ : α
s : Computation α
a : α
h : (pure a).Results a✝ 0
⊢ pure a = (pure a✝).thinkN 0

Tactic:
rw [← eq_of_pure_mem h.mem]

Result:
α : Type u
a✝ : α
s : Computation α
a : α
h : (pure a).Results a✝ 0
⊢ pure a✝ = (pure a✝).thinkN 0

Proof state:
α : Type u
a✝ : α
s : Computation α
a : α
h : (pure a).Results a✝ 0
⊢ pure a✝ = (pure a✝).thinkN 0

Tactic:
rfl

Result:
no goals