mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion

Tactic:
·

Goal state after:
case neg
α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ Nonempty s.FiniteExhaustion
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {x}.op → x✝ ∈ {op x}

pp: case mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op

Tactic:
·

Goal state after:
case mp
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {x}.op → x✝ ∈ {op x}
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op

Tactic:
·

Goal state after:
case mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop → x✝ ∈ {unop x}

pp: case mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop

Tactic:
·

Goal state after:
case mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop → x✝ ∈ {unop x}
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop

Tactic:
·

Goal state after:
case mpr
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {unop x} → x✝ ∈ {x}.unop
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}

pp: case mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop

Tactic:
·

Goal state after:
case mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop

Tactic:
·

Goal state after:
case mpr
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {x} → x✝ ∈ {op x}.unop
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op → x✝ ∈ {x}

pp: case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op

Tactic:
·

Goal state after:
case mp
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {unop x}.op → x✝ ∈ {x}
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op

Tactic:
·

Goal state after:
case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none none
⊢ Prod.fst <$> none ∈ t.head

pp: case none.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none (some b)
⊢ Prod.fst <$> none ∈ t.head

pp: case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head

pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
·

Goal state after:
case none.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none none
⊢ Prod.fst <$> none ∈ t.head
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none (some b)
⊢ Prod.fst <$> none ∈ t.head

pp: case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head

pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
·

Goal state after:
case none.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none (some b)
⊢ Prod.fst <$> none ∈ t.head
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

pp: case inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head

pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
·

Goal state after:
case some.none
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a✝ : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
·

Goal state after:
case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case h1
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s

pp: case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s

Tactic:
·

Goal state after:
case h1
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case inl
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')

pp: case inr
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m✝ : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b ↦ some (some a) = b) ↑s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')

Tactic:
·

Goal state after:
case inl
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s

Tactic:
·

Goal state after:
case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case inl
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')

pp: case inr
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m✝ : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b ↦ some (some a) = b) ↑s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')

Tactic:
· rw [e]
      apply Stream'.mem_cons

Goal state after:
case inr
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m✝ : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b ↦ some (some a) = b) ↑s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case inr
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m✝ : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b ↦ some (some a) = b) ↑s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')

Tactic:
·

Goal state after:
case inr
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m✝ : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
m : Any (fun b ↦ some (some a) = b) ↑s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s')
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

pp: case inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
case inr.inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a✝ : some (some c) = S.get? (n + 1)
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
·

Goal state after:
case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (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 α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

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

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

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

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

Tactic:
·

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

Goal state before:
pp: case none
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
h1 : none ∈ (s.drop 0).destruct
h2 : Prod.fst <$> none = some a
⊢ a ∈ s

pp: case some
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s

Tactic:
·

Goal state after:
case none
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
h1 : none ∈ (s.drop 0).destruct
h2 : Prod.fst <$> none = some a
⊢ a ∈ s
Module: Mathlib.Data.WSeq.Relation

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

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

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

Tactic:
·

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

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

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

Tactic:
·

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

Goal state before:
pp: case h1
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons b s').get? n

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:
·

Goal state after:
case h1
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons b s').get? n
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
·

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