-- 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 h2.inr.some
α : 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')
a : Seq1 (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' =>
          match some a with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a✝ ∈ c

Tactic:
obtain ⟨o, S'⟩ := a

Result:
case h2.inr.some.mk
α : 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')
o : Option (Computation α)
S' : Stream'.Seq (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' =>
          match some (o, S') with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some (o, S')
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Proof state:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ ∃ 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⟩

Result:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ ∀ (C : Computation α),
    a ∈ C →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

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:
rcases this with ⟨c, cl, ac⟩

Result:
case h1.inl.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
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' : α
h' : a' = a
c : Computation α
cl : c ∈ l
ac : a ∈ c
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

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

Tactic:
rw [Seq.destruct_eq_cons e]

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

Proof state:
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
a : α
h : ∃ c, c ∈ [] ∧ a ∈ c
⊢ ∃ c, c ∈ [] ∧ a ∈ c

Tactic:
rcases h with ⟨c, hn, _⟩

Result:
case nil.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
a : α
c : Computation α
hn : c ∈ []
right✝ : a ∈ c
⊢ ∃ c, c ∈ [] ∧ a ∈ c

Proof state:
case nil.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
a : α
c : Computation α
hn : c ∈ []
right✝ : a ∈ c
⊢ ∃ c, c ∈ [] ∧ a ∈ c

Tactic:
exact False.elim <| List.not_mem_nil _ hn

Result:
no goals

Proof state:
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

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

Result:
no goals