awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e : parallel.aux2 l = Sum.inl a'
a₁ :
  ∃ (a : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
          List.foldr
            (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
              match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
              | Sum.inl a => Sum.inl a
              | Sum.inr ls =>
                match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                | Sum.inl a => Sum.inl a
                | Sum.inr b => Sum.inr (b :: ls))
            (Sum.inr []) l with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
        α ⊕ List (Computation α))
      (Sum.inl a : α ⊕ List (Computation α))
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a

Tactic:
simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e

Premises used: List.foldr_cons, Computation.rmap, _private.0.Computation.parallel.aux2
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  Eq (α := α ⊕ List (Computation α))
    (List.foldr
      (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inl a')
a₁ :
  ∃ (a : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl a' with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
        α ⊕ List (Computation α))
      (Sum.inl a : α ⊕ List (Computation α))
⊢ ∃ (a : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
          List.foldr
            (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
              match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
              | Sum.inl a => Sum.inl a
              | Sum.inr ls =>
                match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                | Sum.inl a => Sum.inl a
                | Sum.inr b => Sum.inr (b :: ls))
            (Sum.inr []) l with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
        α ⊕ List (Computation α))
      (Sum.inl a : α ⊕ List (Computation α))

Tactic:
rw [e]
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  Eq (α := α ⊕ List (Computation α))
    (List.foldr
      (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inl a')
⊢ ∃ (a : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl a' with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
        α ⊕ List (Computation α))
      (Sum.inl a : α ⊕ List (Computation α))

Tactic:
⟨a', rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  Eq (α := α ⊕ List (Computation α))
    (List.foldr
      (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inl a')
⊢ ∃ (a : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl a' with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
        α ⊕ List (Computation α))
      (Sum.inl a : α ⊕ List (Computation α))

Tactic:
exact ⟨a', rfl⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
m : Membership.mem (γ := List (Computation α)) [] s.think
l' : List (Computation α)
e' : parallel.aux2 [] = Sum.inr l'
⊢ s ∈ l'

Tactic:
simp at m
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
m : s.think ∈ c :: l
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
⊢ s ∈ l'

Tactic:
?_
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
l' : List (Computation α)
e' : parallel.aux2 l = Sum.inr l'
cons :
  ∀ (c : Computation α) (l : List (Computation α))
    (IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l')
    (m : s.think ∈ c :: l) (l' : List (Computation α)) (e' : parallel.aux2 (c :: l) = Sum.inr l'), s ∈ l'
⊢ s ∈ l'

Tactic:
induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_

Premises used: Stream'.cons
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
m : s.think ∈ c :: l
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
⊢ s.think = c ∨ s.think ∈ l

Tactic:
simp only [List.mem_cons] at m

Premises used: List.mem_cons
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think = c ∨ s.think ∈ l
cons : ∀ (e : s.think = c), s ∈ l'
cons₁ : ∀ (m : s.think ∈ l), s ∈ l'
⊢ s ∈ l'

Tactic:
rcases m with e | m
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
e : s.think = c
⊢ Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))

Tactic:
rw [← e] at e'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
e : s.think = c
e'₁ :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
⊢ s.think = c

Tactic:
rw [← e] at e'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
e : s.think = c
cons :
  ∀
    (e' :
      Eq (α := α ⊕ List (Computation α))
        (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
            List.foldr
              (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
                match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
                | Sum.inl a => Sum.inl a
                | Sum.inr ls =>
                  match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                  | Sum.inl a => Sum.inl a
                  | Sum.inr b => Sum.inr (b :: ls))
              (Sum.inr []) l with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls) :
          α ⊕ List (Computation α))
        (Sum.inr l' : α ⊕ List (Computation α))),
    s ∈ l'
⊢ s ∈ l'

Tactic:
revert e'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e : s.think = c
h_1 :
  ∀ (o : α ⊕ List (Computation α)) (a : α),
    Eq (α := α ⊕ List (Computation α))
        (List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l)
        (Sum.inl a) →
      ∀ (e' : Sum.inl a = Sum.inr l'), s ∈ l'
h_2 :
  ∀ (o : α ⊕ List (Computation α)) (ls : List (Computation α)),
    Eq (α := α ⊕ List (Computation α))
        (List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l)
        (Sum.inr ls) →
      ∀
        (e' :
          Eq (α := α ⊕ List (Computation α))
            (match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls) :
              α ⊕ List (Computation α))
            (Sum.inr l' : α ⊕ List (Computation α))),
        s ∈ l'
⊢ ∀
    (e' :
      Eq (α := α ⊕ List (Computation α))
        (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
            List.foldr
              (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
                match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
                | Sum.inl a => Sum.inl a
                | Sum.inr ls =>
                  match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                  | Sum.inl a => Sum.inl a
                  | Sum.inr b => Sum.inr (b :: ls))
              (Sum.inr []) l with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls) :
          α ⊕ List (Computation α))
        (Sum.inr l' : α ⊕ List (Computation α))),
    s ∈ l'

Tactic:
split
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e : s.think = c
o : α ⊕ List (Computation α)
a : α
heq :
  Eq (α := α ⊕ List (Computation α))
    (List.foldr
      (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inl a)
⊢ ∀ (e' : Sum.inl a = Sum.inr l'), s ∈ l'

Tactic:
simp
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e : s.think = c
o : α ⊕ List (Computation α)
ls : List (Computation α)
heq :
  Eq (α := α ⊕ List (Computation α))
    (List.foldr
      (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inr ls)
h_2 : ∀ (e' : s :: ls = l'), s ∈ l'
⊢ ∀
    (e' :
      Eq (α := α ⊕ List (Computation α))
        (match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
          α ⊕ List (Computation α))
        (Sum.inr l' : α ⊕ List (Computation α))),
    s ∈ l'

Tactic:
simp only [destruct_think, Sum.inr.injEq]

Premises used: Sum.inr.injEq, Computation.destruct_think
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
e : s.think = c
o : α ⊕ List (Computation α)
ls : List (Computation α)
heq :
  Eq (α := α ⊕ List (Computation α))
    (List.foldr
      (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inr ls)
⊢ s ∈ s :: ls

Tactic:
simp