-- Mathlib/Data/Seq/Parallel.lean
theorem exists_of_mem_parallel {S : WSeq (Computation α)} {a} (h : a ∈ parallel S) :
    ∃ c ∈ S, a ∈ c

Proof state:
case cons.inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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:
refine ⟨c, List.mem_cons_self _ _, ?_⟩

Result:
case cons.inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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 ∈ c

Proof state:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c
l : List (Computation α)
⊢ F l (parallel.aux2 l)

Tactic:
induction' l with c l IH <;> simp only [parallel.aux2, List.foldr]

Result:
case nil
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c
⊢ F [] (Sum.inr [])

case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c
c : Computation α
l : List (Computation α)
IH : F l (parallel.aux2 l)
⊢ F (c :: l)
    (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls => rmap (fun c' => c' :: ls) c.destruct)
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' => c' :: ls) c.destruct)

Proof state:
case h2.inr.some.mk.some.intro.intro.inl.inl
α : Type u
S✝ : WSeq (Computation α)
a : α
h : a ∈ parallel S✝
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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, (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')
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

Result:
no goals

Proof state:
case cons.inr.inr.intro.intro
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Tactic:
simp only [List.mem_cons] at dm

Result:
case cons.inr.inr.intro.intro
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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 α
ad : a' ∈ d
dm : d = c' ∨ d ∈ val✝
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Proof state:
case inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S
l : List (Computation α)
a : α
⊢ Prop

Tactic:
exact ∃ c ∈ l, a ∈ c

Result:
no goals

Proof state:
case cons.inr.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝¹ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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' : α
h : ∃ c, c ∈ c' :: val✝ ∧ a' ∈ c
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Tactic:
rcases h with ⟨d, dm, ad⟩

Result:
case cons.inr.inr.intro.intro
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Proof state:
case cons.inr.inr.intro.intro
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Tactic:
simp? at dm says simp only [List.mem_cons] at dm

Result:
case cons.inr.inr.intro.intro
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a =>
    Sum.casesOn a (fun a => ∃ c, c ∈ l ∧ a ∈ c) fun l' => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ 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 α
ad : a' ∈ d
dm : d = c' ∨ d ∈ val✝
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1