mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        (corec fun x ↦
            (TypeVec.id ::: fun x ↦ x) <$$>
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
          fun x ↦ x) <$$>
      (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest

Tactic:
]

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        (corec fun x ↦
            (TypeVec.id ::: fun x ↦ x) <$$>
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
          fun x ↦ x) <$$>
      (TypeVec.id ::: Sum.inl) <$$> x.dest)
    x.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) ↔ u ∈ f '' univ

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
⊢ (∀ (a_1 : (P F).A) (f_1 : (P F).B a_1 → α), abs ⟨a_1, f_1⟩ = abs ⟨a, f⟩ → u ∈ f_1 '' univ) ↔ u ∈ f '' univ
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest

Tactic:
]

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    ((TypeVec.id :::
        ((corec fun x ↦
              (TypeVec.id ::: fun x ↦ x) <$$>
                Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x) ∘
            fun x ↦ x) ∘
          Sum.inl) <$$>
      x.dest)
    x.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : (P F).B a' → α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f '' univ

Tactic:
]

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
u : α
h' : u ∈ f '' univ
a' : (P F).A
f' : (P F).B a' → α
e : abs ⟨a', f'⟩ = abs ⟨a, f⟩
⊢ u ∈ f '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp (abs (repr x)), p u

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) ↔ ∀ u ∈ supp (abs (repr x)), p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ f' '' univ → p u

Tactic:
]

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
⊢ u ∈ f' '' univ → p u
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)

Tactic:
]

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
a' : (P F).A
f' : (P F).B a' → α
abseq : abs ⟨a, f⟩ = abs ⟨a', f'⟩
hf : ∀ (i : (P F).B a'), p (f' i)
u : α
i : (P F).B a'
left✝ : i ∈ univ
hi : f' i = u
⊢ p (f' i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
i : (P F).B a
⊢ f i ∈ f '' univ

Tactic:
]

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
x : F α
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : ∀ u ∈ supp (abs ⟨a, f⟩), p u
i : (P F).B a
⊢ f i ∈ f '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
⊢ supp (g <$> abs (repr x)) = g '' supp (abs (repr x))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)

Tactic:
]

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ g '' f '' univ = g '' f '' univ

Tactic:
]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a a' : (P F).A
f : (P F).B a → α
f' : (P F).B a' → α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
⊢ supp ⟨a', f'⟩ = supp ⟨a', f'⟩

Tactic:
]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ f '' univ = f '' univ

pp: case mpr.h
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ IsUniform

Tactic:
]

Goal state after:
case mpr.h
F : Type u → Type u
q : QPF F
h : IsUniform
α : Type u
a : (P F).A
f : (P F).B a → α
⊢ IsUniform
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩

Tactic:
]

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ Liftp p (abs ⟨a, f⟩) ↔ Liftp p ⟨a, f⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)

Tactic:
]

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
⊢ IsUniform ↔ IsUniform

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (match
      match Sum.inl a with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match 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)) =
    Sum.inl a

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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
⊢ (Pure.pure a).Terminates

Tactic:
]

Goal state after:
α : 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
⊢ (Pure.pure a).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inl
α : 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 α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1, parallel.aux2 (pure a :: l) = Sum.inl a_1

Tactic:
]

Goal state after:
case cons.inl
α : 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 α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1, parallel.aux2 (pure a :: l) = Sum.inl a_1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inr.e_g
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map TypeVec.id ∘ Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val) y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y

Tactic:
]

Goal state after:
case inr.e_g
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x i : β
y : Cofix F α ⊕ β
⊢ (MvFunctor.map TypeVec.id ∘ Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val) y =
    Sum.elim (MvFunctor.map (TypeVec.id ::: Sum.inl) ∘ dest) g y
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x

Tactic:
]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inr
α : 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 α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ ∃ a,
    (match Sum.inl a' with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a

Tactic:
]

Goal state after:
case cons.inr
α : 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 α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ ∃ a,
    (match Sum.inl a' with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match c.destruct with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inl
α : 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 α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match 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 =>
      match s.think.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : s.think = c
⊢ s ∈ l'

Tactic:
]

Goal state after:
case cons.inl
α : 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 α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o ↦
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match 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 =>
      match s.think.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : s.think = c
⊢ s ∈ l'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s))) s.destruct

Tactic:
]

Goal state after:
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ Seq.BisimO (fun s1 s2 ↦ flatten (Computation.pure s2) = s1) (Seq.destruct (flatten (Computation.pure s))) s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 ↦ x1 = x2) s.destruct s.destruct

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s✝ s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun x1 x2 ↦ x1 = x2) s.destruct s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Symm R
s1 s2 : WSeq α
h : LiftRel R s2 s1
⊢ LiftRel R s2 s1

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Symm R
s1 s2 : WSeq α
h : LiftRel R s2 s1
⊢ LiftRel R s2 s1
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
x✝ : Option (Seq1 (Option α))
⊢ match
    match
      match x✝ with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c ↦
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    x✝ with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c ↦
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
cases Seq.destruct s with

Goal state after:
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + m + 1) = some a
⊢ k + 1 = k + 1 + m

Tactic:
]

Goal state after:
case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + m + 1) = some a
⊢ k + 1 = k + 1 + m
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
]

Goal state after:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (s.destruct >>= fun x ↦ Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = s.destruct >>= tail.aux

Tactic:
]

Goal state after:
α : Type u
s : WSeq α
⊢ (s.destruct >>= fun x ↦ Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = s.destruct >>= tail.aux
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ Computation.pure none = Computation.pure none

Tactic:
]

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

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun x ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)

Tactic:
]

Goal state after:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun x ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons.inr.inl
α : 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 α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
a' : α
e' :
  (match Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ s ∈ l'

Tactic:
]

Goal state after:
case cons.inr.inl
α : 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 α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : s.think ∈ l
a' : α
e' :
  (match Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match c.destruct with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ s ∈ l'