α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (Seq.get? (some <$> s) 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) (Seq.get? s 0))
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Computation.destruct (destruct ↑s) = Sum.inl (Option.map (fun a => (a, ↑(Seq.tail s))) (Seq.head s))
simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
  Seq.head]
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (some <$> Seq.get? s 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) (Seq.get? s 0))
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (Seq.get? (some <$> s) 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) (Seq.get? s 0))
rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (some <$> none) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) none)

case some
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (some <$> some a) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) (some a))
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (some <$> Seq.get? s 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) (Seq.get? s 0))
cases' Seq.get? s 0 with a
no goals
case some
α : Type u
β : Type v
γ : Type w
s : Seq α
a : α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (Seq.map some s))) (Option.map some (some a)) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, Seq.map some (Seq.tail s))) (some a))
simp [destruct]
no goals
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0
apply Seq.map_get?
no goals
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ (match
      match Option.map (fun a' => (a', Seq.tail (some <$> s))) (some <$> none) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s =>
            match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a => (a, some <$> Seq.tail s)) none)
rfl