-- Mathlib/Data/Seq/Parallel.lean
theorem terminates_parallel.aux :
    ∀ {l : List (Computation α)} {S c},
      c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S))

Proof state:
case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
this : s ∈ l'
⊢ (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S'))).Terminates

Tactic:
rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> simp [parallel.aux1] <;> apply IH <;>
  simp [this]

Result:
no goals

Proof state:
case a
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inl a

Tactic:
simp only [parallel.aux1, rmap, corec_eq]

Result:
case a
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inl a

Proof state:
case a
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 l = Sum.inl a

Tactic:
induction' l with c l IH <;> simp at m

Result:
case a.cons
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a = c ∨ pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

Proof state:
case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
have H2 : corec parallel.aux1 (l, S) = think _ := destruct_eq_think (by
  simp only [parallel.aux1, rmap, corec_eq]
  rw [h])

Result:
case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1 (l, S)).Terminates

Proof state:
case cons
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think = c ∨ s.think ∈ l
⊢ s ∈ l'

Tactic:
rcases m with e | m <;> simp [parallel.aux2] at e'

Result:
case cons.inl
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : s.think = c
⊢ s ∈ l'

case cons.inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
m : s.think ∈ l
⊢ s ∈ l'

Proof state:
α : Type u
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates

Tactic:
intro l S e

Result:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ a, parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates