awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
let : ∀ (s' : WSeq α) (sd : some (a, s') ∈ (s.drop n).destruct), ∃ b ∈ t, R a b
⊢ ∃ b ∈ t, R a b

Tactic:
let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
let : ∀ (b : β) (t' : WSeq β) (td : some (b, t') ∈ (t.drop n).destruct) (ab : R a b), LiftRel R s' t' → ∃ b ∈ t, R a b
⊢ ∃ b ∈ t, R a b

Tactic:
let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
b : β
t' : WSeq β
td : some (b, t') ∈ (t.drop n).destruct
ab : R a b
right : LiftRel R s' t'
⊢ ∃ b ∈ t, R a b

Tactic:
⟨b, get?_mem (Computation.mem_map (Prod.fst.{v, v} <$> ·) td), ab⟩

Premises used: Stream'.WSeq.get?_mem, Prod.fst, And.intro, Exists.intro, Computation.mem_map, Functor.map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
b : β
t' : WSeq β
td : some (b, t') ∈ (t.drop n).destruct
ab : R a b
right : LiftRel R s' t'
⊢ ∃ b ∈ t, R a b

Tactic:
exact ⟨b, get?_mem (Computation.mem_map (Prod.fst.{v, v} <$> ·) td), ab⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
b : β
h : b ∈ t
rw :
  ∀ (H : swap (φ := fun (x : WSeq β) (y : WSeq α) ↦ Prop) (LiftRel fun (x : β) (y : α) ↦ R y x) s t) {b : β}
    (h : b ∈ t), ∃ a ∈ s, R a b
⊢ ∃ a ∈ s, R a b

Tactic:
rw [← LiftRel.swap] at H

Premises used: Stream'.WSeq.LiftRel.swap
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : swap (φ := fun (x : WSeq β) (y : WSeq α) ↦ Prop) (LiftRel fun (x : β) (y : α) ↦ R y x) s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b

Tactic:
exists_of_liftRel_left H h

Premises used: Stream'.WSeq.exists_of_liftRel_left
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : swap (φ := fun (x : WSeq β) (y : WSeq α) ↦ Prop) (LiftRel fun (x : β) (y : α) ↦ R y x) s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b

Tactic:
exact exists_of_liftRel_left H h

Premises used: Stream'.WSeq.exists_of_liftRel_left
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
⊢ LiftRel R nil nil

Tactic:
simp [liftRel_destruct_iff]

Premises used: Stream'.WSeq.liftRel_destruct_iff
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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:
simp [liftRel_destruct_iff]

Premises used: Stream'.WSeq.liftRel_destruct_iff
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
rw :
  Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ LiftRel R s.think t ↔ LiftRel R s t

Tactic:
rw [liftRel_destruct_iff, liftRel_destruct_iff]

Premises used: Stream'.WSeq.liftRel_destruct_iff
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ LiftRel (fun (x1 x2 : α) ↦ x1 = x2) (cons a s) (cons a t)

Tactic:
simpa using h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s : WSeq α
⊢ LiftRel (fun (x1 x2 : α) ↦ x1 = x2) s.think s

Tactic:
simpa using Equiv.refl _

Premises used: Stream'.WSeq.Equiv.refl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ LiftRel (fun (x1 x2 : α) ↦ x1 = x2) s.think t.think

Tactic:
simpa using h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
suffices : ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ s.head → o ∈ t.head
⊢ ∀ {s t : WSeq α}, s ~ʷ t → s.head ~ t.head

Tactic:
suffices ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o}, o ∈ head s → o ∈ head t from fun s t h o =>
    ⟨this h, this h.symm⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
rcases : ∀ (ds : Option (α × WSeq α)) (dsm : ds ∈ s.destruct) (dse : Prod.fst <$> ds = o), o ∈ t.head
⊢ o ∈ t.head

Tactic:
rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩

Premises used: Computation.exists_of_mem_map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
rw : Prod.fst <$> ds ∈ t.head
⊢ o ∈ t.head

Tactic:
rw [← dse]
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
⊢ ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b

Tactic:
obtain ⟨l, r⟩ := destruct_congr h

Premises used: Stream'.WSeq.destruct_congr
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
⊢ ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b

Tactic:
obtain ⟨l, r⟩ := destruct_congr h

Premises used: Stream'.WSeq.destruct_congr
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
rcases :
  ∀ (dt : Option (α × WSeq α)) (dtm : dt ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) ds dt),
    Prod.fst <$> ds ∈ t.head
