-- 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
α : 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✝)
⊢ F (c :: l) (rmap (fun c' => c' :: val✝) c.destruct)

Tactic:
induction' h : destruct c with a c' <;> simp only [rmap]

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
⊢ F (c :: l) (Sum.inl a)

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'
⊢ F (c :: l) (Sum.inr (c' :: val✝))

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

Tactic:
rcases a with a | l'

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

case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
l l' : List (Computation α)
⊢ Prop

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 ∈ S

Tactic:
rw [Seq.destruct_eq_cons e]

Result:
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'

Proof state:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ List (Computation α) → α ⊕ List (Computation α) → Prop

Tactic:
intro l a

Result:
α : Type u
S : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S
l : List (Computation α)
a : α ⊕ List (Computation α)
⊢ Prop

Proof state:
case h1.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
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, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rw [h'] at this

Result:
case h1.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
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, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Proof state:
case cons.inr.inr.intro.intro.inr.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✝
dl : d✝ ∈ val✝
d : Computation α
dm : d ∈ l ∧ a' ∈ d
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Tactic:
obtain ⟨dm, ad⟩ := dm

Result:
case cons.inr.inr.intro.intro.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✝
dl : d✝ ∈ val✝
d : Computation α
dm : d ∈ l
ad : a' ∈ d
⊢ ∃ c_1, c_1 ∈ c :: l ∧ a' ∈ c_1

Proof state:
case h2.inr.some.mk.none.intro.intro.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
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 α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ d ∈ S

Tactic:
rw [Seq.destruct_eq_cons e]

Result:
case h2.inr.some.mk.none.intro.intro.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
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 α))
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'