-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
rw :
  Eq.{u + 1} (α := α ⊕ 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 α))
              S.destruct 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) :
      α ⊕ Computation α)
    (Sum.inr
        (corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            some (some c, S.tail) with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))) :
      α ⊕ Computation α)
⊢ Eq.{u + 1} (α := α ⊕ 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 α))
              S.destruct 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) :
      α ⊕ Computation α)
    (Sum.inr
        (corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            some (some c, S.tail) with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))) :
      α ⊕ Computation α)
have rw₁ : Eq.{u + 1} (α := α ⊕ 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 α))
            some (some c, S.tail) 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) :
    α ⊕ Computation α)
  (Sum.inr
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))) :
    α ⊕ Computation α)
Tactic: rw [h, H]