-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_join.lem (R : α → β → Prop) {S T} {U : WSeq α → WSeq β → Prop}
    (ST : LiftRel (LiftRel R) S T)
    (HU :
      ∀ s1 s2,
        (∃ s t S T,
            s1 = append s (join S) ∧
              s2 = append t (join T) ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) →
          U s1 s2)
    {a} (ma : a ∈ destruct (join S)) : ∃ b, b ∈ destruct (join T) ∧ LiftRelO R U a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
        LiftRel (LiftRel R) S T →
          ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝ : S.destruct.Results (some (s, S')) m
rs2 : (destruct_join.aux (some (s, S'))).Results a k
mT : some (t, T') ∈ T.destruct
⊢ ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b

Tactic:
simp only [destruct_join.aux, destruct_append] at rs2

Result:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
        LiftRel (LiftRel R) S T →
          ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝ : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
⊢ ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b

Proof state:
case refine_1
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
        LiftRel (LiftRel R) S T →
          ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a✝ : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a✝ n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a✝ k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝¹ : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a✝ k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a✝ k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5✝ : (destruct_append.aux S'.join o').Results a✝ n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
x✝ : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a✝ n1
mt : some (b, t') ∈ t.destruct
⊢ some (b, t'.append T'.join) ∈ (t.destruct.bind (destruct_append.aux T'.join)).think

Tactic:
apply think_mem

Result:
case refine_1.a
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
        LiftRel (LiftRel R) S T →
          ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a✝ : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a✝ n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a✝ k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝¹ : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a✝ k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a✝ k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5✝ : (destruct_append.aux S'.join o').Results a✝ n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
x✝ : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a✝ n1
mt : some (b, t') ∈ t.destruct
⊢ some (b, t'.append T'.join) ∈ t.destruct.bind (destruct_append.aux T'.join)

Proof state:
case refine_1.a
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ (m : ℕ),
    m < n →
      ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
        LiftRel (LiftRel R) S T →
          ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b, b ∈ T.join.destruct ∧ LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a✝ : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a✝ n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a✝ k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
x✝¹ : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a✝ k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a✝ k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5✝ : (destruct_append.aux S'.join o').Results a✝ n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt✝ : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
x✝ : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a✝ n1
mt : some (b, t') ∈ t.destruct
⊢ some (b, t'.append T'.join) ∈ destruct_append.aux T'.join (some (b, t'))

Tactic:
apply ret_mem

Result:
no goals