awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)
      (swap (φ := fun (a : WSeq α) (a_1 : WSeq β) ↦ Prop) (LiftRel R)))
    s.destruct t.destruct
have rw : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct
Tactic: rw [← LiftRelO.swap, Computation.LiftRel.swap]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
a : Option (α × WSeq α)
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) a a
have none : LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) none none
Tactic: rcases a with - | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) a a
have some : ∀ (a : α × WSeq α), LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (some a) (some a)
Tactic: rcases a with - | a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
a : α × WSeq α
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (some a) (some a)
have some : ∀ (fst : α) (snd : WSeq α), LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (some (fst, snd)) (some (fst, snd))
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
fst : α
snd : WSeq α
⊢ LiftRelO R (fun (x1 x2 : WSeq α) ↦ x1 = x2) (some (fst, snd)) (some (fst, snd))
have some : R fst fst
Tactic: simp only [LiftRelO, and_true]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : Std.Refl R
s : WSeq α
⊢ LiftRel R s s
have refine : ∀ {s t : WSeq α} (h : s = t), Computation.LiftRel (LiftRelO R fun (x1 x2 : WSeq α) ↦ x1 = x2) s.destruct t.destruct
Tactic: refine ⟨(· = ·), rfl, fun {s t} (h : s = t) => ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 t.destruct
have rw : Computation.LiftRel (LiftRelO R fun (x1 x2 : WSeq α) ↦ x1 = x2) s.destruct s.destruct
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
R : α → α → Prop
H : Symmetric R
s1 s2 : WSeq α
h : Function.swap (φ := fun (x y : WSeq α) ↦ Prop) (LiftRel R) s2 s1
⊢ LiftRel R s2 s1
have rwa : ∀ (h : LiftRel (Function.swap (φ := fun (a a_1 : α) ↦ Prop) R) s2 s1), LiftRel R s2 s1
Tactic: rwa [LiftRel.swap, H.swap_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRel R s2 s1
have rwa₁ : ∀ (h : LiftRel R s2 s1), LiftRel R s2 s1
Tactic: rwa [LiftRel.swap, H.swap_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
⊢ IsTrans (WSeq α) (LiftRel R)
have refine : ∀ (s t u : WSeq α) (h1 : LiftRel R s t) (h2 : LiftRel R t u), LiftRel R s u
Tactic: refine ⟨fun s t u h1 h2 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
have 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
Tactic: refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ Computation.LiftRel (LiftRelO R fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
    u.destruct
have 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
Tactic: rcases h with ⟨t, h1, h2⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
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 fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
    u.destruct
have h1₁ : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Tactic: have h1 := liftRel_destruct h1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
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 fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) s.destruct
    u.destruct
have h2₁ : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
Tactic: have h2 := liftRel_destruct h2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
have 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
Tactic: refine
    Computation.liftRel_def.2
      ⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2),
        fun {a c} ha hc => ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c
have 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
Tactic: rcases h1.left ha with ⟨b, hb, t1⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
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 (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c
have t2 : LiftRelO R (LiftRel R) b c
Tactic: have t2 := Computation.rel_of_liftRel h2 hb hc
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c
have none : ∀ (ha : none ∈ s.destruct) (t1 : LiftRelO R (LiftRel R) none b),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) none c
Tactic: obtain - | a := a
Cleared hypotheses: a, ha, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) a c
have some : ∀ (a : α × WSeq α) (ha : some a ∈ s.destruct) (t1 : LiftRelO R (LiftRel R) (some a) b),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some a) c
Tactic: obtain - | a := a
Cleared hypotheses: a, ha, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : none ∈ s.destruct
t1 : LiftRelO R (LiftRel R) none b
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) none c
have none : ∀ (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: obtain - | c := c
Cleared hypotheses: c, hc, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none c
have 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)
Tactic: obtain - | c := c
Cleared hypotheses: c, hc, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some a) c
have 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) (some a) none
Tactic: obtain - | c := c
Cleared hypotheses: c, hc, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some a) c
have 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)
Tactic: obtain - | c := c
Cleared hypotheses: c, hc, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
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) none (some c)
have none : ∀ (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 b
Cleared hypotheses: b, hb, t1, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) Option.none (some c)
have 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)
Tactic: cases b
Cleared hypotheses: b, hb, t1, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) 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) (some a) none
have some : ∀ (fst : α) (snd : WSeq α) (ha : some (fst, snd) ∈ s.destruct) (t1 : LiftRelO R (LiftRel R) (some (fst, snd)) b),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (fst, snd)) none
Tactic: cases a
Cleared hypotheses: a, ha, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : some (fst, snd) ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some (fst, snd)) b
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (fst, snd)) none
have some : ∀ (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: rcases b with - | b
Cleared hypotheses: b, hb, t2, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (fst, snd)) none
have 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
Tactic: rcases b with - | b
Cleared hypotheses: b, hb, t2, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) none
t1 : LiftRelO R (LiftRel R) (some (fst, snd)) (some b)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (fst, snd)) none
have some : ∀ (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 b
Cleared hypotheses: b, hb, t2, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : some a ∈ s.destruct
t1 : LiftRelO R (LiftRel R) (some a) b
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) (some a) (some c)
have some : ∀ (a : α) (s_2 : WSeq α) (ha : some (a, s_2) ∈ s.destruct) (t1 : LiftRelO R (LiftRel R) (some (a, s_2)) b),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s_2)) (some c)
Tactic: obtain ⟨a, s⟩ := a
Cleared hypotheses: a, ha, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (some c)
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) b
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
have some : ∀ (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: rcases b with - | b
Cleared hypotheses: b, hb, t2, t1