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
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 α))
m : s.think ∈ l
cons :
  ∀ (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
          (Sum.inr []) l)
        (Sum.inl a')),
    s ∈ l'
cons₁ :
  ∀ (ls : List (Computation α))
    (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
          (Sum.inr []) l)
        (Sum.inr ls)),
    s ∈ l'
⊢ s ∈ l'

Tactic:
rcases e : List.foldr (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
          (Sum.inr List.nil) l with a' | ls

Premises used: Sum.inr, List.foldr, List.nil
-- 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 α))
m : s.think ∈ 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')
⊢ 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.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 α))
m : s.think ∈ 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')
e'₁ :
  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.inr l' : α ⊕ 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.inl a')

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 α))
m : s.think ∈ l
ls : List (Computation α)
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.inr ls)
⊢ Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr ls 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 α))

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 α))
m : s.think ∈ l
ls : List (Computation α)
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.inr ls)
e'₁ :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr ls 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 α))
⊢ 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)

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 α)
m : s.think ∈ l
a' : α
e' :
  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.inr l' : α ⊕ List (Computation α))
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')
⊢ s ∈ l'

Tactic:
contradiction
-- 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 α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr ls 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 :
  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 ∈ ls

Tactic:
have := IH' m _ 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 α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr ls 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 :
  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)
this : s ∈ ls
⊢ s ∈ l'

Tactic:
grind
-- 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'), s ∈ l'

Tactic:
have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := by
      induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_
      simp only [List.mem_cons] at m
      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
      · rw [← e] at e'
        -- Porting note: `revert e'` is required.
        revert e'
        split
        · simp
        · simp only [destruct_think, Sum.inr.injEq]
          rintro rfl
          simp
      · rcases e : List.foldr (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
          (Sum.inr List.nil) l with a' | ls <;> simp only [rmap] at e <;> rw [e] at e'
        · contradiction
        have := IH' m _ e
        grind
-- 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
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
inl : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
inr : ∀ (l' : List (Computation α)) (h : parallel.aux2 l = Sum.inr l'), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rcases h : parallel.aux2 l with a | l'

Premises used: _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 : 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
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
lem1 _ _ ⟨a, h⟩

Premises used: Exists.intro
-- 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
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
exact lem1 _ _ ⟨a, h⟩

Premises used: Exists.intro
-- 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
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
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 α))
              Seq.destruct S 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 α))
            Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))) :
      α ⊕ Computation α)
⊢ (corec parallel.aux1 (l, S)).destruct =
    Sum.inr
      (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')))

Tactic:
simp only [parallel.aux1, rmap, corec_eq]

Premises used: Computation.rmap, _private.0.Computation.parallel.aux1, Computation.corec_eq