⊢ Prod.fst <$> ds ∈ t.head

Tactic:
rcases l dsm with ⟨dt, dtm, dst⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) ds dt
none :
  ∀ (dsm : Option.none ∈ s.destruct) (dse : Functor.map (α := α × WSeq α) Prod.fst Option.none = o)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none dt),
    Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
some :
  ∀ (a : α × WSeq α) (dsm : Option.some a ∈ s.destruct) (dse : Prod.fst <$> Option.some a = o)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) dt), Prod.fst <$> Option.some a ∈ t.head
⊢ Prod.fst <$> ds ∈ t.head

Tactic:
rcases ds with - | a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dsm : Option.none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst Option.none = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none dt
none :
  ∀ (dtm : Option.none ∈ t.destruct)
    (dst : BisimO.{u} (α := α) (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none Option.none),
    Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
none₁ :
  ∀ (b : α × WSeq α) (dtm : some b ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none (some b)),
    Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
⊢ Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head

Tactic:
rcases dt with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
a : α × WSeq α
dsm : Option.some a ∈ s.destruct
dse : Prod.fst <$> Option.some a = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) dt
some :
  ∀ (dtm : none ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) none),
    Prod.fst <$> Option.some a ∈ t.head
some₁ :
  ∀ (b : α × WSeq α) (dtm : Option.some b ∈ t.destruct)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) (Option.some b)),
    Prod.fst <$> Option.some a ∈ t.head
⊢ Prod.fst <$> Option.some a ∈ t.head

Tactic:
rcases dt with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst none = o
dtm : none ∈ t.destruct
dst : BisimO.{u} (α := α) (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none none
⊢ Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head

Tactic:
apply Computation.mem_map _ dtm

Premises used: Computation.mem_map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dsm : Option.none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst Option.none = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none (some b)
none :
  ∀ (fst : α) (snd : WSeq α) (dtm : some (fst, snd) ∈ t.destruct)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none (some (fst, snd))),
    Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
⊢ Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head

Tactic:
cases b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst none = o
fst : α
snd : WSeq α
dtm : some (fst, snd) ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none (some (fst, snd))
⊢ Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head

Tactic:
cases dst
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : Option.some a ∈ s.destruct
dse : Prod.fst <$> Option.some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) none
some :
  ∀ (fst : α) (snd : WSeq α) (dsm : Option.some (fst, snd) ∈ s.destruct) (dse : Prod.fst <$> Option.some (fst, snd) = o)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some (fst, snd)) none),
    Prod.fst <$> Option.some (fst, snd) ∈ t.head
⊢ Prod.fst <$> Option.some a ∈ t.head

Tactic:
cases a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dtm : none ∈ t.destruct
fst : α
snd : WSeq α
dsm : some (fst, snd) ∈ s.destruct
dse : Prod.fst <$> some (fst, snd) = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (fst, snd)) none
⊢ Prod.fst <$> some (fst, snd) ∈ t.head

