Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: 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 < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ 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.join.destruct

pp: case refine_2
α : 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 < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ 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
⊢ LiftRelO R U a✝ (some (b, t'.append T'.join))

Tactic:
· simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            apply ret_mem

Goal state after:
case refine_2
α : 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 < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ 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
⊢ LiftRelO R U a✝ (some (b, t'.append T'.join))