-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
nil :
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil (S.append SS.join).join).destruct.destruct
    (append WSeq.nil (S.join.append (map join SS).join)).destruct.destruct
cons :
  ∀ (a : α) (s : WSeq α),
    LiftRelAux
      (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          c1 = (s.append (S.append SS.join).join).destruct ∧
            c2 = (s.append (S.join.append (map join SS).join)).destruct)
      ((WSeq.cons a s).append (S.append SS.join).join).destruct.destruct
      ((WSeq.cons a s).append (S.join.append (map join SS).join)).destruct.destruct
think :
  ∀ (s : WSeq α),
    LiftRelAux
      (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          c1 = (s.append (S.append SS.join).join).destruct ∧
            c2 = (s.append (S.join.append (map join SS).join)).destruct)
      (s.think.append (S.append SS.join).join).destruct.destruct
      (s.think.append (S.join.append (map join SS).join)).destruct.destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (s.append (S.append SS.join).join).destruct.destruct (s.append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
induction s using WSeq.recOn with
      | nil =>
        induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
      | cons a s => simpa using ⟨s, S, SS, rfl, rfl⟩
      | think s => simpa using ⟨s, S, SS, rfl, rfl⟩

Premises used: Stream'.WSeq.cons, Stream'.WSeq.nil_append, Stream'.WSeq.think, Stream'.WSeq.nil, Stream'.WSeq.join_nil