awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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
dc : d = c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have ad₁ : a ∈ c
Tactic: rw [dc] at ad
Cleared hypotheses: ad, dc
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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 ∈ c
dc : d = c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : c ∈ S
Tactic: refine ⟨c, Or.inr ?_, ad⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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 ∈ c
dc : d = c
⊢ c ∈ S
have h2 : c ∈ Seq.cons (some c) S'
Tactic: rw [Seq.destruct_eq_cons e]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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
have h2 : d ∈ S
Tactic: refine ⟨d, Or.inr ?_, ad⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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 ∈ S
have h2 : d ∈ Seq.cons (some c) S'
Tactic: rw [Seq.destruct_eq_cons e]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
⊢ map f (parallel S) = parallel (WSeq.map (map f) S)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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))
have 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)
Tactic: simp only [parallel.aux2, rmap, lmap]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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 α)
⊢ 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)
have nil : 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: 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
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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 α)
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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))
⊢ 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
have 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
Tactic: simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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))
l' : List (Computation α)
⊢ ∃ (l : List (Computation α)) (S_2 : WSeq (Computation α)),
    map f
          (corec parallel.aux1
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              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_2)) ∧
      corec parallel.aux1
          (match (motive := Option (Seq1 (Option (Computation β))) → List (Computation β) × WSeq (Computation β))
            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_2)
have inr : ∃ (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: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
h : S.head ~> none
h_1 : (parallel S).Terminates
a : α
m : a ∈ parallel S
⊢ False
have let : ∀ (c : Computation α) (cs : c ∈ S), a ∈ c → False
Tactic: let ⟨c, cs, _⟩ := exists_of_mem_parallel m
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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
⊢ False
have let : ∀ (n : ℕ) (nm : some c ∈ S.get? n), False
Tactic: let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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
⊢ False
have let : ∀ (c' : Computation α) (h' : some c' ∈ S.head), False
Tactic: let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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
have rw : S =
  WSeq.map
    (Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
      fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c)
    S
Tactic: rw [← WSeq.map_comp]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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
have 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)
Tactic: refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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
⊢ 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)
have 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
Tactic: funext c
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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 α
⊢ id c =
    Function.comp (β := Computation (α × Computation α)) (map fun (c : α × Computation α) ↦ c.1)
      (fun (c : Computation α) ↦ map (fun (a : α) ↦ (a, c)) c) c
have h₁ : c = map (fun (c : α × Computation α) ↦ c.1) (map (fun (a : α) ↦ (a, c)) c)
Tactic: dsimp [id, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
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) (map (fun (a : α) ↦ (a, c)) c)
have h₁ : c = map ((fun (c : α × Computation α) ↦ c.1) ∘ fun (a : α) ↦ (a, c)) c
Tactic: rw [← map_comp]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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 a
have this : 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
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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
⊢ C a
have pe : parallel S = parallel (WSeq.map (map fun (c : α × Computation α) ↦ c.1) T)
Tactic: have pe := congr_arg parallel this
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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)
⊢ C a
have pe₁ : parallel S = map (fun (c : α × Computation α) ↦ c.1) (parallel T)
Tactic: rw [← map_parallel] at pe
Cleared hypotheses: pe
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
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
⊢ C a
have h'₁ : Membership.mem (γ := Computation α) (map (fun (c : α × Computation α) ↦ c.1) (parallel T)) a
Tactic: rw [pe] at h'
Cleared hypotheses: h'