α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail
      (corec
        (fun x =>
          match x with
          | (s₁, snd) => head s₁)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, tail s₁))
        (s₁, s₂)) =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₂, tail s₁)
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail (s₁ ⋈ s₂) = s₂ ⋈ tail s₁
unfold interleave corecOn
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail
      ((match (s₁, s₂) with
        | (s₁, snd) => head s₁) ::
        corec
          (fun x =>
            match x with
            | (s₁, snd) => head s₁)
          (fun x =>
            match x with
            | (s₁, s₂) => (s₂, tail s₁))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, tail s₁))) =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₂, tail s₁)
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail
      (corec
        (fun x =>
          match x with
          | (s₁, snd) => head s₁)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, tail s₁))
        (s₁, s₂)) =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₂, tail s₁)
rw [corec_eq]
no goals
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ tail
      ((match (s₁, s₂) with
        | (s₁, snd) => head s₁) ::
        corec
          (fun x =>
            match x with
            | (s₁, snd) => head s₁)
          (fun x =>
            match x with
            | (s₁, s₂) => (s₂, tail s₁))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, tail s₁))) =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₂, tail s₁)
rfl