-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
nil :
  Eq (α := β ⊕ List (Computation β))
    (List.foldr
      (fun (c : Computation β) (o : β ⊕ List (Computation β)) ↦
        match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) []))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) [] with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b)
⊢ Eq (α := β ⊕ List (Computation β))
    (List.foldr
      (fun (c : Computation β) (o : β ⊕ List (Computation β)) ↦
        match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) l))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b)
have cons : ∀ (c : Computation α) (l : List (Computation α))
  (IH :
    Eq (α := β ⊕ List (Computation β))
      (List.foldr
        (fun (c : Computation β) (o : β ⊕ List (Computation β)) ↦
          match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β)) o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) (List.map (map f) l))
      (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
        match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
          List.foldr
            (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
              match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
              | Sum.inl a => Sum.inl a
              | Sum.inr ls =>
                match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                | Sum.inl a => Sum.inl a
                | Sum.inr b => Sum.inr (b :: ls))
            (Sum.inr []) l with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (List.map (map f) b) with
      | Sum.inl a => Sum.inl (f a)
      | Sum.inr b => Sum.inr b)),
  Eq (α := β ⊕ List (Computation β))
    (List.foldr
      (fun (c : Computation β) (o : β ⊕ List (Computation β)) ↦
        match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) (c :: l)))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) (c :: l) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b)
Tactic: induction l with
        | nil => simp
        | cons c l IH =>
          simp only [List.map_cons, List.foldr_cons, destruct_map, lmap, rmap]
          rw [IH]
          cases List.foldr _ _ _
          · simp
          · cases destruct c <;> simp
Cleared hypotheses: l