awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (e : Seq.destruct S = none), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases e : Seq.destruct S with - | a
-- 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 : corec parallel.aux1 (l, S) = C'.think
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
h2 : ∀ (e : Seq.destruct S = none), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2₁ : ∀ (a_1 : Seq1 (Option (Computation α))) (e : Seq.destruct S = some a_1), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases e : Seq.destruct S with - | a
-- 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')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = none
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h'₁ : corec parallel.aux1
    ((fun (l' : List (Computation α)) ↦
        (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') :
          List (Computation α) × WSeq (Computation α)))
      l') =
  C'
Tactic: rw [e] at h'
Cleared hypotheses: h', e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (hypothesis)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a_1 : α
h : a_1 ∈ 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_1 ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ 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')
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (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') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
a : Seq1 (Option (Computation α))
e : Seq.destruct S = some a
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
have h'₁ : corec parallel.aux1
    ((fun (l' : List (Computation α)) ↦
        (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
            some a with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S') :
          List (Computation α) × WSeq (Computation α)))
      l') =
  C'
Tactic: rw [e] at h'
Cleared hypotheses: h', e
-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
S_1 : WSeq (Computation α)
a_1 : α
h : a_1 ∈ 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_1 ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ 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')
a : Seq1 (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              some a with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = some a
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
have h2 : ∀ (o : Option (Computation α)) (S' : Stream'.Seq (Option (Computation α)))
  (h' :
    corec parallel.aux1
        ((fun (l' : List (Computation α)) ↦
            (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
                some (o, S') with
              | none => (l', Seq.nil)
              | some (none, S') => (l', S')
              | some (some c, S') => (c :: l', S') :
              List (Computation α) × WSeq (Computation α)))
          l') =
      C')
  (e : Seq.destruct S = some (o, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a_1 ∈ c
Tactic: obtain ⟨o, S'⟩ := a
Cleared hypotheses: a, h', 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')
o : Option (Computation α)
S' : Stream'.Seq (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              some (o, S') with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = some (o, S')
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀
  (h' :
    corec parallel.aux1
        ((fun (l' : List (Computation α)) ↦
            (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') :
              List (Computation α) × WSeq (Computation α)))
          l') =
      C')
  (e : Seq.destruct S = some (none, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: obtain - | c := o
Cleared hypotheses: o, h', 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')
o : Option (Computation α)
S' : Stream'.Seq (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun (l' : List (Computation α)) ↦
          (match (motive := Option (Seq1 (Option (Computation α))) → List (Computation α) × WSeq (Computation α))
              some (o, S') with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S') :
            List (Computation α) × WSeq (Computation α)))
        l') =
    C'
e : Seq.destruct S = some (o, S')
h2 :
  ∀
    (h' :
      corec parallel.aux1
          ((fun (l' : List (Computation α)) ↦
              (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') :
                List (Computation α) × WSeq (Computation α)))
            l') =
        C')
    (e : Seq.destruct S = some (none, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2₁ : ∀ (c : Computation α)
  (h' :
    corec parallel.aux1
        ((fun (l' : List (Computation α)) ↦
            (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') :
              List (Computation α) × WSeq (Computation α)))
          l') =
      C')
  (e : Seq.destruct S = some (some c, S')), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: obtain - | c := o
Cleared hypotheses: o, h', 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 α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (d : Computation α) (ad : a ∈ d) (dl : d ∈ l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases IH _ _ h' with ⟨d, dl | dS', 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 α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
h2 : ∀ (d : Computation α) (ad : a ∈ d) (dl : d ∈ l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2₁ : ∀ (d : Computation α) (ad : a ∈ d) (dS' : d ∈ S'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases IH _ _ h' with ⟨d, dl | dS', 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')
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (d : Computation α) (ad : a ∈ d) (dl : d ∈ c :: l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases IH _ _ h' with ⟨d, dl | dS', 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')
h2 : ∀ (d : Computation α) (ad : a ∈ d) (dl : d ∈ c :: l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2₁ : ∀ (d : Computation α) (ad : a ∈ d) (dS' : d ∈ S'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases IH _ _ h' with ⟨d, dl | dS', 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 α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, 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 α))
h' : corec parallel.aux1 (l', S') = C'
e : Seq.destruct S = some (none, S')
d : Computation α
ad : a ∈ d
dS' : d ∈ S'
⊢ d ∈ S
have h2 : d ∈ Seq.cons none S'
Tactic: rw [Seq.destruct_eq_cons e]
-- 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
dl : d ∈ c :: l'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have dl₁ : d = c ∨ d ∈ l'
Tactic: simp only [List.mem_cons] at dl
Cleared hypotheses: dl
-- 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
dl : d = c ∨ d ∈ l'
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2 : ∀ (dc : d = c), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases dl with dc | dl
Cleared hypotheses: dl
-- 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
dl : d = c ∨ d ∈ l'
h2 : ∀ (dc : d = c), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
have h2₁ : ∀ (dl : d ∈ l'), ∃ (c : Computation α), (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Tactic: rcases dl with dc | dl
Cleared hypotheses: dl