awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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 : Option.none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) Option.none b
none :
  ∀ (hc : Option.none ∈ u.destruct) (t2 : LiftRelO R (LiftRel R) b Option.none),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none Option.none
none₁ :
  ∀ (c : α × WSeq α) (hc : some c ∈ u.destruct) (t2 : LiftRelO R (LiftRel R) b (some c)),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none (some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none c

Tactic:
obtain - | c := c
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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 : Option.some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (Option.some a) b
some :
  ∀ (hc : none ∈ u.destruct) (t2 : LiftRelO R (LiftRel R) b none),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) none
some₁ :
  ∀ (c : α × WSeq α) (hc : Option.some c ∈ u.destruct) (t2 : LiftRelO R (LiftRel R) b (Option.some c)),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) (Option.some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) c

Tactic:
obtain - | c := c
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
b : Option (α × WSeq α)
hb : b ∈ t.destruct
ha : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) none none

Tactic:
trivial
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
b : Option (α × WSeq α)
hb : b ∈ t.destruct
ha : Option.none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) Option.none b
c : α × WSeq α
hc : some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (some c)
none :
  ∀ (hb : Option.none ∈ t.destruct) (t1 : LiftRelO R (LiftRel R) Option.none Option.none)
    (t2 : LiftRelO R (LiftRel R) Option.none (some c)),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none (some c)
none₁ :
  ∀ (val : α × WSeq α) (hb : some val ∈ t.destruct) (t1 : LiftRelO R (LiftRel R) Option.none (some val))
    (t2 : LiftRelO R (LiftRel R) (some val) (some c)),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none (some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none (some c)

Tactic:
cases b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
hb : none ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none none
t2 : LiftRelO R (LiftRel R) none (some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
cases t2
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
ha : none ∈ s.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
val : α × WSeq α
hb : some val ∈ t.destruct
t1 : LiftRelO R (LiftRel R) none (some val)
t2 : LiftRelO R (LiftRel R) (some val) (some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
cases t1
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
b : Option (α × WSeq α)
hb : b ∈ t.destruct
a : α × WSeq α
ha : Option.some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (Option.some a) b
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
some :
  ∀ (fst : α) (snd : WSeq α) (ha : Option.some (fst, snd) ∈ s.destruct)
    (t1 : LiftRelO R (LiftRel R) (Option.some (fst, snd)) b),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) none

Tactic:
cases a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
b : Option (α × WSeq α)
hb : b ∈ t.destruct
hc : none ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b none
fst : α
snd : WSeq α
ha : Option.some (fst, snd) ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (Option.some (fst, snd)) b
some :
  ∀ (hb : none ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) none none)
    (t1 : LiftRelO R (LiftRel R) (Option.some (fst, snd)) none),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none
some₁ :
  ∀ (b : α × WSeq α) (hb : Option.some b ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) (Option.some b) none)
    (t1 : LiftRelO R (LiftRel R) (Option.some (fst, snd)) (Option.some b)),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
hc : none ∈ u.destruct
fst : α
snd : WSeq α
ha : some (fst, snd) ∈ s.destruct
hb : none ∈ t.destruct
t2 : LiftRelO R (LiftRel R) none none
t1 : LiftRelO R (LiftRel R) (some (fst, snd)) none
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (fst, snd)) none

Tactic:
cases t1
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
hc : none ∈ u.destruct
fst : α
snd : WSeq α
ha : Option.some (fst, snd) ∈ s.destruct
b : α × WSeq α
hb : Option.some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (Option.some b) none
t1 : LiftRelO R (LiftRel R) (Option.some (fst, snd)) (Option.some b)
some :
  ∀ (fst_1 : α) (snd_1 : WSeq α) (hb : Option.some (fst_1, snd_1) ∈ t.destruct)
    (t2 : LiftRelO R (LiftRel R) (Option.some (fst_1, snd_1)) none)
    (t1 : LiftRelO R (LiftRel R) (Option.some (fst, snd)) (Option.some (fst_1, snd_1))),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none

Tactic:
cases b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
hc : none ∈ u.destruct
fst : α
snd : WSeq α
ha : some (fst, snd) ∈ s.destruct
fst_1 : α
snd_1 : WSeq α
hb : some (fst_1, snd_1) ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some (fst_1, snd_1)) none
t1 : LiftRelO R (LiftRel R) (some (fst, snd)) (some (fst_1, snd_1))
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (fst, snd)) none

Tactic:
cases t2
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s u t : WSeq α
h1_2 : LiftRel R s t
h2_2 : 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
b : Option (α × WSeq α)
hb : b ∈ t.destruct
a : α × WSeq α
ha : Option.some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (Option.some a) b
c : α × WSeq α
hc : Option.some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (Option.some c)
some :
  ∀ (a : α) (s_2 : WSeq α) (ha : Option.some (a, s_2) ∈ s.destruct)
    (t1 : LiftRelO R (LiftRel R) (Option.some (a, s_2)) b),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s_2))
      (Option.some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) (Option.some c)

Tactic:
obtain ⟨a, s⟩ := a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t : WSeq α
h1_2 : LiftRel R s_2 t
h2_2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
c : α × WSeq α
hc : Option.some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (Option.some c)
a : α
s : WSeq α
ha : Option.some (a, s) ∈ s_2.destruct
t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) b
some :
  ∀ (hb : none ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) none (Option.some c))
    (t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) none),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)
