α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : Computation α}, Results s a n → s = thinkN (pure a) n
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results s a n
⊢ s = thinkN (pure a) n
revert s
α : Type u
β : Type v
γ : Type w
a✝ : α
s : Computation α
a : α
h : Results (pure a) a✝ Nat.zero
⊢ pure a = thinkN (pure a✝) Nat.zero

α : Type u
β : Type v
γ : Type w
a✝ : α
s a : Computation α
h : Results (think a) a✝ Nat.zero
⊢ think a = thinkN (pure a✝) Nat.zero

α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s : Computation α
a : α
h : Results (pure a) a✝ (Nat.succ n)
⊢ pure a = thinkN (pure a✝) (Nat.succ n)

α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s a : Computation α
h : Results (think a) a✝ (Nat.succ n)
⊢ think a = thinkN (pure a✝) (Nat.succ n)
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : Computation α}, Results s a n → s = thinkN (pure a) n
induction' n with n IH <;> intro s <;> apply recOn s (fun a' => _) fun s => _ <;> intro a h
α : Type u
β : Type v
γ : Type w
a✝ : α
s : Computation α
a : α
h : Results (pure a) a✝ Nat.zero
⊢ pure a✝ = thinkN (pure a✝) Nat.zero
α : Type u
β : Type v
γ : Type w
a✝ : α
s : Computation α
a : α
h : Results (pure a) a✝ Nat.zero
⊢ pure a = thinkN (pure a✝) Nat.zero
rw [← eq_of_pure_mem h.mem]
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
s : Computation α
a : α
h : Results (pure a) a✝ Nat.zero
⊢ pure a✝ = thinkN (pure a✝) Nat.zero
rfl
case intro
α : Type u
β : Type v
γ : Type w
a✝ : α
s a : Computation α
h✝ : Results (think a) a✝ Nat.zero
n : ℕ
h : Results a a✝ n ∧ Nat.zero = n + 1
⊢ think a = thinkN (pure a✝) Nat.zero
α : Type u
β : Type v
γ : Type w
a✝ : α
s a : Computation α
h : Results (think a) a✝ Nat.zero
⊢ think a = thinkN (pure a✝) Nat.zero
cases' of_results_think h with n h
case intro.intro
α : Type u
β : Type v
γ : Type w
a✝ : α
s a : Computation α
h : Results (think a) a✝ Nat.zero
n : ℕ
left✝ : Results a a✝ n
right✝ : Nat.zero = n + 1
⊢ think a = thinkN (pure a✝) Nat.zero
case intro
α : Type u
β : Type v
γ : Type w
a✝ : α
s a : Computation α
h✝ : Results (think a) a✝ Nat.zero
n : ℕ
h : Results a a✝ n ∧ Nat.zero = n + 1
⊢ think a = thinkN (pure a✝) Nat.zero
cases h
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
a✝ : α
s a : Computation α
h : Results (think a) a✝ Nat.zero
n : ℕ
left✝ : Results a a✝ n
right✝ : Nat.zero = n + 1
⊢ think a = thinkN (pure a✝) Nat.zero
contradiction
α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s : Computation α
a : α
h : Results (pure a) a✝ (Nat.succ n)
this : Nat.succ n = 0
⊢ pure a = thinkN (pure a✝) (Nat.succ n)
α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s : Computation α
a : α
h : Results (pure a) a✝ (Nat.succ n)
⊢ pure a = thinkN (pure a✝) (Nat.succ n)
have := h.len_unique (results_pure _)
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s : Computation α
a : α
h : Results (pure a) a✝ (Nat.succ n)
this : Nat.succ n = 0
⊢ pure a = thinkN (pure a✝) (Nat.succ n)
contradiction
α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s a : Computation α
h : Results (think a) a✝ (Nat.succ n)
⊢ think (thinkN (pure a✝) n) = thinkN (pure a✝) (Nat.succ n)
α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s a : Computation α
h : Results (think a) a✝ (Nat.succ n)
⊢ think a = thinkN (pure a✝) (Nat.succ n)
rw [IH (results_think_iff.1 h)]
no goals
α : Type u
β : Type v
γ : Type w
a✝ : α
n : ℕ
IH : ∀ {s : Computation α}, Results s a✝ n → s = thinkN (pure a✝) n
s a : Computation α
h : Results (think a) a✝ (Nat.succ n)
⊢ think (thinkN (pure a✝) n) = thinkN (pure a✝) (Nat.succ n)
rfl