awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ (corec parallel.aux1 (l, S)).destruct =
    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')))
have simp : 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 α)
Tactic: simp only [corec_eq, rmap, parallel.aux1.eq_1]
-- 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'
⊢ 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 α))
            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 α)
Tactic: rw [h, H]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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'
⊢ (corec parallel.aux1 (l, S)).Terminates
have C : corec parallel.aux1 (l, S) =
  think
    (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')))
Tactic: have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h, H])
-- 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'
C :
  corec parallel.aux1 (l, S) =
    think
      (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')))
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : Terminates.{u} (α := α)
  (think
    (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'))))
Tactic: rw [C]
-- 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'
C :
  corec parallel.aux1 (l, S) =
    think
      (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')))
⊢ Terminates.{u} (α := α)
    (think
      (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'))))
have inr : Terminates.{u} (α := α)
  (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')))
Tactic: refine @Computation.think_terminates _ _ ?_
-- 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'
C :
  corec parallel.aux1 (l, S) =
    think
      (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')))
⊢ Terminates.{u} (α := α)
    (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')))
have apply : c ∈ c :: l'
Tactic: apply terminates_parallel.aux _ T
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? (n + 1)
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inl : ∀ (a : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases o with a | a
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? (n + 1)
T : c.Terminates
inl : ∀ (a : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : ∀ (a : some (some c) = S.get? (n + 1)), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases o with a | a
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases h : parallel.aux2 l with a | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
inr : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr₁ : ∀ (l' : List (Computation α)) (h : parallel.aux2 l = Sum.inr l'), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases h : parallel.aux2 l with a | l'
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = pure a
have a₁ : (corec parallel.aux1 (l, S)).destruct = Sum.inl a
Tactic: apply destruct_eq_pure
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inl a
have a₁ : Eq (α := α ⊕ Computation α)
  (rmap (corec parallel.aux1)
    (rmap
      (fun (l' : List (Computation α)) ↦
        match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))
      (parallel.aux2 l)))
  (Sum.inl a)
Tactic: rw [corec_eq, parallel.aux1]
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Eq (α := α ⊕ Computation α)
    (rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            S.destruct with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)))
    (Sum.inl a)
have a₁ : Eq (α := α ⊕ Computation α)
  (rmap (corec parallel.aux1)
    (rmap
      (fun (l' : List (Computation α)) ↦
        match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))
      (Sum.inl a)))
  (Sum.inl a)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
have C : corec parallel.aux1 (l, S) = pure a
Tactic: have C : corec parallel.aux1 (l, S) = pure a := by
        apply destruct_eq_pure
        rw [corec_eq, parallel.aux1]
        rw [h]
        simp only [rmap]
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : (pure a).Terminates
Tactic: rw [C]
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).destruct =
    Sum.inr
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
have simp : 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 α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))) :
    α ⊕ Computation α)
Tactic: simp only [corec_eq, rmap, parallel.aux1.eq_1]
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ 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 α))
            S.destruct 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 α))
            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 α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))) :
    α ⊕ Computation α)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates
have C : corec parallel.aux1 (l, S) =
  think
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        S.destruct with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
Tactic: have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h])
-- 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
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : Terminates.{u} (α := α)
  (think
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        S.destruct with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))))
Tactic: rw [C]