awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
h :
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none y
h₁ :
  ∀ (hx : β) (jx : WSeq β),
    Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
        y =
      LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) y
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) x y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) x y

Tactic:
rcases x with ⟨⟩ | ⟨hx, jx⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
h :
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none none =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none none
h₁ :
  ∀ (hy : α) (jy : WSeq α),
    Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none
        (some (hy, jy)) =
      LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none (some (hy, jy))
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none y

Tactic:
rcases y with ⟨⟩ | ⟨hy, jy⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
h :
  Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
      none =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) none
h₁ :
  ∀ (hy : α) (jy : WSeq α),
    Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
        (some (hy, jy)) =
      LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) (some (hy, jy))
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx)) y =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) y

Tactic:
rcases y with ⟨⟩ | ⟨hy, jy⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none none =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none none

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hy : α
jy : WSeq α
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) none
      (some (hy, jy)) =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) none (some (hy, jy))

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
      none =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) none

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
hy : α
jy : WSeq α
⊢ Function.swap (φ := fun (x : Option (α × WSeq α)) (y : Option (β × WSeq β)) ↦ Prop) (LiftRelO R C) (some (hx, jx))
      (some (hy, jy)) =
    LiftRelO (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (Function.swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) C) (some (hx, jx)) (some (hy, jy))

Tactic:
rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
R S : WSeq α → WSeq α → Prop
H : ∀ (s t : WSeq α), R s t → S s t
o p : Option (α × WSeq α)
⊢ BisimO R o p → BisimO S o p

Tactic:
LiftRelO.imp_right _ H

Premises used: Stream'.WSeq.BisimO, Stream'.WSeq.LiftRelO.imp_right
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R_1 : α → β → 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_1 R) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R_1 (LiftRel R_1)) s.destruct t.destruct

Tactic:
Computation.LiftRel.imp ?_ _ _ (h2 h1)

Premises used: Computation.LiftRel.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R_1 : α → β → 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_1 R) s.destruct t.destruct
refine : ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R_1 R a b → LiftRelO R_1 (LiftRel R_1) a b
⊢ Computation.LiftRel (LiftRelO R_1 (LiftRel R_1)) s.destruct t.destruct

Tactic:
refine Computation.LiftRel.imp ?_ _ _ (h2 h1)

Premises used: Computation.LiftRel.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R_1 : α → β → 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_1 R) s.destruct t.destruct
H : ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R_1 s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R_1 R a b → LiftRelO R_1 (LiftRel R_1) 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_1 : α → β → 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_1 R) s.destruct t.destruct
⊢ ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R_1 s t

Tactic:
fun s' t' h' => ⟨R, h', @h2⟩

Premises used: Stream'.WSeq.LiftRel, And.intro, Exists.intro
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R_1 : α → β → 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_1 R) s.destruct t.destruct
⊢ ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R_1 s t

Tactic:
exact fun s' t' h' => ⟨R, h', @h2⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
inl : ∀ (h : LiftRel R s t), Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
inr :
  ∀ (h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct),
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
obtain h | h := h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
liftRel_destruct h

Premises used: Stream'.WSeq.liftRel_destruct
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
exact liftRel_destruct h

Premises used: Stream'.WSeq.liftRel_destruct
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
assumption
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h :
  (fun (s : WSeq α) (t : WSeq β) ↦ 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:
have h : Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t) := by
        obtain h | h := h
        · exact liftRel_destruct h
        · assumption
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h_2 :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
apply :
  ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R
        (fun (s : WSeq α) (t : WSeq β) ↦
          LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
        a b
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
    s.destruct t.destruct

Tactic:
apply Computation.LiftRel.imp _ _ _ h

Premises used: Computation.LiftRel.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s : WSeq α
t : WSeq β
h_2 :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s
    t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
H :
  ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R
        (fun (s : WSeq α) (t : WSeq β) ↦
          LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
        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
s_1 : WSeq α
t_1 : WSeq β
h_1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_1.destruct t_1.destruct
s_2 : WSeq α
t_2 : WSeq β
h_2 :
  (fun (s : WSeq α) (t : WSeq β) ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct)
    s_2 t_2
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
apply Or.inl

Premises used: Or.inl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
⊢ LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) s2 s1

Tactic:
⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => ?_⟩

Premises used: Function.swap, Stream'.WSeq.LiftRel, And.intro, Exists.intro
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h : LiftRel R s1 s2
refine :
  ∀ {s : WSeq β} {t : WSeq α} (h : LiftRel R t s),
    Computation.LiftRel
      (LiftRelO (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
        (swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) (LiftRel R)))
      s.destruct t.destruct
⊢ LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) s2 s1

Tactic:
refine ⟨swap (LiftRel R), h, fun {s t} (h : LiftRel R t s) => ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h_1 : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
rw : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct
⊢ Computation.LiftRel
    (LiftRelO (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) (LiftRel R)))
    s.destruct t.destruct

Tactic:
rw [← LiftRelO.swap, Computation.LiftRel.swap]

Premises used: Computation.LiftRel.swap, Stream'.WSeq.LiftRelO.swap
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h_1 : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct

Tactic:
apply liftRel_destruct h

Premises used: Stream'.WSeq.liftRel_destruct
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
⊢ Function.swap (φ := fun (x : WSeq α) (y : WSeq β) ↦ Prop) (LiftRel R) =
    LiftRel (Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)

Tactic:
funext fun _ => funext fun _ => propext ⟨LiftRel.swap_lem, LiftRel.swap_lem⟩

Premises used: funext, Iff.intro, propext, Stream'.WSeq.LiftRel.swap_lem
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
a : Option (α × WSeq α)
none : LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) Option.none Option.none
some : ∀ (a : α × WSeq α), LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (Option.some a) (Option.some a)
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) a a

