-- 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))
l' : List (Computation α)
inr :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct WSeq.nil with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))) =
        map f (corec parallel.aux1 (l, S)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) WSeq.nil) with
          | none => (List.map (map f) l', Seq.nil)
          | some (none, S') => (List.map (map f) l', S')
          | some (some c, S') => (c :: List.map (map f) l', S')) =
        corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
⊢ ∃ (l : List (Computation α)) (S_2 : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct S with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))) =
        map f (corec parallel.aux1 (l, S_2)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) S) with
          | none => (List.map (map f) l', Seq.nil)
          | some (none, S') => (List.map (map f) l', S')
          | some (some c, S') => (c :: List.map (map f) l', S')) =
        corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S_2)
have inr₁ : ∀ (x : Computation α) (s : WSeq (Computation α)),
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct (WSeq.cons x s) with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))) =
        map f (corec parallel.aux1 (l, S)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) (WSeq.cons x s)) with
          | none => (List.map (map f) l', Seq.nil)
          | some (none, S') => (List.map (map f) l', S')
          | some (some c, S') => (c :: List.map (map f) l', S')) =
        corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S