awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Eq.{u + 1} (α := α ⊕ 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) :
      α ⊕ Computation α)
    (Sum.inr
        (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'))) :
      α ⊕ Computation α)
have rw : Eq.{u + 1} (α := α ⊕ Computation α)
  (match (motive := α ⊕ List (Computation α) × WSeq (Computation α) → α ⊕ Computation α)
      match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α) × WSeq (Computation α)) Sum.inr 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) :
    α ⊕ Computation α)
  (Sum.inr
      (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'))) :
    α ⊕ Computation α)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates
have H2 : corec parallel.aux1 (l, S) =
  think
    (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')))
Tactic: have H2 : corec parallel.aux1 (l, S) = think _ := destruct_eq_think (by
        simp only [parallel.aux1, rmap, corec_eq]
        rw [h])
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : Terminates.{u} (α := α)
  (think
    (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'))))
Tactic: rw [H2]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
⊢ Terminates.{u} (α := α)
    (think
      (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'))))
have inr : Terminates.{u} (α := α)
  (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')))
Tactic: refine @Computation.think_terminates _ _ ?_
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
⊢ Terminates.{u} (α := α)
    (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')))
have this : s ∈ l'
Tactic: have := H1 _ h
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
this : s ∈ l'
⊢ Terminates.{u} (α := α)
    (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')))
have inr : Terminates.{u} (α := α)
  (corec parallel.aux1
    (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α)) none with
    | none => (l', Seq.nil)
    | some (none, S') => (l', S')
    | some (some c, S') => (c :: l', S')))
Tactic: rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩)
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
this : s ∈ l'
inr :
  Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α)) none with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
⊢ Terminates.{u} (α := α)
    (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')))
have inr₁ : ∀ (S' : Stream'.Seq (Option (Computation α))),
  Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        some (none, S') with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
Tactic: rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩)
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
this : s ∈ l'
inr :
  Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α)) none with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
inr₁ :
  ∀ (S' : Stream'.Seq (Option (Computation α))),
    Terminates.{u} (α := α)
      (corec parallel.aux1
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          some (none, S') with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates.{u} (α := α)
    (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')))
have inr₂ : ∀ (S' : Stream'.Seq (Option (Computation α))) (c : Computation α),
  Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        some (some c, S') with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
Tactic: rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩)
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c_1 : Computation α
T : c_1.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : s ∈ l), (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)) (e' : parallel.aux2 l = Sum.inr l'), s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (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')))
this : s ∈ l'
S' : Stream'.Seq (Option (Computation α))
c : Computation α
⊢ Terminates.{u} (α := α)
    (corec parallel.aux1
      (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
        some (some c, S') with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
have inr : s ∈ c :: l'
Tactic: apply IH
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
⊢ (parallel S).Terminates
have List : ∀ (n : ℕ) (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
  c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
Tactic: suffices
    ∀ (n) (l : List (Computation α)) (S c),
      c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
    from
    let ⟨n, h⟩ := h
    this n [] S c (Or.inr h) T
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
n : ℕ
⊢ ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
have zero : ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
  c ∈ l ∨ some (some c) = S.get? 0 → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
n : ℕ
zero :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? 0 → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
⊢ ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
have succ : ∀ (n : ℕ),
  (∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
      c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates) →
    ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
      c ∈ l ∨ some (some c) = S.get? (n + 1) → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inl : ∀ (a : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases o with a | a
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = S.get? 0
T : c.Terminates
inl : ∀ (a : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : ∀ (a : some (some c) = S.get? 0), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases o with a | a
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
⊢ (corec parallel.aux1 (l, S)).Terminates
have H : S.destruct = some (some c, S.tail)
Tactic: have H : Seq.destruct S = some (some c, Seq.tail S) := by simp [Seq.destruct, (· <$> ·), ← a]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases h : parallel.aux2 l with a | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
inr : ∀ (a : α) (h : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr₁ : ∀ (l' : List (Computation α)) (h : parallel.aux2 l = Sum.inr l'), (corec parallel.aux1 (l, S)).Terminates
Tactic: rcases h : parallel.aux2 l with a | l'
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = pure a
have a₁ : (corec parallel.aux1 (l, S)).destruct = Sum.inl a
Tactic: apply destruct_eq_pure
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inl a
have a₁ : Eq (α := α ⊕ Computation α)
  (rmap (corec parallel.aux1)
    (rmap
      (fun (l' : List (Computation α)) ↦
        match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))
      (parallel.aux2 l)))
  (Sum.inl a)
Tactic: rw [corec_eq, parallel.aux1]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Eq (α := α ⊕ Computation α)
    (rmap (corec parallel.aux1)
      (rmap
        (fun (l' : List (Computation α)) ↦
          match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            S.destruct with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)))
    (Sum.inl a)
have a₁ : Eq (α := α ⊕ Computation α)
  (rmap (corec parallel.aux1)
    (rmap
      (fun (l' : List (Computation α)) ↦
        match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
          S.destruct with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))
      (Sum.inl a)))
  (Sum.inl a)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
have C : corec parallel.aux1 (l, S) = pure a
Tactic: have C : corec parallel.aux1 (l, S) = pure a := by
        apply destruct_eq_pure
        rw [corec_eq, parallel.aux1]
        rw [h]
        simp only [rmap]
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
c_1 : Computation α
h_1 : c_1 ∈ S_1
T_1 : c_1.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a_1 : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ (corec parallel.aux1 (l, S)).Terminates
have inr : (pure a).Terminates
Tactic: rw [C]