Tactic:
cases dst
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : Option.some a ∈ s.destruct
dse : Prod.fst <$> Option.some a = o
b : α × WSeq α
dtm : Option.some b ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) (Option.some b)
some :
  ∀ (a : α) (s' : WSeq α) (dsm : Option.some (a, s') ∈ s.destruct) (dse : Prod.fst <$> Option.some (a, s') = o)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some (a, s')) (Option.some b)),
    Prod.fst <$> Option.some (a, s') ∈ t.head
⊢ Prod.fst <$> Option.some a ∈ t.head

Tactic:
obtain ⟨a, s'⟩ := a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
b : α × WSeq α
dtm : Option.some b ∈ t.destruct
a : α
s' : WSeq α
dsm : Option.some (a, s') ∈ s.destruct
dse : Prod.fst <$> Option.some (a, s') = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some (a, s')) (Option.some b)
some :
  ∀ (b : α) (t' : WSeq α) (dtm : Option.some (b, t') ∈ t.destruct)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some (a, s')) (Option.some (b, t'))),
    Prod.fst <$> Option.some (a, s') ∈ t.head
⊢ Prod.fst <$> Option.some (a, s') ∈ t.head

Tactic:
obtain ⟨b, t'⟩ := b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : Option.some (a, s') ∈ s.destruct
dse : Prod.fst <$> Option.some (a, s') = o
b : α
t' : WSeq α
dtm : Option.some (b, t') ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some (a, s')) (Option.some (b, t'))
some : Prod.fst <$> Option.some (b, s') ∈ t.head
⊢ Prod.fst <$> Option.some (a, s') ∈ t.head

Tactic:
rw [dst.left]

Premises used: And.left
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ t.head

Tactic:
@Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
      (some (b, t')) (destruct t) dtm

Premises used: Prod.fst, Computation.mem_map, Functor.map, Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ t.head

Tactic:
exact @Computation.mem_map _ _ (@Functor.map _ _ (α × WSeq α) _ Prod.fst)
      (some (b, t')) (destruct t) dtm

Premises used: Prod.fst, Computation.mem_map, Functor.map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
h1 : flatten (Computation.pure s) ~ʷ s
h2 : ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s
⊢ flatten c ~ʷ s

Tactic:
apply Computation.memRecOn h

Premises used: Computation.memRecOn
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s

Tactic:
simp [Equiv.refl]

Premises used: Stream'.WSeq.Equiv.refl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
h2 : flatten s'.think ~ʷ flatten s'
⊢ flatten s' ~ʷ s → flatten s'.think ~ʷ s

Tactic:
apply Equiv.trans

Premises used: Stream'.WSeq.Equiv.trans
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s'.think ~ʷ flatten s'

Tactic:
simp [think_equiv]

Premises used: Stream'.WSeq.think_equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
simp : Computation.LiftRel (LiftRelO R S) (c1 >>= destruct) (c2 >>= destruct)
⊢ Computation.LiftRel (LiftRelO R S) (flatten c1).destruct (flatten c2).destruct

Tactic:
simp only [destruct_flatten]

Premises used: Stream'.WSeq.destruct_flatten
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
apply : ∀ {a : WSeq α} {b : WSeq β}, LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
⊢ Computation.LiftRel (LiftRelO R S) (c1 >>= destruct) (c2 >>= destruct)

Tactic:
apply liftRel_bind _ _ h

Premises used: Computation.liftRel_bind
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
ab : LiftRel R a b
apply : ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R S a b
⊢ Computation.LiftRel (LiftRelO R S) a.destruct b.destruct

Tactic:
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct ab)

Premises used: Stream'.WSeq.liftRel_destruct, Computation.LiftRel.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a_1 : WSeq α
b_1 : WSeq β
ab : LiftRel R a_1 b_1
a : Option (α × WSeq α)
b : Option (β × WSeq β)
H : ∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → S s t
⊢ LiftRelO R (LiftRel R) a b → LiftRelO R S a b

Tactic:
apply LiftRelO.imp_right

Premises used: Stream'.WSeq.LiftRelO.imp_right
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s_1 : WSeq α
t_1 : WSeq β
h_2 : S s_1 t_1
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h_3 : Computation.LiftRel (LiftRel R) c1 c2
a_1 : WSeq α
b_1 : WSeq β
ab : LiftRel R a_1 b_1
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ S s t

Tactic:
⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩

Premises used: Computation.pure, And.intro, Exists.intro
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s_1 : WSeq α
t_1 : WSeq β
h_2 : S s_1 t_1
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h_3 : Computation.LiftRel (LiftRel R) c1 c2
a_1 : WSeq α
b_1 : WSeq β
ab : LiftRel R a_1 b_1
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
H : s = flatten (Computation.pure s)
H₁ : t = flatten (Computation.pure t)
H₂ : Computation.LiftRel (LiftRel R) (Computation.pure s) (Computation.pure t)
⊢ S s t

Tactic:
refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s_1 : WSeq α
t_1 : WSeq β
h_2 : S s_1 t_1
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h_3 : Computation.LiftRel (LiftRel R) c1 c2
a_1 : WSeq α
b_1 : WSeq β
ab : LiftRel R a_1 b_1
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ s = flatten (Computation.pure s)

Tactic:
simp [h]