-- Mathlib/Data/Stream/Init.lean
theorem interleave_eq (s₁ s₂ : Stream' α) : s₁ ⋈ s₂ = head s₁::head s₂::(tail s₁ ⋈ tail s₂)

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t

Tactic:
rw [corec_eq]

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x =>
          match x with
          | (s₁, snd) => s₁.head)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
let t := tail s₁ ⋈ tail s₂

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x => x.fst.head) (fun x => (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
show s₁ ⋈ s₂ = head s₁::head s₂::t

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: t

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (corecOn (s₁, s₂)
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      fun x =>
      match x with
      | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Tactic:
unfold corecOn

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ corec
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₁, s₂) =
    s₁.head :: s₂.head :: t

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head :: corec (fun x => x.fst.head) (fun x => (x.snd, x.fst.tail)) (s₂, s₁.tail) = s₁.head :: s₂.head :: t

Tactic:
rw [corec_eq]

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head ::
      (s₂, s₁.tail).fst.head ::
        corec (fun x => x.fst.head) (fun x => (x.snd, x.fst.tail)) ((s₂, s₁.tail).snd, (s₂, s₁.tail).fst.tail) =
    s₁.head :: s₂.head :: t

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (match (s₁, s₂) with
      | (s₁, snd) => s₁.head) ::
      corec
        (fun x =>
          match x with
          | (s₁, snd) => s₁.head)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (match (s₁, s₂) with
        | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t

Tactic:
dsimp

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁.head :: corec (fun x => x.fst.head) (fun x => (x.snd, x.fst.tail)) (s₂, s₁.tail) = s₁.head :: s₂.head :: t

Proof state:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: t

Tactic:
unfold interleave

Result:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (corecOn (s₁, s₂)
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      fun x =>
      match x with
      | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t