awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
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'
rw 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 α)
⊢ 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:
rw [h]
-- Module: Mathlib.Data.Seq.Parallel
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) =
    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])
-- Module: Mathlib.Data.Seq.Parallel
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')))
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'))))
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rw [C]
-- Module: Mathlib.Data.Seq.Parallel
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')))
⊢ 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:
@Computation.think_terminates _ _ ?_

Premises used: Computation.think_terminates
-- Module: Mathlib.Data.Seq.Parallel
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')))
inr :
  Terminates.{u} (α := α)
    (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')))
⊢ 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:
refine @Computation.think_terminates _ _ ?_

Premises used: Computation.think_terminates
-- Module: Mathlib.Data.Seq.Parallel
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')))
l'_1 : List (Computation α)
apply : some (some c) = S.tail.get? n
⊢ (corec parallel.aux1 (l'_1, S.tail)).Terminates

Tactic:
apply IH _ _ _ (Or.inr _) T

Premises used: Or.inr
-- Module: Mathlib.Data.Seq.Parallel
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')))
l'_1 : List (Computation α)
rw : S.get? (n + 1) = S.tail.get? n
rw₁ rw₂ : S.get? (n + 1) = S.get? (n + 1)
⊢ some (some c) = S.tail.get? n

Tactic:
rw [a, Seq.get?_tail]

Premises used: Stream'.Seq.get?_tail
-- Module: Mathlib.Data.Seq.Parallel
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')))
⊢ ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates

Tactic:
have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by
        intro
        apply IH _ _ _ (Or.inr _) T
        rw [a, Seq.get?_tail]
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
inr :
  ∀ (e : S.get? 0 = none),
    Terminates.{u} (α := α)
      (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')))
inr₁ :
  ∀ (o : Option (Computation α)) (e : S.get? 0 = some o),
    Terminates.{u} (α := α)
      (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')))
⊢ Terminates.{u} (α := α)
    (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:
rcases e : Seq.get? S 0 with - | o

Premises used: OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
e : S.get? 0 = none
⊢ Terminates.{u} (α := α)
    (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:
grind [Seq.get?_zero_eq_none, Seq.get?_nil]

Premises used: Stream'.Seq.get?_zero_eq_none, Stream'.Seq.get?_nil
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
rw : Option.map (fun (a' : Option (Computation α)) ↦ (a', S.tail)) (some o) = some (o, S.tail)
⊢ Option.map (fun (a' : Option (Computation α)) ↦ (a', S.tail)) (S.get? 0) = some (o, S.tail)

Tactic:
rw [e]
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
⊢ Option.map (fun (a' : Option (Computation α)) ↦ (a', S.tail)) (some o) = some (o, S.tail)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
⊢ S.destruct = some (o, S.tail)

Tactic:
have D : Seq.destruct S = some (o, S.tail) := by
          dsimp [Seq.destruct]
          rw [e]
          rfl
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
D : S.destruct = some (o, S.tail)
inr :
  Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        some (o, 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 α))
        S.destruct with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))

Tactic:
rw [D]
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
o : Option (Computation α)
e : S.get? 0 = some o
D : S.destruct = some (o, S.tail)
inr :
  ∀ (e : S.get? 0 = some none) (D : S.destruct = some (none, S.tail)),
    Terminates.{u} (α := α)
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          some (none, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
inr₁ :
  ∀ (val : Computation α) (e : S.get? 0 = some (some val)) (D : S.destruct = some (some val, S.tail)),
    Terminates.{u} (α := α)
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          some (some val, 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 (o, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))

Tactic:
cases o
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
e : S.get? 0 = some none
D : S.destruct = some (none, S.tail)
⊢ Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        some (none, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))

Tactic:
simp [TT]
-- Module: Mathlib.Data.Seq.Parallel
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')))
TT : ∀ (l' : List (Computation α)), (corec parallel.aux1 (l', S.tail)).Terminates
val : Computation α
e : S.get? 0 = some (some val)
D : S.destruct = some (some val, S.tail)
⊢ Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        some (some val, S.tail) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))

Tactic:
simp [TT]