α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a' ∈ parallel T
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel S
⊢ a' ∈ parallel T
have aa := parallel_promises h1 h
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a' ∈ parallel T
rw [← aa]
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
rw [← aa] at h
no goals
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T
exact
  let ⟨s, sS, as⟩ := exists_of_mem_parallel h
  let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_left H sS
  let aT := (st _).1 as
  mem_parallel h2 tT aT
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel T
⊢ a' ∈ parallel S
have aa := parallel_promises h2 h
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S
rw [← aa]
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
rw [← aa] at h
no goals
α : Type u
β : Type v
S T : WSeq (Computation α)
a : α
h1 : ∀ (s : Computation α), s ∈ S → s ~> a
H : WSeq.LiftRel Equiv S T
h2 : ∀ (t : Computation α), t ∈ T → t ~> a := Iff.mp (parallel_congr_lem H) h1
a' : α
h : a ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S
exact
  let ⟨s, sS, as⟩ := exists_of_mem_parallel h
  let ⟨t, tT, st⟩ := WSeq.exists_of_liftRel_right H sS
  let aT := (st _).2 as
  mem_parallel h1 tT aT