awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h :
  Eq.{u + 1} (α := Option α) ((fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) n) none
rw : ∀ (h : l.length ≤ n), l.length ≤ n + 1
⊢ Eq.{u + 1} (α := Option α) ((fun (x : ℕ) ↦ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l x) (n + 1))
    none

Tactic:
rw [List.getElem?_eq_none_iff] at h ⊢

Premises used: List.getElem?_eq_none_iff
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : l.length ≤ n
⊢ l.length ≤ n + 1

Tactic:
Nat.le_succ_of_le h

Premises used: Nat.le_succ_of_le
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : l.length ≤ n
⊢ l.length ≤ n + 1

Tactic:
exact Nat.le_succ_of_le h

Premises used: Nat.le_succ_of_le
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Seq α) (↑[] : Seq α) nil

Tactic:
rfl

Premises used: Stream'.Seq.ofList, Stream'.Seq.nil, Stream'.const, List.get?Internal, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
l : List α
n : ℕ
⊢ (↑l : Seq α).get? n = getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n

Tactic:
rfl

Premises used: rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
l : List α
h : (↑(a :: l) : Seq α).get? 0 = (cons a (↑l : Seq α)).get? 0
h₁ : ∀ (n : ℕ), (↑(a :: l) : Seq α).get? (n + 1) = (cons a (↑l : Seq α)).get? (n + 1)
⊢ (↑(a :: l) : Seq α) = cons a (↑l : Seq α)

Tactic:
ext1 (_ | n)
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
l : List α
⊢ (↑(a :: l) : Seq α).get? 0 = (cons a (↑l : Seq α)).get? 0

Tactic:
simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
l : List α
n : ℕ
⊢ (↑(a :: l) : Seq α).get? (n + 1) = (cons a (↑l : Seq α)).get? (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ Function.Injective.{u + 1, u + 1} (α := List α) ofList

Tactic:
fun _ _ h => List.ext_getElem? fun _ => congr_fun (Subtype.ext_iff.1 h) _

Premises used: Subtype.ext_iff, List.ext_getElem?, Iff.mp, Function.Injective, congr_fun
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Stream' α
n : ℕ
h : map some s n = none
⊢ map some s (n + 1) = none

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
dsimp : Option.map f (s n) = none → Option.map f (s (n + 1)) = none
⊢ Stream'.map (Option.map f) s n = none → Stream'.map (Option.map f) s (n + 1) = none

Tactic:
dsimp [Stream'.map, Stream'.get]

Premises used: Stream'.get, Stream'.map
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
none : ∀ (e : s n = Option.none), Option.map f Option.none = Option.none → Option.map f (s (n + 1)) = Option.none
some :
  ∀ (e : α) (e_1 : s n = Option.some e),
    Option.map f (Option.some e) = Option.none → Option.map f (s (n + 1)) = Option.none
⊢ Option.map f (s n) = Option.none → Option.map f (s (n + 1)) = Option.none

Tactic:
rcases e : s n with - | e
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = Option.none
h none : Option.map f Option.none = Option.none
⊢ Option.map f (s (n + 1)) = Option.none

Tactic:
rw [al e]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
h : Option.map f none = none
⊢ Option.map f none = none

Tactic:
assumption
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e_1 : α
e : s n = some e_1
h : Option.map f (some e_1) = none
⊢ Option.map f (s (n + 1)) = none

Tactic:
contradiction
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
pos :
  ∀ (hi : i = n),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
neg :
  ∀ (hi : ¬i = n),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
⊢ Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none

Tactic:
by_cases hi : i = n
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : i = n
⊢ Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none

Tactic:
simp [Function.update, hi]

Premises used: Function.update
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : ¬i = n
⊢ Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
    s.get? i = none

Tactic:
simp [Function.update, hi]

Premises used: Function.update
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
⊢ ∀ (i : ℕ),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none

Tactic:
have (i : ℕ) : Function.update s.val n ((s.get? n).map f) i = none ↔ s.get? i = none := by
      by_cases hi : i = n <;> simp [Function.update, hi]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
this :
  ∀ (i : ℕ),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
simp : ∀ {n : ℕ}, s.get? n = none → s.get? (n + 1) = none
⊢ IsSeq
    (Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n
      (Option.map f ((↑s : Stream' (Option α)) n)))

Tactic:
simp only [IsSeq, val_eq_get, this]

Premises used: Stream'.Seq.val_eq_get, Stream'.IsSeq
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
this :
  ∀ (i : ℕ),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
⊢ ∀ {n : ℕ}, s.get? n = none → s.get? (n + 1) = none

Tactic:
@s.prop

Premises used: Stream'.IsSeq, Subtype.prop, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
this :
  ∀ (i : ℕ),
    Function.update (β := fun (a : ℕ) ↦ Option α) (↑s : Stream' (Option α)) n (Option.map f (s.get? n)) i = none ↔
      s.get? i = none
⊢ ∀ {n : ℕ}, s.get? n = none → s.get? (n + 1) = none

Tactic:
exact @s.prop

Premises used: Subtype.prop
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ (a : α), parallel.aux2 l = Sum.inl a
obtain : ∀ (a : α) (e : parallel.aux2 l = Sum.inl a), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
obtain ⟨a, e⟩ := e
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
a₁ : (corec parallel.aux1 (l, S)).destruct = Sum.inl a
⊢ corec parallel.aux1 (l, S) = Pure.pure a

Tactic:
apply destruct_eq_pure

Premises used: Computation.destruct_eq_pure
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
a₁ :
  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.inl a : α ⊕ Computation α)
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inl a

Tactic:
simp only [parallel.aux1, rmap, corec_eq]

Premises used: Computation.rmap, _private.0.Computation.parallel.aux1, Computation.corec_eq
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
a₁ a₂ :
  Eq.{u + 1} (α := α ⊕ 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) :
      α ⊕ Computation α)
    (Sum.inl a : α ⊕ Computation α)
⊢ 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.inl a : α ⊕ Computation α)

Tactic:
rw [e]
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = Pure.pure a

Tactic:
have : corec parallel.aux1 (l, S) = return a := by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
rw : Terminates (Pure.pure a)
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rw [this]
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ Terminates (Pure.pure a)

Tactic:
ret_terminates a

Premises used: Computation.ret_terminates
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ Terminates (Pure.pure a)

Tactic:
exact ret_terminates a

Premises used: Computation.ret_terminates
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates

Tactic:
have lem1 :
    ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := by
    intro l S e
    obtain ⟨a, e⟩ := e
    have : corec parallel.aux1 (l, S) = return a := by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
    rw [this]
    exact ret_terminates a
-- Module: Mathlib.Data.Seq.Parallel
Goal:
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ (a : α), parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
T : c.Terminates
revert : ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : c ∈ l), (corec parallel.aux1 (l, S)).Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
revert l S
-- Module: Mathlib.Data.Seq.Parallel
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
apply :
  ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)} (m : pure a ∈ l),
    (corec parallel.aux1 (l, S)).Terminates
