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
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have revert : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
Tactic: revert l S
Cleared hypotheses: l, S, m
-- 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
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
have apply : ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)} (m : pure a ∈ l),
  (corec parallel.aux1 (l, S)).Terminates
Tactic: apply @terminatesRecOn _ _ c T _ _
-- 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
apply :
  ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)} (m : pure a ∈ l),
    (corec parallel.aux1 (l, S)).Terminates
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
have apply₁ : ∀ (s : Computation α),
  (∀ {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
Tactic: apply @terminatesRecOn _ _ c T _ _
-- 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
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
have a₁ : ∃ (a : α), parallel.aux2 l = Sum.inl a
Tactic: apply lem1
-- 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
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ ∃ (a : α), parallel.aux2 l = Sum.inl a
have a₁ : ∀ (c : Computation α) (l : List (Computation α)) (IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a)
  (m : pure a ∈ c :: l), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
Tactic: induction l with | nil => simp at m | cons c l IH => ?_
Cleared hypotheses: l, m
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ c :: l
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
have m₁ : pure a = c ∨ pure a ∈ l
Tactic: simp only [List.mem_cons] at m
Cleared hypotheses: m
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : 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
have a₁ : ∀ (e : pure a = c), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
Tactic: rcases m with e | m
Cleared hypotheses: m
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a = c ∨ pure a ∈ l
a₁ : ∀ (e : pure a = c), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
have a₂ : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
Tactic: rcases m with e | m
Cleared hypotheses: m
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
have a₁ : ∃ (a_1 : α), parallel.aux2 (pure a :: l) = Sum.inl a_1
Tactic: rw [← e]
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ (a_1 : α), parallel.aux2 (pure a :: l) = Sum.inl a_1
have a₁ : ∃ (a_1 : α),
  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 => Sum.inl a :
      α ⊕ List (Computation α))
    (Sum.inl a_1 : α ⊕ List (Computation α))
Tactic: simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ (a_1 : α),
    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 => Sum.inl a :
        α ⊕ List (Computation α))
      (Sum.inl a_1 : α ⊕ List (Computation α))
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) →
    ∃ (a_1 : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a) (Sum.inl a_1)
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = 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) →
      ∃ (a_1 : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a) (Sum.inl a_1)
⊢ ∃ (a_1 : α),
    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 => Sum.inl a :
        α ⊕ List (Computation α))
      (Sum.inl a_1 : α ⊕ List (Computation α))
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) →
    ∃ (a_1 : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a) (Sum.inl a_1)
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
have a₁ : ∀ (a' : α) (e : parallel.aux2 l = Sum.inl a'), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
Tactic: obtain ⟨a', e⟩ := IH m
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e : parallel.aux2 l = Sum.inl a'
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
have a₁ : ∃ (a : α),
  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.inl a : α ⊕ List (Computation α))
Tactic: simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
-- 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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ 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')
⊢ ∃ (a : α),
    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.inl a : α ⊕ List (Computation α))
have a₁ : ∃ (a : α),
  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.inl a : α ⊕ List (Computation α))
Tactic: rw [e]
-- 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
l' : List (Computation α)
e' : parallel.aux2 l = Sum.inr l'
⊢ s ∈ l'
have cons : ∀ (c : Computation α) (l : List (Computation α))
  (IH' : ∀ (m : s.think ∈ l) (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l')
  (m : s.think ∈ c :: l) (l' : List (Computation α)) (e' : parallel.aux2 (c :: l) = Sum.inr l'), s ∈ l'
Tactic: induction l generalizing l' with | nil => simp at m | cons c l IH' => ?_
Cleared hypotheses: l, m, l', 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'
m : s.think ∈ c :: l
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
⊢ s ∈ l'
have m₁ : s.think = c ∨ s.think ∈ l
Tactic: simp only [List.mem_cons] at m
Cleared hypotheses: m
-- 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' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think = c ∨ s.think ∈ l
⊢ s ∈ l'
have cons : ∀ (e : s.think = c), s ∈ l'
Tactic: rcases m with e | m
Cleared hypotheses: m
-- 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' : parallel.aux2 (c :: l) = Sum.inr l'
m : s.think = c ∨ s.think ∈ l
cons : ∀ (e : s.think = c), s ∈ l'
⊢ s ∈ l'
have cons₁ : ∀ (m : s.think ∈ l), s ∈ l'
Tactic: rcases m with e | m
Cleared hypotheses: m
-- 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 α))
e : s.think = c
⊢ s ∈ l'
have 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 α))
Tactic: rw [← e] at e'
Cleared hypotheses: e', e
-- 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 α)) s.think.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      α ⊕ List (Computation α))
    (Sum.inr l' : α ⊕ List (Computation α))
e : s.think = c
⊢ s ∈ l'
have cons : ∀
  (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'
Tactic: revert e'
Cleared hypotheses: e'