awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
a' : α
this : F l (Sum.inl a')
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          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'))
        (Sum.inl a')) =
    Sum.inr C'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
injection e'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
e' :
  Eq (α := α ⊕ Computation α)
    (rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          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'))
        (Sum.inr l')))
    (Sum.inr C')
⊢ corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'

Tactic:
injection e' with h'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
h1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)) (e : corec parallel.aux1 (l, S) = pure a) (a' : α)
    (this : F l (Sum.inl a')) (h' : a' = a), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2 :
  ∀ (C' : Computation α)
    (IH :
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c)
    (l : List (Computation α)) (S : WSeq (Computation α)) (e : corec parallel.aux1 (l, S) = C'.think)
    (l' : List (Computation α)) (this : F l (Sum.inr l'))
    (h' :
      corec parallel.aux1
          ((fun (l' : List (Computation α)) ↦
              (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') :
                List (Computation α) × WSeq (Computation α)))
            l') =
        C'),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l <;> simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e' <;>
    revert this e' <;> rcases parallel.aux2 l with a' | l' <;> intro this e' <;>
    [injection e' with h'; injection e'; injection e'; injection e' with h']

Premises used: Computation.memRecOn, Computation.destruct_pure, _private.0.Computation.parallel.aux1, Computation.destruct_think, Computation.corec_eq
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
this : F l (Sum.inl a')
h' : a' = a
⊢ F l (Sum.inl a)

Tactic:
rw [h'] at this
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
this : F l (Sum.inl a')
h' : a' = a
this₁ : F l (Sum.inl a)
⊢ a' = a

Tactic:
rw [h'] at this
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
this : F l (Sum.inl a)
h' : a' = a
h1 : ∀ (c : Computation α) (cl : c ∈ l) (ac : a ∈ c), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases this with ⟨c, cl, ac⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
h' : a' = a
c : Computation α
cl : c ∈ l
ac : a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
⟨c, Or.inl cl, ac⟩

Premises used: And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
a' : α
h' : a' = a
c : Computation α
cl : c ∈ l
ac : a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
exact ⟨c, Or.inl cl, ac⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
h2 : ∀ (e : Seq.destruct S = none), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2₁ :
  ∀ (a_1 : Seq1 (Option (Computation α))) (e : Seq.destruct S = some a_1),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases e : Seq.destruct S with - | a

Premises used: Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = none
⊢ corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              none with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'

Tactic:
rw [e] at h'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = none
h'₁ :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              none with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
⊢ Seq.destruct S = none

Tactic:
rw [e] at h'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a_1 : α
h : a_1 ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a_1 ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
a : Seq1 (Option (Computation α))
e : Seq.destruct S = some a
⊢ corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              some a with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'

Tactic:
rw [e] at h'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a_1 : α
h : a_1 ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a_1 ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
a : Seq1 (Option (Computation α))
e : Seq.destruct S = some a
h'₁ :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              some a with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
⊢ Seq.destruct S = some a

Tactic:
rw [e] at h'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              none with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = none
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
let ⟨d, o, ad⟩ := IH _ _ h'
        let ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (WSeq.notMem_nil _), ad⟩
        ⟨c, Or.inl cl, ac⟩

Premises used: _private.0.Computation.exists_of_mem_parallel.match_2, Membership.mem, Exists, Stream'.Seq.nil, And, And.intro, Exists.intro, Stream'.WSeq.notMem_nil, Or.inl, Or, Or.resolve_right, _private.0.Computation.exists_of_mem_parallel.match_3
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              none with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = none
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
exact
        let ⟨d, o, ad⟩ := IH _ _ h'
        let ⟨c, cl, ac⟩ := this a ⟨d, o.resolve_right (WSeq.notMem_nil _), ad⟩
        ⟨c, Or.inl cl, ac⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S_1 : WSeq (Computation α)
a_1 : α
h : a_1 ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a_1 ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
a : Seq1 (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              some a with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = some a
h2 :
  ∀ (o : Option (Computation α)) (S' : Stream'.Seq (Option (Computation α)))
    (h' :
      corec parallel.aux1
          ((fun (l' : List (Computation α)) ↦
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                  some (o, S') with
                | none => (l', Seq.nil)
                | some (none, S') => (l', S')
                | some (some c, S') => (c :: l', S') :
                List (Computation α) × WSeq (Computation α)))
            l') =
        C')
    (e : Seq.destruct S = some (o, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c

Tactic:
obtain ⟨o, S'⟩ := a