apply₁ :
  ∀ (s : Computation α),
    (∀ {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), (corec parallel.aux1 (l, S)).Terminates
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} (m : c ∈ l), (corec parallel.aux1 (l, S)).Terminates

Tactic:
apply @terminatesRecOn _ _ c T _ _

Premises used: Computation.terminatesRecOn
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
a₁ : ∃ (a : α), parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
apply lem1
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
m : Membership.mem (γ := List (Computation α)) [] (pure a)
⊢ ∃ (a : α), parallel.aux2 [] = Sum.inl a

Tactic:
simp at m
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ c :: l
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a

Tactic:
?_
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
a₁ :
  ∀ (c : Computation α) (l : List (Computation α)) (IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a)
    (m : pure a ∈ c :: l), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
⊢ ∃ (a : α), parallel.aux2 l = Sum.inl a

Tactic:
induction l with | nil => simp at m | cons c l IH => ?_

Premises used: Stream'.cons
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ c :: l
⊢ pure a = c ∨ pure a ∈ l

Tactic:
simp only [List.mem_cons] at m

Premises used: List.mem_cons
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a = c ∨ pure a ∈ l
a₁ : ∀ (e : pure a = c), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
a₂ : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a

Tactic:
rcases m with e | m
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
a₁ : ∃ (a_1 : α), parallel.aux2 (pure a :: l) = Sum.inl a_1
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a

Tactic:
rw [← e]
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
a₁ :
  ∃ (a_1 : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ 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 ls => Sum.inl a :
        α ⊕ List (Computation α))
      (Sum.inl a_1 : α ⊕ List (Computation α))
⊢ ∃ (a_1 : α), parallel.aux2 (pure a :: l) = Sum.inl a_1

Tactic:
simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]

Premises used: Computation.destruct_pure, List.foldr_cons, Computation.rmap, _private.0.Computation.parallel.aux2
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
h_1 :
  ∀ (o : α ⊕ List (Computation α)) (a : α),
    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 []) l)
        (Sum.inl a) →
      ∃ (a_1 : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a) (Sum.inl a_1)
h_2 :
  ∀ (o : α ⊕ List (Computation α)) (ls : List (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 []) l)
        (Sum.inr ls) →
      ∃ (a_1 : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a) (Sum.inl a_1)
⊢ ∃ (a_1 : α),
    Eq (α := α ⊕ List (Computation α))
      (match (motive := α ⊕ List (Computation α) → α ⊕ 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 ls => Sum.inl a :
        α ⊕ List (Computation α))
      (Sum.inl a_1 : α ⊕ List (Computation α))

Tactic:
split
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
o : α ⊕ List (Computation α)
a_1 : α
heq :
  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 []) l)
    (Sum.inl a_1)
⊢ ∃ (a : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a_1) (Sum.inl a)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
e : pure a = c
o : α ⊕ List (Computation α)
ls : List (Computation α)
heq :
  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 []) l)
    (Sum.inr ls)
⊢ ∃ (a_1 : α), Eq (α := α ⊕ List (Computation α)) (Sum.inl a) (Sum.inl a_1)

Tactic:
simp
-- Module: Mathlib.Data.Seq.Parallel
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
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : ∀ (m : pure a ∈ l), ∃ (a : α), parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a₁ : ∀ (a' : α) (e : parallel.aux2 l = Sum.inl a'), ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a
⊢ ∃ (a : α), parallel.aux2 (c :: l) = Sum.inl a

Tactic:
obtain ⟨a', e⟩ := IH m