mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case zero
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
⊢ ∀ (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

pp: case succ
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
n✝ : ℕ
a✝ :
  ∀ (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:
<;>

Goal state after:
case zero
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
⊢ ∀ (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

case succ
α : Type u
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : c.Terminates
n✝ : ℕ
a✝ :
  ∀ (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
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get 0 → a ∈ s

pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get (n✝ + 1) → a ∈ s

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get 0 → a ∈ s

case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
⊢ ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get (n✝ + 1) → a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail).get 0
⊢ a ∈ s

pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail).get (n✝ + 1)
⊢ a ∈ s

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail).get 0
⊢ a ∈ s

case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = (↑s.tail).get (n✝ + 1)
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : Option (α × WSeq α)
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none b
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd b

pp: case some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : Option (α × WSeq α)
a : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) b
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd b

Tactic:
<;>

Goal state after:
case none
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : Option (α × WSeq α)
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none b
⊢ Option.rec nil Prod.snd none ~ʷ Option.rec nil Prod.snd b

case some
α : Type u
s t : WSeq α
h✝ : s ~ʷ t
b : Option (α × WSeq α)
a : α × WSeq α
h : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) b
⊢ Option.rec nil Prod.snd (some a) ~ʷ Option.rec nil Prod.snd b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
a : α
s : WSeq α
⊢ some a ∈ s.get? 0 → a ∈ s

pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, some a ∈ s.get? n✝ → a ∈ s
s : WSeq α
⊢ some a ∈ s.get? (n✝ + 1) → a ∈ s

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
s : WSeq α
⊢ some a ∈ s.get? 0 → a ∈ s

case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, some a ∈ s.get? n✝ → a ∈ s
s : WSeq α
⊢ some a ∈ s.get? (n✝ + 1) → a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case zero
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.drop 0 ~ʷ t.drop 0

pp: case succ
α : Type u
s t : WSeq α
h : s ~ʷ t
n✝ : ℕ
a✝ : s.drop n✝ ~ʷ t.drop n✝
⊢ s.drop (n✝ + 1) ~ʷ t.drop (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.drop 0 ~ʷ t.drop 0

case succ
α : Type u
s t : WSeq α
h : s ~ʷ t
n✝ : ℕ
a✝ : s.drop n✝ ~ʷ t.drop n✝
⊢ s.drop (n✝ + 1) ~ʷ t.drop (n✝ + 1)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (s : WSeq α), (∃ n, some a ∈ s.get? n) → ∃ n, some a ∈ s.think.get? n

Tactic:
· intro s' h
    obtain ⟨n, h⟩ := h
    exists n
    simp only [get?, dropn_think, head_think]
    apply think_mem h

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case refine_2.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : Option (α × WSeq α)
mb : b ∈ t.destruct
ma : none ∈ s.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none b

pp: case refine_2.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : Option (α × WSeq α)
mb : b ∈ t.destruct
a : α × WSeq α
ma : some a ∈ s.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) b

Tactic:
<;>

Goal state after:
case refine_2.none
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : Option (α × WSeq α)
mb : b ∈ t.destruct
ma : none ∈ s.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none b

case refine_2.some
α : Type u
s✝ t✝ : WSeq α
h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n
s t : WSeq α
h : (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
b : Option (α × WSeq α)
mb : b ∈ t.destruct
a : α × WSeq α
ma : some a ∈ s.destruct
⊢ LiftRelO Eq (fun s t ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) b
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) none p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) p)

pp: case some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) p)

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) none p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) p)

case some
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some a)) (Option.map (Prod.map f2 (map f2)) p)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
⊢ List (Computation α) → α ⊕ List (Computation α) → Prop

Tactic:
intro l a

Goal state after:
α : Type u
S : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S
l : List (Computation α)
a : α ⊕ List (Computation α)
⊢ Prop
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case nil
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (parallel.aux2 [])

