-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
S_1 T_1 : WSeq (WSeq α)
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
    s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : WSeq (WSeq α)
nil :
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
        c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (append WSeq.nil (append WSeq.nil T).join).destruct.destruct
    (append WSeq.nil (append (join WSeq.nil) T.join)).destruct.destruct
nil₁ :
  ∀ (s : WSeq α) (S : WSeq (WSeq α)),
    LiftRelAux
      (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
          s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
          c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
      (append WSeq.nil ((cons s S).append T).join).destruct.destruct
      (append WSeq.nil ((cons s S).join.append T.join)).destruct.destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
        c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (append WSeq.nil (S.append T).join).destruct.destruct (append WSeq.nil (S.join.append T.join)).destruct.destruct
have nil₂ : ∀ (S : WSeq (WSeq α)),
  LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
        s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T : WSeq (WSeq α)),
        c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (append WSeq.nil (S.think.append T).join).destruct.destruct
    (append WSeq.nil (S.think.join.append T.join)).destruct.destruct
Tactic: induction S using WSeq.recOn with
    | nil =>
      simp only [nil_append, join_nil]
      induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp
    | cons s S => simpa using ⟨s, S, T, rfl, rfl⟩
    | think S => refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
Cleared hypotheses: S