-- 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 α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
inl :
  ∀ (a : α),
    match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
      match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
        match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β))
          match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) Sum.inl a with
            | Sum.inl a => Sum.inl a
            | Sum.inr b =>
              Sum.inr
                (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                  Seq.destruct S with
                | none => (b, Seq.nil)
                | some (none, S') => (b, S')
                | some (some c, S') => (c :: b, S')) with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (map f b) with
      | Sum.inl a => Sum.inl (f a)
      | Sum.inr b => Sum.inr b,
      match (motive := β ⊕ List (Computation β) × WSeq (Computation β) → β ⊕ Computation β)
        match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β) × WSeq (Computation β))
          lmap f (rmap (List.map (map f)) (Sum.inl a)) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
              Seq.destruct (WSeq.map (map f) S) with
            | none => (b, Seq.nil)
            | some (none, S') => (b, S')
            | some (some c, S') => (c :: b, S')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' =>
      ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
        s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
    | x, x_1 => False
⊢ match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
      match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β))
        match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
          match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α))
            parallel.aux2 l with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match (motive := β ⊕ List (Computation β) × WSeq (Computation β) → β ⊕ Computation β)
      match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β) × WSeq (Computation β))
        lmap f (rmap (List.map (map f)) (parallel.aux2 l)) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
      s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False
have inr : ∀ (l' : List (Computation α)),
  match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
      match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β))
        match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
          match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) Sum.inr l' with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match (motive := β ⊕ List (Computation β) × WSeq (Computation β) → β ⊕ Computation β)
      match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β) × WSeq (Computation β))
        lmap f (rmap (List.map (map f)) (Sum.inr l')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
      s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False
Tactic: rcases parallel.aux2 l with a | l'