α : Type u
β : Type v
γ : Type w
s : Computation α
x✝ : Terminates s
a : α
n : ℕ
h : some a = ↑s n
⊢ Option.isSome (↑s n) = true
α : Type u
β : Type v
γ : Type w
s : Computation α
x✝ : Terminates s
a : α
n : ℕ
h : (fun b => some a = b) (Stream'.nth (↑s) n)
⊢ Option.isSome (↑s n) = true
dsimp [Stream'.nth] at h
α : Type u
β : Type v
γ : Type w
s : Computation α
x✝ : Terminates s
a : α
n : ℕ
h : some a = ↑s n
⊢ Option.isSome (some a) = true
α : Type u
β : Type v
γ : Type w
s : Computation α
x✝ : Terminates s
a : α
n : ℕ
h : some a = ↑s n
⊢ Option.isSome (↑s n) = true
rw [← h]
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
x✝ : Terminates s
a : α
n : ℕ
h : some a = ↑s n
⊢ Option.isSome (some a) = true
exact rfl