α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a n
this : Terminates s
⊢ ∃ m, Results s a m ∧ n = m + 1
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a n
⊢ ∃ m, Results s a m ∧ n = m + 1
haveI := of_think_terminates h.terminates
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a n
this✝ : Terminates s
this : Results s a (length s)
⊢ ∃ m, Results s a m ∧ n = m + 1
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a n
this : Terminates s
⊢ ∃ m, Results s a m ∧ n = m + 1
have := results_of_terminates' _ (of_think_mem h.mem)
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
n : ℕ
h : Results (think s) a n
this✝ : Terminates s
this : Results s a (length s)
⊢ ∃ m, Results s a m ∧ n = m + 1
exact ⟨_, this, Results.len_unique h (results_think this)⟩