awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d_1 : Computation α
dm_1 : d_1 ∈ c' :: val
ad : a' ∈ d_1
dl : d_1 ∈ val
d : Computation α
dm : d ∈ l ∧ a' ∈ d
⊢ d ∈ l

Tactic:
obtain ⟨dm, ad⟩ := dm
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d_1 : Computation α
dm_1 : d_1 ∈ c' :: val
ad : a' ∈ d_1
dl : d_1 ∈ val
d : Computation α
dm : d ∈ l ∧ a' ∈ d
dm₁ : d ∈ l
⊢ a' ∈ d

Tactic:
obtain ⟨dm, ad⟩ := dm
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d_1 : Computation α
dm_1 : d_1 ∈ c' :: val
ad_1 : a' ∈ d_1
dl : d_1 ∈ val
d : Computation α
dm : d ∈ l
ad : a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
⟨d, List.Mem.tail _ dm, ad⟩

Premises used: List.Mem.tail, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d_1 : Computation α
dm_1 : d_1 ∈ c' :: val
ad_1 : a' ∈ d_1
dl : d_1 ∈ val
d : Computation α
dm : d ∈ l
ad : a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
exact ⟨d, List.Mem.tail _ dm, ad⟩
-- 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
⊢ ∀ (l : List (Computation α)), F l (parallel.aux2 l)

Tactic:
have lem1 (l) : F l (parallel.aux2 l) := by
    induction l <;> simp only [parallel.aux2, List.foldr]
    case nil =>
      intro a h
      assumption
    case cons c l IH =>
      simp only [parallel.aux2] at IH
      -- Porting note: `revert IH` & `intro IH` are required.
      revert IH
      cases 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 <;>
        intro IH <;> simp only
      · rcases IH with ⟨c', cl, ac⟩
        exact ⟨c', List.Mem.tail _ cl, ac⟩
      · rcases h : destruct c with a | c' <;> simp only [rmap]
        · refine ⟨c, List.mem_cons_self, ?_⟩
          rw [destruct_eq_pure h]
          apply ret_mem
        · intro a' h
          rcases h with ⟨d, dm, ad⟩
          rcases List.mem_cons.mp dm with e | dl
          · rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad
          · obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩
-- 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 α)),
    corec parallel.aux1 (l, S) = pure a → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2 :
  ∀ (s : Computation α),
    (∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = s → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c) →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = s.think → ∃ (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

Premises used: Computation.memRecOn
-- 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 α)),
    corec parallel.aux1 (l, S) = pure 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 α)),
    corec parallel.aux1 (l, S) = C'.think → ∃ (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]

Premises used: Computation.memRecOn
-- 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
⊢ (corec parallel.aux1 (l, S)).destruct = (pure a).destruct

Tactic:
have e' := congr_arg destruct 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
⊢ (corec parallel.aux1 (l, S)).destruct = C'.think.destruct

Tactic:
have e' := congr_arg destruct 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
⊢ F l (parallel.aux2 l)

Tactic:
have := lem1 l
-- 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
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
⊢ F l (parallel.aux2 l)

Tactic:
have := lem1 l
-- 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
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
this : F l (parallel.aux2 l)
⊢ 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'))
        (parallel.aux2 l)))
    (Sum.inl a)

Tactic:
simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'

Premises used: 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
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
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
this : F l (parallel.aux2 l)
⊢ 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'))
        (parallel.aux2 l)) =
    Sum.inr C'

Tactic:
simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'

Premises used: 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
this : F l (parallel.aux2 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'))
        (parallel.aux2 l)))
    (Sum.inl a)
h1 :
  ∀ (this : F l (parallel.aux2 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'))
            (parallel.aux2 l)))
        (Sum.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
revert this 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
this : F l (parallel.aux2 l)
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'))
        (parallel.aux2 l)) =
    Sum.inr C'
h2 :
  ∀ (this : F l (parallel.aux2 l))
    (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'))
            (parallel.aux2 l)) =
        Sum.inr C'),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
revert this 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
h1 :
  ∀ (a' : α) (this : F l (Sum.inl a'))
    (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.inl a')))
        (Sum.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h1₁ :
  ∀ (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.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (this : F l (parallel.aux2 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'))
            (parallel.aux2 l)))
        (Sum.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

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

Premises used: _private.0.Computation.parallel.aux2
-- 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
h2 :
  ∀ (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
h2₁ :
  ∀ (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')),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (this : F l (parallel.aux2 l))
    (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'))
            (parallel.aux2 l)) =
        Sum.inr C'),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

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

Premises used: _private.0.Computation.parallel.aux2
-- 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')
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.inl a')))
    (Sum.inl a)
⊢ a' = a

Tactic:
injection e' with 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
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.inl a)
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
injection e'