-- Mathlib/Data/Seq/Parallel.lean
theorem parallel_congr_left {S T : WSeq (Computation α)} {a} (h1 : ∀ s ∈ S, s ~> a)
    (H : S.LiftRel Equiv T) : parallel S ~ parallel T :=
  let h2 := (parallel_congr_lem H).1 h1
  fun a' =>
  ⟨fun h => by
    have aa := parallel_promises h1 h
    rw [← aa]
    rw [← aa] at h
    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,
    fun h => by
    have aa := parallel_promises h2 h
    rw [← aa]
    rw [← aa] at h
    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⟩

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
⊢ a' ∈ parallel T

Tactic:
have aa := parallel_promises h1 h

Result:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a' ∈ parallel T

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S

Tactic:
rw [← aa] at h

Result:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T

Tactic:
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

Result:
no goals

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
⊢ a' ∈ parallel S

Tactic:
have aa := parallel_promises h2 h

Result:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T

Tactic:
rw [← aa] at h

Result:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S

Tactic:
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

Result:
no goals

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a' ∈ parallel S

Tactic:
rw [← aa]

Result:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel T
aa : a = a'
⊢ a ∈ parallel S

Proof state:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a' ∈ parallel T

Tactic:
rw [← aa]

Result:
α : Type u
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 := (parallel_congr_lem H).mp h1
a' : α
h : a' ∈ parallel S
aa : a = a'
⊢ a ∈ parallel T