-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_append (R : α → β → Prop) {s1 s2 : WSeq α} {t1 t2 : WSeq β} (h1 : LiftRel R s1 t1)
    (h2 : LiftRel R s2 t2) : LiftRel R (append s1 s2) (append t1 t2) :=
  ⟨fun s t => LiftRel R s t ∨ ∃ s1 t1, s = append s1 s2 ∧ t = append t1 t2 ∧ LiftRel R s1 t1,
    Or.inr ⟨s1, t1, rfl, rfl, h1⟩, fun {s t} h =>
    match s, t, h with
    | s, t, Or.inl h => by
      apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h)
      intro a b; apply LiftRelO.imp_right
      intro s t; apply Or.inl
    | _, _, Or.inr ⟨s1, t1, rfl, rfl, h⟩ => by
      simp only [LiftRelO, exists_and_left, destruct_append, destruct_append.aux]
      apply Computation.liftRel_bind _ _ (liftRel_destruct h)
      intro o p h
      rcases o with - | a <;> rcases p with - | b
      · simp only [destruct_append.aux]
        apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h2)
        intro a b
        apply LiftRelO.imp_right
        intro s t
        apply Or.inl
      · cases b; cases h
      · cases a; cases h
      · obtain ⟨a, s⟩ := a; obtain ⟨b, t⟩ := b
        obtain ⟨r, h⟩ := h
        -- Porting note: These 2 theorems should be excluded.
        simpa [-liftRel_pure_left, -liftRel_pure_right] using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩⟩

Proof state:
case H
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝¹ t✝¹
s✝ : WSeq α
t✝ : WSeq β
h : LiftRel R s✝ t✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1

Tactic:
apply Or.inl

Result:
no goals

Proof state:
case H
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x

Tactic:
apply Or.inl

Result:
no goals

Proof state:
case H
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1

Tactic:
intro s t

Result:
case H
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝¹ t✝¹
s✝ : WSeq α
t✝ : WSeq β
h : LiftRel R s✝ t✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1

Proof state:
case H
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x

Tactic:
intro s t

Result:
case H
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b

Tactic:
intro a b

Result:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s.destruct
    t.destruct

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

Result:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t => LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x) a b

Tactic:
apply LiftRelO.imp_right

Result:
case H
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t => LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x