Tactic:
rcases a with - | a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) none none

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
a : α × WSeq α
some :
  ∀ (fst : α) (snd : WSeq α),
    LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (Option.some (fst, snd)) (Option.some (fst, snd))
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (Option.some a) (Option.some a)

Tactic:
cases a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
fst : α
snd : WSeq α
some : R fst fst
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (Option.some (fst, snd)) (Option.some (fst, snd))

Tactic:
simp only [LiftRelO, and_true]

Premises used: and_true, Stream'.WSeq.LiftRelO
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
fst : α
snd : WSeq α
⊢ R fst fst

Tactic:
apply refl_of R

Premises used: refl_of
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
s : WSeq α
⊢ LiftRel R s s

Tactic:
⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩

Premises used: Stream'.WSeq.LiftRel, And.intro, Exists.intro, Eq, rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
s : WSeq α
refine :
  ∀ {s t : WSeq α} (h : s = t), Computation.LiftRel (LiftRelO R fun (x1 x2 : WSeq α) ↦ x1 = x2) s.destruct t.destruct
⊢ LiftRel R s s

Tactic:
refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
s_1 s t : WSeq α
h : s = t
rw : Computation.LiftRel (LiftRelO R fun (x1 x2 : WSeq α) ↦ x1 = x2) s.destruct s.destruct
⊢ Computation.LiftRel (LiftRelO R fun (x1 x2 : WSeq α) ↦ x1 = x2) s.destruct t.destruct

Tactic:
rw [← h]
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
s_1 s t : WSeq α
h : s = t
⊢ Computation.LiftRel (LiftRelO R fun (x1 x2 : WSeq α) ↦ x1 = x2) s.destruct s.destruct

Tactic:
apply Computation.LiftRel.refl _ |>.refl

Premises used: Std.Refl.refl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
R : α → α → Prop
H : Symmetric R
s1 s2 : WSeq α
h : Function.swap (φ := fun (x y : WSeq α) ↦ Prop) (LiftRel R) s2 s1
rwa : ∀ (h : LiftRel (Function.swap (φ := fun (a a_1 : α) ↦ Prop) R) s2 s1), LiftRel R s2 s1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : LiftRel R s2 s1), LiftRel R s2 s1
⊢ LiftRel R s2 s1

Tactic:
rwa [LiftRel.swap, H.swap_eq] at h

Premises used: Stream'.WSeq.LiftRel.swap, Symmetric.swap_eq
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
⊢ IsTrans (WSeq α) (LiftRel R)

Tactic:
⟨fun s t u h1 h2 ↦ ?_⟩

Premises used: IsTrans.mk
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
refine : ∀ (s t u : WSeq α) (h1 : LiftRel R s t) (h2 : LiftRel R t u), LiftRel R s u
⊢ IsTrans (WSeq α) (LiftRel R)

Tactic:
refine ⟨fun s t u h1 h2 ↦ ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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
⊢ LiftRel R s u

Tactic:
⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩

Premises used: Exists, Stream'.WSeq.LiftRel, And, And.intro, Exists.intro
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : 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
refine :
  ∀ {s u : WSeq α} (h : (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s u),
    Computation.LiftRel (LiftRelO R fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
      u.destruct
⊢ LiftRel R s u

Tactic:
refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t u_1 : WSeq α
h1 : LiftRel R s_1 t
h2 : LiftRel R t u_1
s u : WSeq α
h : (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s u
rcases :
  ∀ (t : WSeq α) (h1 : LiftRel R s t) (h2 : LiftRel R t u),
    Computation.LiftRel (LiftRelO R fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
      u.destruct
⊢ Computation.LiftRel (LiftRelO R fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
    u.destruct

Tactic:
rcases h with ⟨t, h1, h2⟩
-- 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 : LiftRel R s t
h2 : LiftRel R t u
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
have h1 := liftRel_destruct h1
-- 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 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct

Tactic:
have h2 := liftRel_destruct h2
-- 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
⊢ Computation.LiftRel (LiftRelO R fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
    u.destruct

Tactic:
Computation.liftRel_def.2
      ⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2),
        fun {a c} ha hc => ?_⟩

Premises used: Iff.mpr, And.intro, Iff.trans, Computation.terminates_of_liftRel, Computation.liftRel_def
-- 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
fun :
  ∀ {a c : Option (α × WSeq α)} (ha : a ∈ s.destruct) (hc : c ∈ u.destruct),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c
⊢ Computation.LiftRel (LiftRelO R fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
    u.destruct

Tactic:
refine
    Computation.liftRel_def.2
      ⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2),
        fun {a c} ha hc => ?_⟩

Premises used: Iff.mpr, And.intro, Iff.trans, Computation.terminates_of_liftRel, Computation.liftRel_def
-- 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
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
rcases :
  ∀ (b : Option (α × WSeq α)) (hb : b ∈ t.destruct) (t1 : LiftRelO R (LiftRel R) a b),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c

Tactic:
rcases h1.left ha with ⟨b, hb, t1⟩

Premises used: And.left
-- 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
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t1 : LiftRelO R (LiftRel R) a b
⊢ LiftRelO R (LiftRel R) b c

Tactic:
have t2 := Computation.rel_of_liftRel h2 hb hc
-- 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
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
t1 : LiftRelO R (LiftRel R) a b
t2 : LiftRelO R (LiftRel R) b c
none :
  ∀ (ha : Option.none ∈ s.destruct) (t1 : LiftRelO R (LiftRel R) Option.none b),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none c
some :
  ∀ (a : α × WSeq α) (ha : Option.some a ∈ s.destruct) (t1 : LiftRelO R (LiftRel R) (Option.some a) b),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) c
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c

Tactic:
obtain - | a := a