awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Parallel
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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
⟨d, Or.inr ?_, ad⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.Seq.Parallel
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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
h2 : d ∈ S
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
refine ⟨d, Or.inr ?_, ad⟩
-- Module: Mathlib.Data.Seq.Parallel
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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
h2 : d ∈ Seq.cons (some c) S'
⊢ d ∈ S

Tactic:
rw [Seq.destruct_eq_cons e]

Premises used: Stream'.Seq.destruct_eq_cons
-- Module: Mathlib.Data.Seq.Parallel
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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ d ∈ Seq.cons (some c) S'

Tactic:
Seq.mem_cons_of_mem _ dS'

Premises used: Stream'.Seq.mem_cons_of_mem, Stream'.WSeq.Mem
-- Module: Mathlib.Data.Seq.Parallel
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_1 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
S' : Stream'.Seq (Option (Computation α))
c : Computation α
h' : corec parallel.aux1 (c :: l', S') = C'
e : Seq.destruct S = some (some c, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ d ∈ Seq.cons (some c) S'

Tactic:
exact Seq.mem_cons_of_mem _ dS'

Premises used: Stream'.Seq.mem_cons_of_mem
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ map f (parallel S) = parallel (WSeq.map (map f) S)

Tactic:
eq_of_bisim
      (fun c1 c2 =>
        ∃ l S,
          c1 = map f (corec parallel.aux1 (l, S)) ∧
            c2 = corec parallel.aux1 (l.map (map f), S.map (map f)))
      ?_ ⟨[], S, rfl, rfl⟩

Premises used: Computation.corec, List.map, Exists, _private.0.Computation.parallel.aux1, Prod.mk, And, Computation.map, And.intro, Stream'.WSeq.map, Exists.intro, Computation.eq_of_bisim, Eq, rfl, List.nil
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 :
  IsBisimulation.{v} (α := β) fun (c1 c2 : Computation β) ↦
    ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
      c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
⊢ map f (parallel S) = parallel (WSeq.map (map f) S)

Tactic:
refine
    eq_of_bisim
      (fun c1 c2 =>
        ∃ l S,
          c1 = map f (corec parallel.aux1 (l, S)) ∧
            c2 = corec parallel.aux1 (l.map (map f), S.map (map f)))
      ?_ ⟨[], S, rfl, rfl⟩

Premises used: Computation.corec, List.map, Exists, _private.0.Computation.parallel.aux1, Prod.mk, And, Computation.map, And.intro, Stream'.WSeq.map, Exists.intro, Computation.eq_of_bisim, Eq, rfl, List.nil
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
simp :
  Eq (α := β ⊕ 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 =>
          match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) l))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b)
⊢ parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))

Tactic:
simp only [parallel.aux2, rmap, lmap]

Premises used: Computation.rmap, Computation.lmap, _private.0.Computation.parallel.aux2
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
S : WSeq (Computation α)
⊢ Eq (α := β ⊕ 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 =>
          match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) []))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (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 =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) [] with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
⊢ parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))

Tactic:
have : parallel.aux2 (l.map (map f))
          = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) := by
        simp only [parallel.aux2, rmap, lmap]
        induction l with
        | nil => simp
        | cons c l IH =>
          simp only [List.map_cons, List.foldr_cons, destruct_map, lmap, rmap]
          rw [IH]
          cases List.foldr _ _ _
          · simp
          · cases destruct c <;> simp
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
simp :
  match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
      match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β))
        match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
          match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α))
            parallel.aux2 l with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match (motive := β ⊕ List (Computation β) × WSeq (Computation β) → β ⊕ Computation β)
      match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β) × WSeq (Computation β))
        parallel.aux2 (List.map (map f) l) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
      s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False
⊢ BisimO
    (fun (c1 c2 : Computation β) ↦
      ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    (map f (corec parallel.aux1 (l, S))).destruct
    (corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)).destruct

Tactic:
simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]

