Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, 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))
l' : List (Computation α)
⊢ ∃ l S_1,
    map f
          (corec parallel.aux1
            (match Seq.destruct 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_1)) ∧
      corec parallel.aux1
          (match Seq.destruct (WSeq.map (map f) 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_1)

Tactic:
induction S using WSeq.recOn

Goal state after:
case inr.nil
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, 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 S,
    map f
          (corec parallel.aux1
            (match 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 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)

case inr.cons
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, 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 S,
    map f
          (corec parallel.aux1
            (match 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 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)

case inr.think
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, 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 S,
    map f
          (corec parallel.aux1
            (match 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 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)