pp: case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝) (parallel.aux2 (head✝ :: tail✝))

Tactic:
<;>

Goal state after:
case nil
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
⊢ F [] (parallel.aux2 [])

case cons
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
head✝ : Computation α
tail✝ : List (Computation α)
tail_ih✝ : F tail✝ (parallel.aux2 tail✝)
⊢ F (head✝ :: tail✝) (parallel.aux2 (head✝ :: tail✝))
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
⊢ F l (Sum.inl val✝) →
    F (c :: l)
      (match Sum.inl val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

pp: case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
⊢ F l (Sum.inr val✝) →
    F (c :: l)
      (match Sum.inr val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
<;>

Goal state after:
case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
⊢ F l (Sum.inl val✝) →
    F (c :: l)
      (match Sum.inl val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
⊢ F l (Sum.inr val✝) →
    F (c :: l)
      (match Sum.inr val✝ with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
IH : F l (Sum.inl val✝)
⊢ F (c :: l)
    (match Sum.inl val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

pp: case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
⊢ F (c :: l)
    (match Sum.inr val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

Tactic:
<;>

Goal state after:
case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
IH : F l (Sum.inl val✝)
⊢ F (c :: l)
    (match Sum.inl val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)

case inr
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
⊢ F (c :: l)
    (match Sum.inr val✝ with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' ↦ c' :: ls) c.destruct)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) (Sum.inl a))

pp: case inr.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) (Sum.inr c'))

Tactic:
<;>

Goal state after:
case inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) (Sum.inl a))

case inr.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) (Sum.inr c'))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) none p
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 none) (destruct_append.aux t2 p)

pp: case some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) p
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 p)

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) none p
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 none) (destruct_append.aux t2 p)

case some
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (some a) p
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some a)) (destruct_append.aux t2 p)
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hab : ⟨j✝, a⟩ < ⟨i✝, b⟩
⊢ False

pp: case refine_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : ⟨i✝, a⟩ < ⟨i✝, b⟩
⊢ False

Tactic:
<;>

Goal state after:
case refine_1.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ j✝ : ι
b : α i✝
a : α j✝
hji : i✝ < j✝
hab : ⟨j✝, a⟩ < ⟨i✝, b⟩
⊢ False

case refine_1.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i✝ : ι
b a : α i✝
hba : b ≤ a
hab : ⟨i✝, a⟩ < ⟨i✝, b⟩
⊢ False
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
apply memRecOn aC

Goal state after:
case h1
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop := ⋯
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = pure a → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop := ⋯
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (s : Computation α),
    (∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = s → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c) →
      ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
        corec parallel.aux1 (l, S) = s.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop := ⋯
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = pure a → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

pp: case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (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, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C'.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
<;>

Goal state after:
case h1
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop := ⋯
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = pure a → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

case h2
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (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, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C'.think → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) none) = Computation.pure none

pp: case some
α : Type u
s : Seq α
val✝ : α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) (some val✝)) = Computation.pure (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) none) = Computation.pure none

case some
α : Type u
s : Seq α
val✝ : α
⊢ Computation.pure (Option.map (Prod.fst ∘ fun a ↦ (a, ↑s.tail)) (some val✝)) = Computation.pure (some val✝)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case nil
α : Type u
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑Seq.nil.tail)) Seq.nil.head) = ↑Seq.nil.tail

pp: case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑(Seq.cons x✝ s✝).tail)) (Seq.cons x✝ s✝).head) =
    ↑(Seq.cons x✝ s✝).tail

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑Seq.nil.tail)) Seq.nil.head) = ↑Seq.nil.tail

case cons
α : Type u
x✝ : α
s✝ : Seq α
⊢ Option.rec nil Prod.snd (Option.map (fun a ↦ (a, ↑(Seq.cons x✝ s✝).tail)) (Seq.cons x✝ s✝).head) =
    ↑(Seq.cons x✝ s✝).tail