α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ instFunctorOption.1
      (fun a' =>
        (a',
          tail
            { val := some a :: ↑{ val := f, property := al },
              property :=
                (_ :
                  ∀ {n : ℕ},
                    (some a :: ↑{ val := f, property := al }) n = none →
                      (some a :: ↑{ val := f, property := al }) (n + 1) = none) }))
      (get?
        { val := some a :: ↑{ val := f, property := al },
          property :=
            (_ :
              ∀ {n : ℕ},
                (some a :: ↑{ val := f, property := al }) n = none →
                  (some a :: ↑{ val := f, property := al }) (n + 1) = none) }
        0) =
    some (a, { val := f, property := al })
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ destruct (cons a { val := f, property := al }) = some (a, { val := f, property := al })
unfold cons destruct Functor.map
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ tail
      { val := some a :: ↑{ val := f, property := al },
        property :=
          (_ :
            ∀ {n : ℕ},
              (some a :: ↑{ val := f, property := al }) n = none →
                (some a :: ↑{ val := f, property := al }) (n + 1) = none) } =
    { val := f, property := al }
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ instFunctorOption.1
      (fun a' =>
        (a',
          tail
            { val := some a :: ↑{ val := f, property := al },
              property :=
                (_ :
                  ∀ {n : ℕ},
                    (some a :: ↑{ val := f, property := al }) n = none →
                      (some a :: ↑{ val := f, property := al }) (n + 1) = none) }))
      (get?
        { val := some a :: ↑{ val := f, property := al },
          property :=
            (_ :
              ∀ {n : ℕ},
                (some a :: ↑{ val := f, property := al }) n = none →
                  (some a :: ↑{ val := f, property := al }) (n + 1) = none) }
        0) =
    some (a, { val := f, property := al })
apply congr_arg fun s => some (a, s)
case a
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ ↑(tail
        { val := some a :: ↑{ val := f, property := al },
          property :=
            (_ :
              ∀ {n : ℕ},
                (some a :: ↑{ val := f, property := al }) n = none →
                  (some a :: ↑{ val := f, property := al }) (n + 1) = none) }) =
    ↑{ val := f, property := al }
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ tail
      { val := some a :: ↑{ val := f, property := al },
        property :=
          (_ :
            ∀ {n : ℕ},
              (some a :: ↑{ val := f, property := al }) n = none →
                (some a :: ↑{ val := f, property := al }) (n + 1) = none) } =
    { val := f, property := al }
apply Subtype.eq
no goals
case a
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option α)
al : IsSeq f
⊢ ↑(tail
        { val := some a :: ↑{ val := f, property := al },
          property :=
            (_ :
              ∀ {n : ℕ},
                (some a :: ↑{ val := f, property := al }) n = none →
                  (some a :: ↑{ val := f, property := al }) (n + 1) = none) }) =
    ↑{ val := f, property := al }
dsimp [tail]