α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
let t := tail s₁ ⋈ tail s₂
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: t
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
show s₁ ⋈ s₂ = head s₁::head s₂::t
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ (corecOn (s₁, s₂)
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      fun x =>
      match x with
      | (s₁, s₂) => (s₂, tail s₁)) =
    head s₁ :: head s₂ :: t
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ s₁ ⋈ s₂ = head s₁ :: head s₂ :: t
unfold interleave
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₁, s₂) =
    head s₁ :: head s₂ :: t
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ (corecOn (s₁, s₂)
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      fun x =>
      match x with
      | (s₁, s₂) => (s₂, tail s₁)) =
    head s₁ :: head s₂ :: t
unfold corecOn
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ (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₁)) =
    head s₁ :: head s₂ :: t
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ corec
      (fun x =>
        match x with
        | (s₁, snd) => head s₁)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, tail s₁))
      (s₁, s₂) =
    head s₁ :: head s₂ :: t
rw [corec_eq]
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ head s₁ :: corec (fun x => head x.fst) (fun x => (x.snd, tail x.fst)) (s₂, tail s₁) =
    head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ (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₁)) =
    head s₁ :: head s₂ :: t
dsimp
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ head s₁ ::
      head (s₂, tail s₁).fst ::
        corec (fun x => head x.fst) (fun x => (x.snd, tail x.fst)) ((s₂, tail s₁).snd, tail (s₂, tail s₁).fst) =
    head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ head s₁ :: corec (fun x => head x.fst) (fun x => (x.snd, tail x.fst)) (s₂, tail s₁) =
    head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
rw [corec_eq]
no goals
α : Type u
β : Type v
δ : Type w
s₁ s₂ : Stream' α
t : Stream' α := tail s₁ ⋈ tail s₂
⊢ head s₁ ::
      head (s₂, tail s₁).fst ::
        corec (fun x => head x.fst) (fun x => (x.snd, tail x.fst)) ((s₂, tail s₁).snd, tail (s₂, tail s₁).fst) =
    head s₁ :: head s₂ :: (tail s₁ ⋈ tail s₂)
rfl