mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) = LiftRelO (Function.swap R) (Function.swap C)

Tactic:
funext x y
  rcases x with ⟨⟩ | ⟨hx, jx⟩ <;> rcases y with ⟨⟩ | ⟨hy, jy⟩ <;> rfl

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) = LiftRelO (Function.swap R) (Function.swap C)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R✝ (LiftRel R✝)) s.destruct t.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).destruct.destruct = Sum.inl (some (a, s))

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think.destruct.destruct = Sum.inr s.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ nil.head = Computation.pure none

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).head = Computation.pure (some a)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think.head = s.head.think

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap R) s2 s1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
⊢ enumerate sel s 0 = none

Tactic:
by

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
s : Set α
h : sel s = none
n : ℕ
⊢ enumerate sel s (n + 1) = none

Tactic:
by

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
s : Set α
n m : ℕ
h : enumerate sel s (n + 1) = none
hm : n + 1 ≤ m
⊢ enumerate sel s m = none

Tactic:
by

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
a : Option (α × WSeq α)
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) a a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
s : WSeq α
⊢ LiftRel R s s

Tactic:
by

Goal state after:
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 : Function.swap (LiftRel R) s2 s1
⊢ LiftRel R s2 s1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ flatten (Computation.pure s) = s

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Computation (WSeq α)
⊢ Seq.destruct (flatten c.think) = some (none, flatten c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
sel : Set α → Option α
n₁ n₂ : ℕ
a : α
s : Set α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
h₁ : enumerate sel s n₁ = some a
h₂ : enumerate sel s n₂ = some a
⊢ n₁ = n₂

Tactic:
by

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

Goal state before:
pp: α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c.destruct c.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) (flatten c).destruct.destruct
    (c.bind destruct).destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Computation (WSeq α)
⊢ (flatten c).destruct = c >>= destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ nil.tail = nil

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : WSeq α
⊢ (cons a s).tail = s

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think.tail = s.tail.think

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ nil.drop n = nil

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
⊢ S.think.join = S.join.think

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
S : WSeq (WSeq α)
⊢ (cons s S).join = (s.append S.join).think

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.tail.destruct = s.destruct >>= tail.aux

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
T : s.tail.head.Terminates
⊢ s.destruct.Terminates

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd t' = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
rcases t' with - | t' <;> rw [← ht2] at td

Goal state after:
case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ (Option.rec nil Prod.snd none).destruct
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
⊢ ∃ a', some a' ∈ s.destruct

case some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ (Option.rec nil Prod.snd (some t')).destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
l' : List (Computation α)
e' : parallel.aux2 l = Sum.inr l'
⊢ s ∈ l'

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α × WSeq α
h : some a ∈ s.tail.destruct
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : some a ∈ s.tail.head
⊢ ∃ a', some a' ∈ s.head

Tactic:
by

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

Goal state before:
pp: case 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
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
a : α
h : parallel.aux2 l = Sum.inl a
⊢ (corec parallel.aux1 (l, S)).Terminates

pp: case 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
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
· exact lem1 _ _ ⟨a, h⟩

Goal state after:
case 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
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ a', some a' ∈ s.head

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
⊢ (s.get? n).Terminates → (s.get? m).Terminates

Tactic:
by

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

Goal state before:
pp: α : 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
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).destruct = Sum.inr ?m.407

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.List

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.List

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length ≤ n}.Finite

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
⊢ IsTrans (WSeq α) (LiftRel R)

Tactic:
by

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

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
⊢ C s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
a : Option (α × WSeq α)
b : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a b
x✝ : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux none) (tail.aux none)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Monad

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝² : DecidableEq β
f : Set (α → β)
s : Set α
inst✝¹ : Fintype ↑f
inst✝ : Fintype ↑s
⊢ Fintype ↑(f.seq s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s✝ : WSeq α
t✝ : WSeq β
H : LiftRel R s✝ t✝
n : ℕ
a✝ : Option (α × WSeq α)
b✝ : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a✝ b✝
a : α
s : WSeq α
b : β
t : WSeq β
left✝ : R a b
h2 : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux (some (a, s))) (tail.aux (some (b, t)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Finite.Monad

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
f : Set (α → β)
s : Set α
inst✝¹ : Finite ↑f
inst✝ : Finite ↑s
⊢ Finite ↑(f.seq s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop (n + 1)).destruct (t.drop (n + 1)).destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h : a ∈ s
⊢ ∃ b ∈ t, R a b

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
a : α
⊢ a ∈ s.think ↔ a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
⊢ LiftRel R nil nil

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ LiftRel R s.think t ↔ LiftRel R s t

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ LiftRel R s t.think ↔ LiftRel R s t

Tactic:
by

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

Goal state before:
pp: α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ cons a s ~ʷ cons a t

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ s.think ~ʷ s

Tactic:
by

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.think ~ʷ t.think

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
⊢ ∀ (n : ℕ), Finite ↑∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
n : ℕ
⊢ ∅ ⊆ ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
⊢ s.FiniteExhaustion

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ Nonempty s.FiniteExhaustion ↔ s.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
⊢ ⋃ n, K n ×ˢ K' n = s ×ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
n : ℕ
⊢ (K.prod K') n = K n ×ˢ K' n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ op a ∈ s.op ↔ a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set αᵒᵖ
a : αᵒᵖ
⊢ unop a ∈ s.unop ↔ a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
⊢ {x}.op = {op x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : αᵒᵖ
⊢ {x}.unop = {unop x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
⊢ {op x}.unop = {x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : αᵒᵖ
⊢ {unop x}.op = {x}

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → c.Terminates → (corec parallel.aux1 (l, S)).Terminates

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ S.destruct = some (some c, S.tail)

Tactic:
by

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

Goal state before:
pp: α : 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) = pure a

Tactic:
by

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

Goal state before:
pp: α : 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'
⊢ a = a' ↔ some (some a) = some (some a')

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ ∀ {s t : WSeq α}, s ~ʷ t → s.head ~ t.head

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ Computation.LiftRel (LiftRelO R S) (flatten c1).destruct (flatten c2).destruct

Tactic:
simp only [destruct_flatten]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ Computation.LiftRel (LiftRelO R S) (c1 >>= destruct) (c2 >>= destruct)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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)).destruct = Sum.inr ?m.158

Tactic:
by

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

Goal state before:
pp: case h1.cons
α : 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'))
this : (cons x✝ s✝).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
case h1.cons =>
    simp only [destruct_cons, destruct_pure, Sum.inl.injEq, Option.some.injEq,
      Prod.mk.injEq] at this
    obtain ⟨i1, i2⟩ := this
    rw [i1, i2]
    dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]
    have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
    rw [h_a_eq_a']
    refine ⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩
    rcases o with e | m
    · rw [e]
      apply Stream'.mem_cons
    · exact Stream'.mem_cons_of_mem _ m

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

Goal state before:
pp: α : Type u
s : WSeq α
a a' : α
s' : WSeq α
⊢ some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
by

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

Goal state before:
pp: α : Type u
s : WSeq α
b a : α
⊢ some (b, s) ∈ (cons b s).destruct

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : 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) = pure a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ Computation.LiftRel (LiftRelO R S) (flatten c1).destruct (flatten c2).destruct

Tactic:
by

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

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

Tactic:
by

Goal state after: