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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
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')
h2 :
  ∀
    (h' :
      corec parallel.aux1
          ((fun (l' : List (Computation α)) ↦
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                  some (none, 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 (none, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2₁ :
  ∀ (c : Computation α)
    (h' :
      corec parallel.aux1
          ((fun (l' : List (Computation α)) ↦
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                  some (some c, 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 (some c, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
obtain - | c := o
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
h2 : ∀ (d : Computation α) (ad : a ∈ d) (dl : d ∈ l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2₁ : ∀ (d : Computation α) (ad : a ∈ d) (dS' : d ∈ S'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases IH _ _ h' with ⟨d, dl | dS', ad⟩
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
h2 : ∀ (d : Computation α) (ad : a ∈ d) (dl : d ∈ c :: l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2₁ : ∀ (d : Computation α) (ad : a ∈ d) (dS' : d ∈ S'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases IH _ _ h' with ⟨d, dl | dS', ad⟩
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dl : d ∈ l'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
          ⟨c, Or.inl cl, ac⟩

Premises used: _private.0.Computation.exists_of_mem_parallel.match_2, Membership.mem, Exists, And, And.intro, Exists.intro, Or.inl, Or
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dl : d ∈ l'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
exact
          let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
          ⟨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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
⟨d, Or.inr ?_, ad⟩

Premises used: And.intro, Exists.intro, Or.inr
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
h2 : d ∈ S
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
refine ⟨d, Or.inr ?_, ad⟩
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
h2 : d ∈ Seq.cons none S'
⊢ d ∈ S

Tactic:
rw [Seq.destruct_eq_cons e]

Premises used: Stream'.Seq.destruct_eq_cons
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ d ∈ Seq.cons none S'

Tactic:
Seq.mem_cons_of_mem _ dS'

Premises used: Stream'.Seq.mem_cons_of_mem, Stream'.WSeq.Mem
-- 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')
S' : Stream'.Seq (Option (Computation α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ d ∈ Seq.cons none S'

Tactic:
exact Seq.mem_cons_of_mem _ dS'

Premises used: Stream'.Seq.mem_cons_of_mem
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dl : d ∈ c :: l'
⊢ d = c ∨ d ∈ l'

Tactic:
simp only [List.mem_cons] at dl

Premises used: List.mem_cons
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dl : d = c ∨ d ∈ l'
h2 : ∀ (dc : d = c), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
h2₁ : ∀ (dl : d ∈ l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases dl with dc | dl
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dc : d = c
⊢ a ∈ c

Tactic:
rw [dc] at ad
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dc : d = c
ad₁ : a ∈ c
⊢ d = c

Tactic:
rw [dc] at ad
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ c
dc : d = c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
⟨c, Or.inr ?_, ad⟩

Premises used: And.intro, Exists.intro, Or.inr
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ c
dc : d = c
h2 : c ∈ S
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
refine ⟨c, Or.inr ?_, ad⟩
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ c
dc : d = c
h2 : c ∈ Seq.cons (some c) S'
⊢ c ∈ S

Tactic:
rw [Seq.destruct_eq_cons e]

Premises used: Stream'.Seq.destruct_eq_cons
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ c
dc : d = c
⊢ c ∈ Seq.cons (some c) S'

Tactic:
apply Seq.mem_cons

Premises used: Stream'.Seq.mem_cons
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dl : d ∈ l'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
            ⟨c, Or.inl cl, ac⟩

Premises used: _private.0.Computation.exists_of_mem_parallel.match_2, Membership.mem, Exists, And, And.intro, Exists.intro, Or.inl, Or
-- 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')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dl : d ∈ l'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
exact
            let ⟨c, cl, ac⟩ := this a ⟨d, dl, ad⟩
            ⟨c, Or.inl cl, ac⟩