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

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y
Module: Mathlib.Data.WSeq.Relation

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

pp: case some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) y = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) y

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) none y = LiftRelO (Function.swap R) (Function.swap C) none y

case some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) y = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) y
Module: Mathlib.Data.WSeq.Relation

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

pp: case none.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) none (some (hy, jy)) = LiftRelO (Function.swap R) (Function.swap C) none (some (hy, jy))

pp: case some.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) none = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) none

pp: case some.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) (some (hy, jy)) =
    LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) (some (hy, jy))

Tactic:
<;>

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

case none.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) none (some (hy, jy)) = LiftRelO (Function.swap R) (Function.swap C) none (some (hy, jy))

case some.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) none = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) none

case some.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) (some (hy, jy)) =
    LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) (some (hy, jy))
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:
LiftRel.swap,

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

Goal state before:
pp: α : Type u
c : Computation (WSeq α)
c1 : Computation (Option (α × WSeq α))
⊢ ∀ ⦃s₂ : Computation (Option (α × WSeq α))⦄,
    (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1 s₂ →
      BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1.destruct s₂.destruct

Tactic:
c2

Goal state after:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
⊢ (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1 c2 →
    BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) c1.destruct c2.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none c

pp: case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) c

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) none c

case some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : Option (α × WSeq α)
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) b c
a : α × WSeq α
ha : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) c
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case succ.none
α : 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
h : sel s = none
⊢ k + 1 = k + 1 + m

pp: case succ.some
α : 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
val✝ : α
h : sel s = some val✝
⊢ k + 1 = k + 1 + m

Tactic:
<;>

Goal state after:
case succ.none
α : 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
h : sel s = none
⊢ k + 1 = k + 1 + m

case succ.some
α : 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
val✝ : α
h : sel s = some val✝
⊢ k + 1 = k + 1 + m
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case inl
α : 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 α))
val✝ : Option (α × WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) (Sum.inl val✝) (Sum.inl val✝)

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

Tactic:
<;>

Goal state after:
case inl
α : 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 α))
val✝ : Option (α × WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) (Sum.inl val✝) (Sum.inl val✝)

case inr
α : Type u
c✝ : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c val✝ : Computation (Option (α × WSeq α))
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct) (Sum.inr val✝) (Sum.inr val✝)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case pure.inl
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Option (α × WSeq α)
⊢ match Sum.inl val✝, Sum.inl val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

pp: case pure.inr
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Computation (Option (α × WSeq α))
⊢ match Sum.inr val✝, Sum.inr val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
<;>

Goal state after:
case pure.inl
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Option (α × WSeq α)
⊢ match Sum.inl val✝, Sum.inl val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

case pure.inr
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Computation (Option (α × WSeq α))
⊢ match Sum.inr val✝, Sum.inr val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero
α : Type u
⊢ nil.drop 0 = nil

pp: case succ
α : Type u
n✝ : ℕ
a✝ : nil.drop n✝ = nil
⊢ nil.drop (n✝ + 1) = nil

Tactic:
<;>

Goal state after:
case zero
α : Type u
⊢ nil.drop 0 = nil

case succ
α : Type u
n✝ : ℕ
a✝ : nil.drop n✝ = nil
⊢ nil.drop (n✝ + 1) = nil
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: case zero
α : Type u
s : WSeq α
⊢ s.think.drop 0 = (s.drop 0).think

pp: case succ
α : Type u
s : WSeq α
n✝ : ℕ
a✝ : s.think.drop n✝ = (s.drop n✝).think
⊢ s.think.drop (n✝ + 1) = (s.drop (n✝ + 1)).think

Tactic:
<;>

Goal state after:
case zero
α : Type u
s : WSeq α
⊢ s.think.drop 0 = (s.drop 0).think

case succ
α : Type u
s : WSeq α
n✝ : ℕ
a✝ : s.think.drop n✝ = (s.drop n✝).think
⊢ s.think.drop (n✝ + 1) = (s.drop (n✝ + 1)).think
Module: Mathlib.Data.WSeq.Basic

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

pp: case some
α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ Pure.pure (Option.rec nil Prod.snd (some (a, s))) >>= destruct = tail.aux (some (a, s))

Tactic:
<;>

Goal state after:
case none
α : Type u
s : WSeq α
⊢ Pure.pure (Option.rec nil Prod.snd none) >>= destruct = tail.aux none

case some
α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ Pure.pure (Option.rec nil Prod.snd (some (a, s))) >>= destruct = tail.aux (some (a, s))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (Option.rec nil Prod.snd none).destruct = tail.aux none

pp: α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ (Option.rec nil Prod.snd (some (a, s))).destruct = tail.aux (some (a, s))

Tactic:
<;>

Goal state after:
α : Type u
s : WSeq α
⊢ (Option.rec nil Prod.snd none).destruct = tail.aux none

α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ (Option.rec nil Prod.snd (some (a, s))).destruct = tail.aux (some (a, s))
Module: Mathlib.Data.WSeq.Basic

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

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

Tactic:
<;>

Goal state after:
case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.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 α
td : some a ∈ t.destruct
t' : α × WSeq α
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: 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

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

Tactic:
<;>

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.WSeq.Basic

Goal state before:
pp: case mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f → some (some a) ∈ f

pp: case mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ f → some (some a) ∈ some none :: f

Tactic:
<;>

Goal state after:
case mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f → some (some a) ∈ f

case mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ f → some (some a) ∈ some none :: f
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α}, s.destruct = Computation.pure (some (a', s')) → (a ∈ s ↔ a = a' ∨ a ∈ s')

pp: case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
⊢ ∀ {s : WSeq α}, s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
<;>

Goal state after:
case h1
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α}, s.destruct = Computation.pure (some (a', s')) → (a ∈ s ↔ a = a' ∨ a ∈ s')

case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
⊢ ∀ {s : WSeq α}, s.destruct = c.think → (a ∈ s ↔ a = a' ∨ a ∈ s')
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
m : s.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'

pp: case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s : WSeq α
m : s.destruct = c.think
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'

Tactic:
<;>

Goal state after:
case h1
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
m : s.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'

case h2
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s : WSeq α
m : s.destruct = c.think
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case 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
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none dt
⊢ Prod.fst <$> none ∈ t.head

pp: case 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
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) dt
⊢ Prod.fst <$> some a ∈ t.head

Tactic:
<;>

Goal state after:
case 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
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dsm : none ∈ s.destruct
dse : Prod.fst <$> none = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) none dt
⊢ Prod.fst <$> none ∈ t.head

case 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
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some a) dt
⊢ Prod.fst <$> some a ∈ t.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1.nil
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : nil.destruct = Computation.pure (some (a', s'))
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

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'))
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

pp: case h1.think
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

pp: case h2.nil
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
m : nil.destruct = c.think
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

pp: case h2.cons
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

pp: case h2.think
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

Tactic:
<;>

Goal state after:
case h1.nil
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : nil.destruct = Computation.pure (some (a', s'))
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

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'))
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

case h1.think
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

case h2.nil
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
m : nil.destruct = c.think
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

case h2.cons
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

case h2.think
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'