awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
⊢ S =
    WSeq.map
      (Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
        fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c)
      S

Tactic:
(WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)

Premises used: congr_arg, Stream'.WSeq.map, Stream'.WSeq.map_id, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
refine :
  Eq.{u + 1} (α := Computation α → Computation α) id
    (Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
      fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c)
⊢ S =
    WSeq.map
      (Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
        fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c)
      S

Tactic:
refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)

Premises used: congr_arg, Stream'.WSeq.map, Stream'.WSeq.map_id, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
h₁ :
  ∀ (c : Computation α),
    id c =
      Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
        (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) c
⊢ Eq.{u + 1} (α := Computation α → Computation α) id
    (Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
      fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c)

Tactic:
funext c
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
c : Computation α
h₁ : c = map (fun (c : α × Computation α) ↦ c.1) (map (fun (a : α) ↦ (a, c)) c)
⊢ id c =
    Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
      (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) c

Tactic:
dsimp [id, Function.comp_def]

Premises used: id, Function.comp_def
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
c : Computation α
h₁ : c = map ((fun (c : α × Computation α) ↦ c.1) ∘ fun (a : α) ↦ (a, c)) c
⊢ c = map (fun (c : α × Computation α) ↦ c.1) (map (fun (a : α) ↦ (a, c)) c)

Tactic:
rw [← map_comp]

Premises used: Computation.map_comp
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
c : Computation α
⊢ c = map ((fun (c : α × Computation α) ↦ c.1) ∘ fun (a : α) ↦ (a, c)) c

Tactic:
(map_id _).symm

Premises used: Computation.map_id, Eq.symm
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
c : Computation α
⊢ c = map ((fun (c : α × Computation α) ↦ c.1) ∘ fun (a : α) ↦ (a, c)) c

Tactic:
exact (map_id _).symm

Premises used: Computation.map_id, Eq.symm
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
⊢ S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T

Tactic:
have : S = T.map (map fun c => c.1) := by
    rw [← WSeq.map_comp]
    refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)
    funext c
    dsimp [id, Function.comp_def]
    rw [← map_comp]
    exact (map_id _).symm
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
⊢ parallel S = parallel (WSeq.map (map fun (c : α × Computation α) ↦ c.1) T)

Tactic:
have pe := congr_arg parallel this
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = parallel (WSeq.map (map fun (c : α × Computation α) ↦ c.1) T)
⊢ parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)

Tactic:
rw [← map_parallel] at pe

Premises used: Computation.map_parallel
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
⊢ a ∈ parallel S

Tactic:
have h' := h
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : a ∈ parallel S
⊢ Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a

Tactic:
rw [pe] at h'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
⊢ (parallel T).Terminates

Tactic:
haveI : Terminates (parallel T) := (terminates_map_iff _ _).1 ⟨⟨_, h'⟩⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
rcases : (a' : α) → (c : Computation α) → (e : (parallel T).get = (a', c)) → C a
⊢ C a

Tactic:
rcases e : get (parallel T) with ⟨a', c⟩

Premises used: Computation.parallel, Computation.get
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
rcases : ∀ (d : α × Computation α) (dT : d ∈ parallel T) (cd : d.1 = a), a ∈ c ∧ c ∈ S
⊢ a ∈ c ∧ c ∈ S

