-- Mathlib/Data/Seq/WSeq.lean
theorem LiftRel.trans (R : α → α → Prop) (H : Transitive R) : Transitive (LiftRel R) :=
  fun s t u h1 h2 => by
  refine ⟨fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u, ⟨t, h1, h2⟩, fun {s u} h => ?_⟩
  rcases h with ⟨t, h1, h2⟩
  have h1 := liftRel_destruct h1
  have h2 := liftRel_destruct h2
  refine
    Computation.liftRel_def.2
      ⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2),
        fun {a c} ha hc => ?_⟩
  rcases h1.left ha with ⟨b, hb, t1⟩
  have t2 := Computation.rel_of_liftRel h2 hb hc
  obtain - | a := a <;> obtain - | c := c
  · trivial
  · cases b
    · cases t2
    · cases t1
  · cases a
    rcases b with - | b
    · cases t1
    · cases b
      cases t2
  · obtain ⟨a, s⟩ := a
    rcases b with - | b
    · cases t1
    obtain ⟨b, t⟩ := b
    obtain ⟨c, u⟩ := c
    obtain ⟨ab, st⟩ := t1
    obtain ⟨bc, tu⟩ := t2
    exact ⟨H ab bc, t, st, tu⟩

Proof state:
case intro.intro.intro.intro.some.some.mk.some
α : Type u
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
obtain ⟨b, t⟩ := b

Result:
case intro.intro.intro.intro.some.some.mk.some.mk
α : Type u
R : α → α → Prop
H : Transitive R
s✝¹ t✝¹ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝¹
h2✝¹ : LiftRel R t✝¹ u✝
s✝ u t✝ : WSeq α
h1✝ : LiftRel R s✝ t✝
h2✝ : LiftRel R t✝ u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t✝.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Proof state:
case intro.intro.intro.intro.some.none.mk.some.mk
α : Type u
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
hc : none ∈ u.destruct
fst✝¹ : α
snd✝¹ : WSeq α
ha : some (fst✝¹, snd✝¹) ∈ s.destruct
fst✝ : α
snd✝ : WSeq α
hb : some (fst✝, snd✝) ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) none
t1 : LiftRelO R (LiftRel R) (some (fst✝¹, snd✝¹)) (some (fst✝, snd✝))
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝¹, snd✝¹)) none

Tactic:
cases t2

Result:
no goals

Proof state:
case intro.intro.intro.intro.some.some
α : Type u
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) (some c)

Tactic:
obtain ⟨a, s⟩ := a

Result:
case intro.intro.intro.intro.some.some.mk
α : Type u
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
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✝.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Proof state:
case intro.intro
α : Type u
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c

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

Result:
case intro.intro.intro.intro
α : Type u
R : α → α → Prop
H : Transitive R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) a c

Proof state:
case intro.intro.intro.intro.some.some.mk
α : Type u
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
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✝.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) b
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

Tactic:
rcases b with - | b

Result:
case intro.intro.intro.intro.some.some.mk.none
α : Type u
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)

case intro.intro.intro.intro.some.some.mk.some
α : Type u
R : α → α → Prop
H : Transitive R
s✝¹ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝¹ t✝
h2✝¹ : LiftRel R t✝ u✝
s✝ u t : WSeq α
h1✝ : LiftRel R s✝ t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)