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

Tactic:
have h2 := liftRel_destruct h2

Result:
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
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct

Proof state:
case intro.intro.intro.intro.none.some.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
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
cases t2

Result:
no goals

Proof state:
case intro.intro.intro.intro.some.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
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some a) none

Tactic:
cases a

Result:
case intro.intro.intro.intro.some.none.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
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

Proof state:
case intro.intro.intro.intro.some.some.mk.some.mk.mk.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 : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Tactic:
obtain ⟨bc, tu⟩ := t2

Result:
case intro.intro.intro.intro.some.some.mk.some.mk.mk.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 : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Proof state:
case intro.intro.intro.intro.some.none.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
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

Tactic:
cases t1

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
H : Transitive R
s t u : WSeq α
h1 : LiftRel R s t
h2 : LiftRel R t u
⊢ 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 => ?_⟩

Result:
α : Type u
R : α → α → Prop
H : Transitive R
s✝ t u✝ : WSeq α
h1 : LiftRel R s✝ t
h2 : LiftRel R t u✝
s u : WSeq α
h : (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s u
⊢ Computation.LiftRel (LiftRelO R fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct

Proof state:
case intro.intro.intro.intro.none.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
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 => ∃ t, LiftRel R s t ∧ LiftRel R t u) none (some c)

Tactic:
cases t1

Result:
no goals

Proof state:
case intro.intro.intro.intro.some.some.mk.some.mk.mk.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 : α
s : WSeq α
ha : some (a, s) ∈ s✝.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t✝.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u✝.destruct
ab : R a b
st : LiftRel R s t
bc : R b c
tu : LiftRel R t u
⊢ LiftRelO R (fun s u => ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))

Tactic:
exact ⟨H ab bc, t, st, tu⟩

Result:
no goals