Premises used: Computation.rmap, Computation.destruct_map, Computation.lmap, Computation.corec_eq, _private.0.Computation.parallel.aux1.eq_1, Computation.BisimO
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
a : α
⊢ match (motive := β ⊕ Computation β → β ⊕ Computation β → Prop)
    match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
      match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β))
        match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
          match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) Sum.inl a with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                Seq.destruct S with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (map f b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b,
    match (motive := β ⊕ List (Computation β) × WSeq (Computation β) → β ⊕ Computation β)
      match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β) × WSeq (Computation β))
        lmap f (rmap (List.map (map f)) (Sum.inl a)) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) S) with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' =>
    ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
      s = map f (corec parallel.aux1 (l, S)) ∧ s' = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
l' : List (Computation α)
⊢ ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct WSeq.nil with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))) =
        map f (corec parallel.aux1 (l, S)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) WSeq.nil) with
          | none => (List.map (map f) l', Seq.nil)
          | some (none, S') => (List.map (map f) l', S')
          | some (some c, S') => (c :: List.map (map f) l', S')) =
        corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)

Tactic:
simpa using ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
l' : List (Computation α)
x : Computation α
s : WSeq (Computation α)
⊢ ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct (WSeq.cons x s) with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))) =
        map f (corec parallel.aux1 (l, S)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) (WSeq.cons x s)) with
          | none => (List.map (map f) l', Seq.nil)
          | some (none, S') => (List.map (map f) l', S')
          | some (some c, S') => (c :: List.map (map f) l', S')) =
        corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)

Tactic:
simpa using ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
l' : List (Computation α)
s : WSeq (Computation α)
⊢ ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              Seq.destruct s.think with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))) =
        map f (corec parallel.aux1 (l, S)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            Seq.destruct (WSeq.map (map f) s.think) with
          | none => (List.map (map f) l', Seq.nil)
          | some (none, S') => (List.map (map f) l', S')
          | some (some c, S') => (c :: List.map (map f) l', S')) =
        corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)

Tactic:
simpa using ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
⊢ BisimO
    (fun (c1 c2 : Computation β) ↦
      ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    c1.destruct c2.destruct

Tactic:
exact
    match c1, c2, h with
    | _, _, ⟨l, S, rfl, rfl⟩ => by
      have : parallel.aux2 (l.map (map f))
          = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) := by
        simp only [parallel.aux2, rmap, lmap]
        induction l with
        | nil => simp
        | cons c l IH =>
          simp only [List.map_cons, List.foldr_cons, destruct_map, lmap, rmap]
          rw [IH]
          cases List.foldr _ _ _
          · simp
          · cases destruct c <;> simp
      simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]
      rw [this]
      rcases parallel.aux2 l with a | l'
      · simp
      simp only [lmap, rmap]
      induction S using WSeq.recOn <;> simpa using ⟨_, _, rfl, rfl⟩
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
h_1 : (parallel S).Terminates
a : α
m : a ∈ parallel S
let : ∀ (c : Computation α) (cs : c ∈ S), a ∈ c → False
⊢ False

Tactic:
let ⟨c, cs, _⟩ := exists_of_mem_parallel m
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
h_1 : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right : a ∈ c
let : ∀ (n : ℕ) (nm : some c ∈ S.get? n), False
⊢ False

Tactic:
let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
h_1 : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
let : ∀ (c' : Computation α) (h' : some c' ∈ S.head), False
⊢ False

Tactic:
let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
h_1 : (parallel S).Terminates
a : α
m : a ∈ parallel S
c : Computation α
cs : c ∈ S
right : a ∈ c
n : ℕ
nm : some c ∈ S.get? n
c' : Computation α
h' : some c' ∈ S.head
⊢ False

Tactic:
injection 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
let : C a
⊢ C a

Tactic:
let T : WSeq (Computation (α × Computation α)) := S.map fun c => c.map fun a => (a, 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
rw :
  S =
    WSeq.map
      (Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
        fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c)
      S
⊢ S = WSeq.map (map fun (c : α × Computation α) ↦ c.1) T

Tactic:
rw [← WSeq.map_comp]

Premises used: Stream'.WSeq.map_comp