-- Mathlib/Data/Seq/WSeq.lean
theorem join_join (SS : WSeq (WSeq (WSeq α))) : join (join SS) ~ʷ join (map join SS)

Proof state:
case h3
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    (s.append (S.append SS.join).join).destruct = (s_1.append (S_1.append SS_1.join).join).destruct ∧
      (s.append (S.join.append (map join SS).join)).destruct =
        (s_1.append (S_1.join.append (map join SS_1).join)).destruct

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

Result:
no goals

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

Tactic:
intro c1 c2 h

Result:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h✝ : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
h :
  ∃ s S SS,
    c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    c1.destruct c2.destruct

Proof state:
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
s : WSeq α
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
h1 : s1 = s.append (S.append SS.join).join
h2 : s2 = s.append (S.join.append (map join SS).join)
⊢ s1.destruct = (s.append (S.append SS.join).join).destruct

Tactic:
simp [h1]

Result:
no goals

Proof state:
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, 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 α))
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 =>
      ∃ s S SS,
        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 a s s <;> simp

Result:
case h1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ LiftRelAux
    (LiftRelO (fun x1 x2 => x1 = x2) fun s1 s2 =>
      ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun c1 c2 =>
      ∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (S.append SS.join).join.destruct.destruct (S.join.append (map join SS).join).destruct.destruct

case h2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
a : α
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    s.append (S.append SS.join).join = s_1.append (S_1.append SS_1.join).join ∧
      s.append (S.join.append (map join SS).join) = s_1.append (S_1.join.append (map join SS_1).join)

case h3
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
s : WSeq α
⊢ ∃ s_1 S_1 SS_1,
    (s.append (S.append SS.join).join).destruct = (s_1.append (S_1.append SS_1.join).join).destruct ∧
      (s.append (S.join.append (map join SS).join)).destruct =
        (s_1.append (S_1.join.append (map join SS_1).join)).destruct

Proof state:
case h1.h1.h3
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S SS_1,
    SS.join.join.destruct = (s.append (S.append SS_1.join).join).destruct ∧
      (map join SS).join.destruct = (s.append (S.join.append (map join SS_1).join)).destruct

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

Result:
no goals

Proof state:
case h1.h3
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ ∃ s S_1 SS_1,
    (S.append SS.join).join.destruct = (s.append (S_1.append SS_1.join).join).destruct ∧
      (S.join.append (map join SS).join).destruct = (s.append (S_1.join.append (map join SS_1).join)).destruct

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

Result:
no goals

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

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

Result:
case h1.h1.h2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S_1 SS_1,
    (S.append SS.join).join.destruct = (s.append (S_1.append SS_1.join).join).destruct ∧
      (S.join.append (map join SS).join).destruct = (s.append (S_1.join.append (map join SS_1).join)).destruct

case h1.h1.h3
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ ∃ s S SS_1,
    SS.join.join.destruct = (s.append (S.append SS_1.join).join).destruct ∧
      (map join SS).join.destruct = (s.append (S.join.append (map join SS_1).join)).destruct

Proof state:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS).join = nil.append (nil.join.append (map join SS).join)

Tactic:
simp

Result:
no goals