case mk
α : Type u
β : Type v
γ : Type w
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ tail (think { val := f, property := al }) = { val := f, property := al }
α : Type u
β : Type v
γ : Type w
s : Computation α
⊢ tail (think s) = s
cases' s with f al
case mk.a
α : Type u
β : Type v
γ : Type w
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑(tail (think { val := f, property := al })) = ↑{ val := f, property := al }
case mk
α : Type u
β : Type v
γ : Type w
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ tail (think { val := f, property := al }) = { val := f, property := al }
apply Subtype.eq
no goals
case mk.a
α : Type u
β : Type v
γ : Type w
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑(tail (think { val := f, property := al })) = ↑{ val := f, property := al }
dsimp [tail, think]