some₁ :
  ∀ (b : α × WSeq α) (hb : Option.some b ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) (Option.some b) (Option.some c))
    (t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some b)),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t : WSeq α
h1_2 : LiftRel R s_2 t
h2_2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
hb : none ∈ t.destruct
t2 : LiftRelO R (LiftRel R) none (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) none
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
cases t1
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t : WSeq α
h1_2 : LiftRel R s_2 t
h2_2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : Option.some c ∈ u.destruct
a : α
s : WSeq α
ha : Option.some (a, s) ∈ s_2.destruct
b : α × WSeq α
hb : Option.some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (Option.some b) (Option.some c)
t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some b)
some :
  ∀ (b : α) (t_2 : WSeq α) (hb : Option.some (b, t_2) ∈ t.destruct)
    (t2 : LiftRelO R (LiftRel R) (Option.some (b, t_2)) (Option.some c))
    (t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some (b, t_2))),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)

Tactic:
obtain ⟨b, t⟩ := b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u.destruct
c : α × WSeq α
hc : Option.some c ∈ u.destruct
a : α
s : WSeq α
ha : Option.some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : Option.some (b, t) ∈ t_2.destruct
t2 : LiftRelO R (LiftRel R) (Option.some (b, t)) (Option.some c)
t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some (b, t))
some :
  ∀ (c : α) (u_2 : WSeq α) (hc : Option.some (c, u_2) ∈ u.destruct)
    (t2 : LiftRelO R (LiftRel R) (Option.some (b, t)) (Option.some (c, u_2))),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s))
      (Option.some (c, u_2))
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)

Tactic:
obtain ⟨c, u⟩ := c
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
⊢ R a b

Tactic:
obtain ⟨ab, st⟩ := t1
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
⊢ LiftRel R s t

Tactic:
obtain ⟨ab, st⟩ := t1
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ R b c

Tactic:
obtain ⟨bc, tu⟩ := t2
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
bc : R b c
⊢ LiftRel R t u

Tactic:
obtain ⟨bc, tu⟩ := t2
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Tactic:
⟨trans_of R ab bc, t, st, tu⟩

Premises used: Stream'.WSeq.LiftRelO, And.intro, Exists.intro, trans_of
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Tactic:
exact ⟨trans_of R ab bc, t, st, tu⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
⊢ ∀ (s : WSeq α), s ~ʷ s

Tactic:
LiftRel.refl (· = ·) |>.refl

Premises used: Std.Refl.refl, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
⊢ ∀ {s t : WSeq α}, s ~ʷ t → t ~ʷ s

Tactic:
@(LiftRel.symm (· = ·) (@Eq.symm _))

Premises used: Symmetric, Stream'.WSeq.LiftRel.symm, Eq.symm, Eq, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t u : WSeq α
⊢ s ~ʷ t → t ~ʷ u → s ~ʷ u

Tactic:
LiftRel.trans (· = ·) |>.trans _ _ _

Premises used: IsTrans.trans, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
⊢ Equivalence.{u + 1} (α := WSeq α) Equiv

Tactic:
⟨@Equiv.refl _, @Equiv.symm _, @Equiv.trans _⟩

Premises used: Stream'.WSeq.Equiv.refl, Stream'.WSeq.Equiv.symm, Equivalence.mk, Stream'.WSeq.Equiv.trans
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
⊢ s ~ʷ t → Computation.LiftRel (BisimO fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) s.destruct t.destruct

Tactic:
liftRel_destruct

Premises used: Stream'.WSeq.liftRel_destruct, Stream'.WSeq.BisimO, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
⊢ s ~ʷ t ↔ Computation.LiftRel (BisimO fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) s.destruct t.destruct

Tactic:
liftRel_destruct_iff

Premises used: Stream'.WSeq.BisimO, Stream'.WSeq.liftRel_destruct_iff, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
simp :
  Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop (n + 1)).destruct (t.drop (n + 1)).destruct

Tactic:
simp only [drop, destruct_tail]

Premises used: Stream'.WSeq.drop, Stream'.WSeq.destruct_tail
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop n).destruct (t.drop n).destruct
h2 :
  ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)
R₁ : Option (α × WSeq α) → Option (β × WSeq β) → Prop
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)

Tactic:
apply liftRel_bind

Premises used: Computation.liftRel_bind
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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).destruct (t.drop n).destruct

Tactic:
apply liftRel_dropn_destruct H n
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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
h : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux none) (tail.aux none)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
H : LiftRel R s_1 t_1
n : ℕ
a_1 : Option (α × WSeq α)
b_1 : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a_1 b_1
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:
simpa [tail.aux] using liftRel_destruct h2

Premises used: Stream'.WSeq.tail.aux, Stream'.WSeq.liftRel_destruct
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)

Tactic:
exact fun {a b} o =>
      match a, b, o with
      | none, none, _ => by simp
      | some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h : a ∈ s
let : ∀ (n : ℕ) (h : some a ∈ s.get? n), ∃ b ∈ t, R a b
⊢ ∃ b ∈ t, R a b

Tactic:
let ⟨n, h⟩ := exists_get?_of_mem h