awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
c : Computation α
l : List (Computation α)
⊢ ∀
    (IH :
      F l
        (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)),
    F (c :: l)
      (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
have inl : ∀ (val : α) (IH : F l (Sum.inl val)),
  F (c :: l)
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl val with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
Tactic: cases 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
-- 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
c : Computation α
l : List (Computation α)
inl :
  ∀ (val : α) (IH : F l (Sum.inl val)),
    F (c :: l)
      (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inl val with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
⊢ ∀
    (IH :
      F l
        (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)),
    F (c :: l)
      (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 => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
have inr : ∀ (val : List (Computation α)) (IH : F l (Sum.inr val)),
  F (c :: l)
    (match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) Sum.inr val with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun (c' : Computation α) ↦ c' :: ls) c.destruct)
Tactic: cases 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
-- 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
c : Computation α
l : List (Computation α)
val : α
IH : F l (Sum.inl val)
⊢ F (c :: l) (Sum.inl val)
have inl : ∀ (c' : Computation α) (cl : c' ∈ l) (ac : val ∈ c'), F (c :: l) (Sum.inl val)
Tactic: rcases IH with ⟨c', cl, ac⟩
Cleared hypotheses: IH
-- 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) c.destruct)
have inr : ∀ (a : α) (h : c.destruct = Sum.inl a), F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inl a))
Tactic: rcases h : destruct c with a | c'
-- 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
inr : ∀ (a : α) (h : c.destruct = Sum.inl a), F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inl a))
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) c.destruct)
have inr₁ : ∀ (c' : Computation α) (h : c.destruct = Sum.inr c'),
  F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inr c'))
Tactic: rcases h : destruct c with a | c'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inl a))
have inr : F (c :: l) (Sum.inl a)
Tactic: simp only [rmap]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (rmap (fun (c' : Computation α) ↦ c' :: val) (Sum.inr c'))
have inr : F (c :: l) (Sum.inr (c' :: val))
Tactic: simp only [rmap]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (Sum.inl a)
have inr : a ∈ c
Tactic: refine ⟨c, List.mem_cons_self, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a_1 : α
h_1 : a_1 ∈ 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
a : α
h : c.destruct = Sum.inl a
⊢ a ∈ c
have inr : a ∈ pure a
Tactic: rw [destruct_eq_pure h]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h_2 : c.destruct = Sum.inr c'
a' : α
h : ∃ c ∈ c' :: val, a' ∈ c
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have inr : ∀ (d : Computation α) (dm : d ∈ c' :: val) (ad : a' ∈ d), ∃ c_1 ∈ c :: l, a' ∈ c_1
Tactic: rcases h with ⟨d, dm, ad⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have inr : ∀ (e : d = c'), ∃ c_1 ∈ c :: l, a' ∈ c_1
Tactic: rcases List.mem_cons.mp dm with e | dl
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
inr : ∀ (e : d = c'), ∃ c_1 ∈ c :: l, a' ∈ c_1
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have inr₁ : ∀ (dl : d ∈ val), ∃ c_1 ∈ c :: l, a' ∈ c_1
Tactic: rcases List.mem_cons.mp dm with e | dl
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have ad₁ : a' ∈ c'
Tactic: rw [e] at ad
Cleared hypotheses: ad, e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have inr : a' ∈ c
Tactic: refine ⟨c, List.mem_cons_self, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c
have inr : a' ∈ c'.think
Tactic: rw [destruct_eq_think h]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val
ad : a' ∈ d
dl : d ∈ val
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have inr : ∀ (d : Computation α) (dm : d ∈ l ∧ a' ∈ d), ∃ c_1 ∈ c :: l, a' ∈ c_1
Tactic: obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d_1 : Computation α
dm_1 : d_1 ∈ c' :: val
ad : a' ∈ d_1
dl : d_1 ∈ val
d : Computation α
dm : d ∈ l ∧ a' ∈ d
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have dm₁ : d ∈ l
Tactic: obtain ⟨dm, ad⟩ := dm
Cleared hypotheses: dm
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S : WSeq (Computation α)
a : α
h_1 : 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
c : Computation α
l val : List (Computation α)
IH : F l (Sum.inr val)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d_1 : Computation α
dm_1 : d_1 ∈ c' :: val
ad : a' ∈ d_1
dl : d_1 ∈ val
d : Computation α
dm : d ∈ l ∧ a' ∈ d
dm₁ : d ∈ l
⊢ ∃ c_1 ∈ c :: l, a' ∈ c_1
have ad₁ : a' ∈ d
Tactic: obtain ⟨dm, ad⟩ := dm
Cleared hypotheses: dm
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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
⊢ ∀ (C : Computation α),
    a ∈ C →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = C → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
Tactic: have lem1 (l) : F l (parallel.aux2 l) := by
    induction l <;> simp only [parallel.aux2, List.foldr]
    case nil =>
      intro a h
      assumption
    case cons c l IH =>
      simp only [parallel.aux2] at IH
      -- Porting note: `revert IH` & `intro IH` are required.
      revert IH
      cases 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 <;>
        intro IH <;> simp only
      · rcases IH with ⟨c', cl, ac⟩
        exact ⟨c', List.Mem.tail _ cl, ac⟩
      · rcases h : destruct c with a | c' <;> simp only [rmap]
        · refine ⟨c, List.mem_cons_self, ?_⟩
          rw [destruct_eq_pure h]
          apply ret_mem
        · intro a' h
          rcases h with ⟨d, dm, ad⟩
          rcases List.mem_cons.mp dm with e | dl
          · rw [e] at ad
            refine ⟨c, List.mem_cons_self, ?_⟩
            rw [destruct_eq_think h]
            exact think_mem ad
          · obtain ⟨d, dm⟩ := IH a' ⟨d, dl, ad⟩
            obtain ⟨dm, ad⟩ := dm
            exact ⟨d, List.Mem.tail _ dm, ad⟩
-- 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 α)),
  corec parallel.aux1 (l, S) = pure a → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: apply memRecOn aC
-- 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 α)),
    corec parallel.aux1 (l, S) = pure 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 : ∀ (s : Computation α),
  (∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = s → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c) →
    ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
      corec parallel.aux1 (l, S) = s.think → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: apply memRecOn aC
-- 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 α)),
  corec parallel.aux1 (l, S) = pure a → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: apply memRecOn aC <;> [skip; intro C' IH]
-- 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 α)),
    corec parallel.aux1 (l, S) = pure 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 α)),
  corec parallel.aux1 (l, S) = C'.think → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: apply memRecOn aC <;> [skip; intro C' IH]
-- 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
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
Tactic: have e' := congr_arg destruct 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
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
Tactic: have e' := congr_arg destruct 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
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have this : F l (parallel.aux2 l)
Tactic: have := lem1 l