Tactic:
rcases exists_of_mem_map h' with ⟨d, dT, cd⟩

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
d : α × Computation α
dT : d ∈ parallel T
cd : d.1 = a
⊢ d = (a', c)

Tactic:
rw [get_eq_of_mem _ dT] at e

Premises used: Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
d : α × Computation α
dT : d ∈ parallel T
cd : d.1 = a
e₁ : d = (a', c)
⊢ d ∈ parallel T

Tactic:
rw [get_eq_of_mem _ dT] at e

Premises used: Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
e : (parallel T).get = (a', c)
d : α × Computation α
dT : d ∈ parallel T
cd : d.1 = a
e₁ : d = (a', c)
dT₁ : d ∈ parallel T
⊢ d.1 = a

Tactic:
rw [get_eq_of_mem _ dT] at e

Premises used: Computation.get_eq_of_mem
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
d : α × Computation α
e : d = (a', c)
dT : d ∈ parallel T
cd : d.1 = a
⊢ (a', c) ∈ parallel T

Tactic:
cases e
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
d : α × Computation α
e : d = (a', c)
dT : d ∈ parallel T
cd : d.1 = a
dT₁ : (a', c) ∈ parallel T
⊢ (a', c).1 = a

Tactic:
cases e
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
a' : α
c : Computation α
dT : (a', c) ∈ parallel T
cd : a' = a
⊢ (a, c) ∈ parallel T

Tactic:
cases cd
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
refl : ∀ (d' : Computation (α × Computation α)) (dT' : d' ∈ T) (ad' : (a, c) ∈ d'), a ∈ c ∧ c ∈ S
⊢ a ∈ c ∧ c ∈ S

Tactic:
rcases exists_of_mem_parallel dT with ⟨d', dT', ad'⟩

Premises used: Computation.exists_of_mem_parallel
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
refl : ∀ (c' : Computation α) (cs' : c' ∈ S) (e' : map (fun (a : α) ↦ (a, c')) c' = d'), a ∈ c ∧ c ∈ S
⊢ a ∈ c ∧ c ∈ S

Tactic:
rcases WSeq.exists_of_mem_map dT' with ⟨c', cs', e'⟩

Premises used: Stream'.WSeq.exists_of_mem_map
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
c' : Computation α
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
⊢ Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)

Tactic:
rw [← e'] at ad'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
c' : Computation α
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
ad'₁ : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
⊢ c' ∈ S

Tactic:
rw [← e'] at ad'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
ad' : (a, c) ∈ d'
c' : Computation α
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
ad'₁ : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs'₁ : c' ∈ S
⊢ map (fun (a : α) ↦ (a, c')) c' = d'

Tactic:
rw [← e'] at ad'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
refl : ∀ (a' : α) (ac' : a' ∈ c') (e' : (a', c') = (a, c)), a ∈ c ∧ c ∈ S
⊢ a ∈ c ∧ c ∈ S

Tactic:
rcases exists_of_mem_map ad' with ⟨a', ac', e'⟩

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e'_1 : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
e' : (a', c') = (a, c)
⊢ a' = a

Tactic:
injection e' with i1 i2
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e'_1 : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
e' : (a', c') = (a, c)
i1 : a' = a
⊢ c' = c

Tactic:
injection e' with i1 i2
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
refl : a ∈ c
refl₁ : c ∈ S
⊢ a ∈ c ∧ c ∈ S

Tactic:
constructor
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
refl : ∀ (ac' : a ∈ c') (i1 : a' = a) (i2 : c' = c), a ∈ c
refl₁ refl₂ refl₃ refl₄ : ∀ (ac' : a ∈ c) (i1 : a' = a) (i2 : c' = c), a ∈ c
⊢ a ∈ c

Tactic:
rwa [i1, i2] at ac'
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) S
this_1 : S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T
pe : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
h' : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
this : (parallel T).Terminates
c : Computation α
dT : (a, c) ∈ parallel T
d' : Computation (α × Computation α)
dT' : d' ∈ T
c' : Computation α
ad' : Membership.mem (γ := Computation (α × Computation α)) (map (fun (a : α) ↦ (a, c')) c') (a, c)
cs' : c' ∈ S
e' : map (fun (a : α) ↦ (a, c')) c' = d'
a' : α
ac' : a' ∈ c'
i1 : a' = a
i2 : c' = c
refl refl₁ refl₂ refl₃ :
  ∀ (cs' : c ∈ S) (e' : map (fun (a : α) ↦ (a, c')) c' = d') (a' : α) (ac' : a' ∈ c') (i1 : a' = a) (i2 : c' = c), c ∈ S
⊢ c ∈ S

Tactic:
rwa [i2] at cs'