-- Mathlib/Data/Seq/WSeq.lean
theorem join_append (S T : WSeq (WSeq α)) : join (append S T) ~ʷ append (join S) (join T)

Proof state:
α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join = nil.append (S.append T).join

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ Computation.LiftRel
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    s1.destruct s2.destruct

Tactic:
apply
  liftRel_rec
    (fun c1 c2 =>
      ∃ (s : WSeq α) (S T : _),
        c1 = destruct (append s (join (append S T))) ∧
          c2 = destruct (append s (append (join S) (join T))))
    _ _ _
    (let ⟨s, S, T, h1, h2⟩ := h
    ⟨s, S, T, congr_arg destruct h1, congr_arg destruct h2⟩)

Result:
α : Type u
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
        ca cb →
      LiftRelAux
        (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
          ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
        (fun c1 c2 =>
          ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
        ca.destruct cb.destruct

Proof state:
case intro.intro.intro.intro.h1.h1.h3
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ ∃ s S T_1,
    T.join.destruct = (s.append (S.append T_1).join).destruct ∧
      T.join.destruct = (s.append (S.join.append T_1.join)).destruct

Tactic:
refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp

Result:
no goals

Proof state:
α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join ~ʷ S.join.append T.join

Tactic:
refine
  ⟨fun s1 s2 =>
    ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T)),
    ⟨nil, S, T, by simp, by simp⟩, ?_⟩

Result:
α : Type u
S T : WSeq (WSeq α)
⊢ ∀ {s t : WSeq α},
    (fun s1 s2 => ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)) s t →
      Computation.LiftRel
        (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
          ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
        s.destruct t.destruct

Proof state:
α : Type u
S T : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
        ca cb →
      LiftRelAux
        (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
          ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
        (fun c1 c2 =>
          ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
        ca.destruct cb.destruct

Tactic:
rintro c1 c2 ⟨s, S, T, rfl, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
S T : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (s.append (S.append T).join).destruct.destruct (s.append (S.join.append T.join)).destruct.destruct

Proof state:
case intro.intro.intro.intro.h1.h2
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 T_1,
    (s.append (S.append T).join).destruct = (s_1.append (S_1.append T_1).join).destruct ∧
      (s.append (S.join.append T.join)).destruct = (s_1.append (S_1.join.append T_1.join)).destruct

Tactic:
exact ⟨s, S, T, rfl, rfl⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.h1.h1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    T.join.destruct.destruct T.join.destruct.destruct

Tactic:
induction' T using WSeq.recOn with s T T <;> simp

Result:
case intro.intro.intro.intro.h1.h1.h2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ ∃ s_1 S T_1,
    (s.append T.join).destruct = (s_1.append (S.append T_1).join).destruct ∧
      (s.append T.join).destruct = (s_1.append (S.join.append T_1.join)).destruct

case intro.intro.intro.intro.h1.h1.h3
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ ∃ s S T_1,
    T.join.destruct = (s.append (S.append T_1).join).destruct ∧
      T.join.destruct = (s.append (S.join.append T_1.join)).destruct

Proof state:
case intro.intro.intro.intro.h1
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
S T : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    (S.append T).join.destruct.destruct (S.join.append T.join).destruct.destruct

Tactic:
induction' S using WSeq.recOn with s S S <;> simp

Result:
case intro.intro.intro.intro.h1.h1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 => ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    T.join.destruct.destruct T.join.destruct.destruct

case intro.intro.intro.intro.h1.h2
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1 T_1,
    (s.append (S.append T).join).destruct = (s_1.append (S_1.append T_1).join).destruct ∧
      (s.append (S.join.append T.join)).destruct = (s_1.append (S_1.join.append T_1.join)).destruct

case intro.intro.intro.intro.h1.h3
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ ∃ s S_1 T_1,
    (S.append T).join.destruct = (s.append (S_1.append T_1).join).destruct ∧
      (S.join.append T.join).destruct = (s.append (S_1.join.append T_1.join)).destruct