awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have this : F l (parallel.aux2 l)
Tactic: have := lem1 l
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
this : F l (parallel.aux2 l)
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have e'₁ : Eq (α := α ⊕ Computation α)
  (rmap (corec parallel.aux1)
    (rmap
      (fun (l' : List (Computation α)) ↦
        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'))
      (parallel.aux2 l)))
  (Sum.inl a)
Tactic: simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
this : F l (parallel.aux2 l)
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have e'₁ : rmap (corec parallel.aux1)
    (rmap
      (fun (l' : List (Computation α)) ↦
        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'))
      (parallel.aux2 l)) =
  Sum.inr C'
Tactic: simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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
this : F l (parallel.aux2 l)
e' :
  Eq (α := α ⊕ Computation α)
    (rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          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'))
        (parallel.aux2 l)))
    (Sum.inl a)
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h1 : ∀ (this : F l (parallel.aux2 l))
  (e' :
    Eq (α := α ⊕ Computation α)
      (rmap (corec parallel.aux1)
        (rmap
          (fun (l' : List (Computation α)) ↦
            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'))
          (parallel.aux2 l)))
      (Sum.inl a)),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: revert this e'
Cleared hypotheses: this, e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
this : F l (parallel.aux2 l)
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          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'))
        (parallel.aux2 l)) =
    Sum.inr C'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (this : F l (parallel.aux2 l))
  (e' :
    rmap (corec parallel.aux1)
        (rmap
          (fun (l' : List (Computation α)) ↦
            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'))
          (parallel.aux2 l)) =
      Sum.inr C'),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: revert this e'
Cleared hypotheses: this, e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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
⊢ ∀ (this : F l (parallel.aux2 l))
    (e' :
      Eq (α := α ⊕ Computation α)
        (rmap (corec parallel.aux1)
          (rmap
            (fun (l' : List (Computation α)) ↦
              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'))
            (parallel.aux2 l)))
        (Sum.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h1 : ∀ (a' : α) (this : F l (Sum.inl a'))
  (e' :
    Eq (α := α ⊕ Computation α)
      (rmap (corec parallel.aux1)
        (rmap
          (fun (l' : List (Computation α)) ↦
            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'))
          (Sum.inl a')))
      (Sum.inl a)),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases parallel.aux2 l with a' | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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
h1 :
  ∀ (a' : α) (this : F l (Sum.inl a'))
    (e' :
      Eq (α := α ⊕ Computation α)
        (rmap (corec parallel.aux1)
          (rmap
            (fun (l' : List (Computation α)) ↦
              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'))
            (Sum.inl a')))
        (Sum.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (this : F l (parallel.aux2 l))
    (e' :
      Eq (α := α ⊕ Computation α)
        (rmap (corec parallel.aux1)
          (rmap
            (fun (l' : List (Computation α)) ↦
              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'))
            (parallel.aux2 l)))
        (Sum.inl a)),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h1₁ : ∀ (l' : List (Computation α)) (this : F l (Sum.inr l'))
  (e' :
    Eq (α := α ⊕ Computation α)
      (rmap (corec parallel.aux1)
        (rmap
          (fun (l' : List (Computation α)) ↦
            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'))
          (Sum.inr l')))
      (Sum.inl a)),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases parallel.aux2 l with a' | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
⊢ ∀ (this : F l (parallel.aux2 l))
    (e' :
      rmap (corec parallel.aux1)
          (rmap
            (fun (l' : List (Computation α)) ↦
              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'))
            (parallel.aux2 l)) =
        Sum.inr C'),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (a' : α) (this : F l (Sum.inl a'))
  (e' :
    rmap (corec parallel.aux1)
        (rmap
          (fun (l' : List (Computation α)) ↦
            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'))
          (Sum.inl a')) =
      Sum.inr C'),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases parallel.aux2 l with a' | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
h2 :
  ∀ (a' : α) (this : F l (Sum.inl a'))
    (e' :
      rmap (corec parallel.aux1)
          (rmap
            (fun (l' : List (Computation α)) ↦
              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'))
            (Sum.inl a')) =
        Sum.inr C'),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (this : F l (parallel.aux2 l))
    (e' :
      rmap (corec parallel.aux1)
          (rmap
            (fun (l' : List (Computation α)) ↦
              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'))
            (parallel.aux2 l)) =
        Sum.inr C'),
    ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2₁ : ∀ (l' : List (Computation α)) (this : F l (Sum.inr l'))
  (e' :
    Eq (α := α ⊕ Computation α)
      (rmap (corec parallel.aux1)
        (rmap
          (fun (l' : List (Computation α)) ↦
            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'))
          (Sum.inr l')))
      (Sum.inr C')),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases parallel.aux2 l with a' | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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')
e' :
  Eq (α := α ⊕ Computation α)
    (rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          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'))
        (Sum.inl a')))
    (Sum.inl a)
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h' : a' = a
Tactic: injection e' with h'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (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')
e' :
  Eq (α := α ⊕ Computation α)
    (rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          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'))
        (Sum.inr l')))
    (Sum.inr C')
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h' : corec parallel.aux1
    ((fun (l' : List (Computation α)) ↦
        (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') :
          List (Computation α) × WSeq (Computation α)))
      l') =
  C'
Tactic: injection e' with h'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 α)),
    corec parallel.aux1 (l, S) = C → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h1 : ∀ (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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l <;> simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e' <;>
    revert this e' <;> rcases parallel.aux2 l with a' | l' <;> intro this e' <;>
    [injection e' with h'; injection e'; injection e'; injection e' with h']
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
h1 :
  ∀ (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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (C' : Computation α)
  (IH :
    ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (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'))
  (h' :
    corec parallel.aux1
        ((fun (l' : List (Computation α)) ↦
            (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') :
              List (Computation α) × WSeq (Computation α)))
          l') =
      C'),
  ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: apply memRecOn aC <;> [skip; intro C' IH] <;> intro l S e <;> have e' := congr_arg destruct e <;>
    have := lem1 l <;> simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e' <;>
    revert this e' <;> rcases parallel.aux2 l with a' | l' <;> intro this e' <;>
    [injection e' with h'; injection e'; injection e'; injection e' with h']
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have this₁ : F l (Sum.inl a)
Tactic: rw [h'] at this
Cleared hypotheses: this, h'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a : α
h : a ∈ parallel S_1
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun (l : List (Computation α)) (a : α ⊕ List (Computation α)) ↦
    Sum.casesOn (motive := fun (x : α ⊕ List (Computation α)) ↦ Prop) a (fun (a : α) ↦ ∃ c ∈ l, a ∈ c)
      fun (l' : List (Computation α)) ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ 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 : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h1 : ∀ (c : Computation α) (cl : c ∈ l) (ac : a ∈ c), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases this with ⟨c, cl, ac⟩
Cleared hypotheses: this