awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
a₁ :
  ∀ (C : Computation α),
    a ∈ C →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = C → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ c ∈ S, a ∈ c

Tactic:
suffices
    ∀ C, a ∈ C → ∀ (l : List (Computation α)) (S),
      corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c from
    let ⟨c, h1, h2⟩ := this _ h [] S rfl
    ⟨c, h1.resolve_left <| List.not_mem_nil, h2⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h : a_1 ∈ parallel S
l : List (Computation α)
a : α ⊕ List (Computation α)
inl : (a : α) → Prop
inr : (l' : List (Computation α)) → Prop
⊢ Prop

Tactic:
rcases a with a | l'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h : a_1 ∈ parallel S
l : List (Computation α)
a : α
⊢ Prop

Tactic:
exact ∃ c ∈ l, a ∈ c
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
l l' : List (Computation α)
⊢ Prop

Tactic:
exact ∀ a', (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
-- 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 α)
nil : F [] (parallel.aux2 [])
cons :
  ∀ (head : Computation α) (tail : List (Computation α)),
    F tail (parallel.aux2 tail) → F (head :: tail) (parallel.aux2 (head :: tail))
⊢ F l (parallel.aux2 l)

Tactic:
induction l
-- 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
simp : F [] (Sum.inr [])
⊢ F [] (parallel.aux2 [])

Tactic:
simp only [parallel.aux2, List.foldr]

Premises used: List.foldr, _private.0.Computation.parallel.aux2
-- 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
head : Computation α
tail : List (Computation α)
tail_ih : F tail (parallel.aux2 tail)
cons :
  F (head :: tail)
    (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
        (Sum.inr []) tail with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) head.destruct)
⊢ F (head :: tail) (parallel.aux2 (head :: tail))

Tactic:
simp only [parallel.aux2, List.foldr]

Premises used: List.foldr, _private.0.Computation.parallel.aux2
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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
a : α
h : ∃ (c : Computation α), Membership.mem (γ := List (Computation α)) [] c ∧ a ∈ c
⊢ ∃ (c : Computation α), Membership.mem (γ := List (Computation α)) [] c ∧ a ∈ c

Tactic:
assumption
-- 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
⊢ F [] (Sum.inr [])

Tactic:
case nil =>
      intro a h
      assumption
-- 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
c : Computation α
l : List (Computation α)
IH :
  F l
    (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)
revert :
  ∀
    (IH :
      F l
        (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)),
    F (c :: l)
      (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
⊢ F (c :: l)
    (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)

Tactic:
revert IH
-- 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
c : Computation α
l : List (Computation α)
inl :
  ∀ (val : α) (IH : F l (Sum.inl val)),
    F (c :: l)
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl val with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
inr :
  ∀ (val : List (Computation α)) (IH : F l (Sum.inr val)),
    F (c :: l)
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr val with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
⊢ ∀
    (IH :
      F l
        (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)),
    F (c :: l)
      (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)

Tactic:
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

Premises used: Sum.inr, List.foldr, List.nil
-- 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
c : Computation α
l : List (Computation α)
val : α
IH : F l (Sum.inl val)
inl : F (c :: l) (Sum.inl val)
⊢ F (c :: l)
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl val with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)

Tactic:
simp only
-- 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
inr : F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) c.destruct)
⊢ F (c :: l)
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr val with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)

Tactic:
simp only
-- 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
c : Computation α
l : List (Computation α)
val : α
IH : F l (Sum.inl val)
inl : ∀ (c' : Computation α) (cl : c' ∈ l) (ac : val ∈ c'), F (c :: l) (Sum.inl val)
⊢ F (c :: l) (Sum.inl val)

Tactic:
rcases IH with ⟨c', cl, ac⟩
-- 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
c : Computation α
l : List (Computation α)
val : α
c' : Computation α
cl : c' ∈ l
ac : val ∈ c'
⊢ F (c :: l) (Sum.inl val)

Tactic:
⟨c', List.Mem.tail _ cl, ac⟩

Premises used: List.Mem.tail, And.intro, Exists.intro
-- 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
c : Computation α
l : List (Computation α)
val : α
c' : Computation α
cl : c' ∈ l
ac : val ∈ c'
⊢ F (c :: l) (Sum.inl val)

Tactic:
exact ⟨c', List.Mem.tail _ cl, ac⟩
-- 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
inr : ∀ (a : α) (h : c.destruct = Sum.inl a), F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inl a))
inr₁ :
  ∀ (c' : Computation α) (h : c.destruct = Sum.inr c'),
    F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inr c'))
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) c.destruct)

Tactic:
rcases h : destruct c with a | c'

Premises used: Computation.destruct
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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)
a : α
h : c.destruct = Sum.inl a
inr : F (c :: l) (Sum.inl a)
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inl a))

Tactic:
simp only [rmap]

Premises used: Computation.rmap
-- 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'
inr : F (c :: l) (Sum.inr (c' :: val))
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inr c'))

Tactic:
simp only [rmap]

Premises used: Computation.rmap
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (Sum.inl a)

Tactic:
⟨c, List.mem_cons_self, ?_⟩

Premises used: And.intro, Exists.intro, List.mem_cons_self
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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)
a : α
h : c.destruct = Sum.inl a
inr : a ∈ c
⊢ F (c :: l) (Sum.inl a)

Tactic:
refine ⟨c, List.mem_cons_self, ?_⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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)
a : α
h : c.destruct = Sum.inl a
inr : a ∈ pure a
⊢ a ∈ c

Tactic:
rw [destruct_eq_pure h]

Premises used: Computation.destruct_eq_pure
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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)
a : α
h : c.destruct = Sum.inl a
⊢ a ∈ pure a

Tactic:
apply ret_mem

Premises used: Computation.ret_mem
-- 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_2 : c.destruct = Sum.inr c'
a' : α
h : ∃ c ∈ c' :: val, a' ∈ c
inr : ∀ (d : Computation α) (dm : d ∈ c' :: val) (ad : a' ∈ d), ∃ c_1 ∈ c :: l, a' ∈ c_1
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
rcases h with ⟨d, dm, ad⟩
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
inr : ∀ (e : d = c'), ∃ c_1 ∈ c :: l, a' ∈ c_1
inr₁ : ∀ (dl : d ∈ val), ∃ c_1 ∈ c :: l, a' ∈ c_1
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
rcases List.mem_cons.mp dm with e | dl

Premises used: Iff.mp, List.mem_cons
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
e : d = c'
⊢ a' ∈ c'

Tactic:
rw [e] at ad
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
e : d = c'
ad₁ : a' ∈ c'
⊢ d = c'

Tactic:
rw [e] at ad
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
⟨c, List.mem_cons_self, ?_⟩

Premises used: And.intro, Exists.intro, List.mem_cons_self
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
inr : a' ∈ c
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
refine ⟨c, List.mem_cons_self, ?_⟩
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
inr : a' ∈ c'.think
⊢ a' ∈ c

Tactic:
rw [destruct_eq_think h]

Premises used: Computation.destruct_eq_think
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c'.think

Tactic:
think_mem ad

Premises used: Computation.think_mem
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c'.think

Tactic:
exact think_mem ad

Premises used: Computation.think_mem
-- 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 : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
dl : d ∈ val
inr : ∀ (d : Computation α) (dm : d ∈ l ∧ a' ∈ d), ∃ c_1 ∈ c :: l, a' ∈ c_1
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1

Tactic:
obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩

Premises used: And.intro, Exists.intro