awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e : s.think = c
⊢ ∀
    (e' :
      Eq (α := α ⊕ List (Computation α))
        (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 =>
                  match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) 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 (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls) :
          α ⊕ List (Computation α))
        (Sum.inr l' : α ⊕ List (Computation α))),
    s ∈ l'
have h_1 : ∀ (o : α ⊕ List (Computation α)) (a : α),
  Eq (α := α ⊕ 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 =>
            match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l)
      (Sum.inl a) →
    ∀ (e' : Sum.inl a = Sum.inr l'), s ∈ l'
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e : s.think = c
h_1 :
  ∀ (o : α ⊕ List (Computation α)) (a : α),
    Eq (α := α ⊕ 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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l)
        (Sum.inl a) →
      ∀ (e' : Sum.inl a = Sum.inr l'), s ∈ l'
⊢ ∀
    (e' :
      Eq (α := α ⊕ List (Computation α))
        (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 =>
                  match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) 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 (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls) :
          α ⊕ List (Computation α))
        (Sum.inr l' : α ⊕ List (Computation α))),
    s ∈ l'
have h_2 : ∀ (o : α ⊕ List (Computation α)) (ls : List (Computation α)),
  Eq (α := α ⊕ 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 =>
            match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l)
      (Sum.inr ls) →
    ∀
      (e' :
        Eq (α := α ⊕ List (Computation α))
          (match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls) :
            α ⊕ List (Computation α))
          (Sum.inr l' : α ⊕ List (Computation α))),
      s ∈ l'
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e : s.think = c
o : α ⊕ List (Computation α)
ls : List (Computation α)
heq :
  Eq (α := α ⊕ 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 =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inr ls)
⊢ ∀
    (e' :
      Eq (α := α ⊕ List (Computation α))
        (match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) s.think.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) :
          α ⊕ List (Computation α))
        (Sum.inr l' : α ⊕ List (Computation α))),
    s ∈ l'
have h_2 : ∀ (e' : s :: ls = l'), s ∈ l'
Tactic: simp only [destruct_think, Sum.inr.injEq]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) 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 (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
m : s.think ∈ l
⊢ s ∈ l'
have cons : ∀ (a' : α)
  (e :
    Eq (α := α ⊕ 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)
      (Sum.inl a')),
  s ∈ l'
Tactic: rcases e : 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 with a' | ls
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) 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 (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
m : s.think ∈ l
cons :
  ∀ (a' : α)
    (e :
      Eq (α := α ⊕ 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)
        (Sum.inl a')),
    s ∈ l'
⊢ s ∈ l'
have cons₁ : ∀ (ls : List (Computation α))
  (e :
    Eq (α := α ⊕ 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)
      (Sum.inr ls)),
  s ∈ l'
Tactic: rcases e : 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 with a' | ls
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) 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 (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
m : s.think ∈ l
a' : α
e :
  Eq (α := α ⊕ 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 =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inl a')
⊢ s ∈ l'
have e'₁ : Eq (α := α ⊕ List (Computation α))
  (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls) :
    α ⊕ List (Computation α))
  (Sum.inr l' : α ⊕ List (Computation α))
Tactic: rw [e] at e'
Cleared hypotheses: e', e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) 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 (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
m : s.think ∈ l
ls : List (Computation α)
e :
  Eq (α := α ⊕ 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 =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inr ls)
⊢ s ∈ l'
have e'₁ : Eq (α := α ⊕ List (Computation α))
  (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls) :
    α ⊕ List (Computation α))
  (Sum.inr l' : α ⊕ List (Computation α))
Tactic: rw [e] at e'
Cleared hypotheses: e', e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
ls : List (Computation α)
e' :
  Eq (α := α ⊕ List (Computation α))
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr ls with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
e :
  Eq (α := α ⊕ 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 =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l)
    (Sum.inr ls)
⊢ s ∈ l'
have this : s ∈ ls
Tactic: have := IH' m _ e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : 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 α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
have H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
Tactic: have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' := by
      induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_
      simp only [List.mem_cons] at m
      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
      · rw [← e] at e'
        -- Porting note: `revert e'` is required.
        revert e'
        split
        · simp
        · simp only [destruct_think, Sum.inr.injEq]
          rintro rfl
          simp
      · rcases e : 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 with a' | ls <;> simp only [rmap] at e <;> rw [e] at e'
        · contradiction
        have := IH' m _ e
        grind
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : 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 α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
⊢ (corec parallel.aux1 (l, S)).Terminates
have inl : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases h : parallel.aux2 l with a | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : 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 α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
inl : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : ∀ (l' : List (Computation α)) (h : parallel.aux2 l = Sum.inr l'), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases h : parallel.aux2 l with a | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : 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 α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).destruct =
    Sum.inr
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
have simp : Eq.{u + 1} (α := α ⊕ Computation α)
  (match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
      match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            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) :
    α ⊕ Computation α)
  (Sum.inr
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))) :
    α ⊕ Computation α)
Tactic: simp only [parallel.aux1, rmap, corec_eq]