awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
S 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)
T : WSeq (WSeq α)
nil :
  LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (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)
    (Computation.destruct (destruct (join WSeq.nil))) (Computation.destruct (destruct (join WSeq.nil)))
nil₁ :
  ∀ (s : WSeq α) (T : 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)
      (cons s T).join.destruct.destruct (cons s T).join.destruct.destruct
nil₂ :
  ∀ (T : 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)
      T.think.join.destruct.destruct T.think.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)
    T.join.destruct.destruct T.join.destruct.destruct

Tactic:
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

Premises used: Computation.liftRelAux_inr_inr, Stream'.WSeq.cons, Stream'.WSeq.join_think, Stream'.WSeq.join_cons, Stream'.WSeq.think, Computation.destruct_think, Stream'.WSeq.nil, Stream'.WSeq.destruct_think
-- Module: Mathlib.Data.WSeq.Relation
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)
T : WSeq (WSeq α)
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 nil ((cons s S).append T).join).destruct.destruct
    (append nil ((cons s S).join.append T.join)).destruct.destruct

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
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)
T 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 nil (S.think.append T).join).destruct.destruct (append nil (S.think.join.append T.join)).destruct.destruct

Tactic:
⟨nil, S, T, ?_, ?_⟩

Premises used: Computation.LiftRelAux, And.intro, Exists.intro, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Relation
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)
T S : WSeq (WSeq α)
nil : (append WSeq.nil (S.think.append T).join).destruct.tail = (append WSeq.nil (S.append T).join).destruct
nil₁ : (append WSeq.nil (S.think.join.append T.join)).destruct.tail = (append WSeq.nil (S.join.append T.join)).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.think.append T).join).destruct.destruct
    (append WSeq.nil (S.think.join.append T.join)).destruct.destruct

Tactic:
refine ⟨nil, S, T, ?_, ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
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)
T S : WSeq (WSeq α)
⊢ (append nil (S.think.append T).join).destruct.tail = (append nil (S.append T).join).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
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)
T S : WSeq (WSeq α)
⊢ (append nil (S.think.join.append T.join)).destruct.tail = (append nil (S.join.append T.join)).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
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 α)
a : α
s : 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)
    ((cons a s).append (S.append T).join).destruct.destruct ((cons a s).append (S.join.append T.join)).destruct.destruct

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
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 α)
s : 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)
    (s.think.append (S.append T).join).destruct.destruct (s.think.append (S.join.append T.join)).destruct.destruct

Tactic:
simpa using ⟨s, S, T, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
rw : (map ret (map f s)).join ~ʷ map f s
⊢ (map (ret ∘ f) s).join ~ʷ map f s

Tactic:
rw [map_comp]

Premises used: Stream'.WSeq.map_comp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map ret (map f s)).join ~ʷ map f s

Tactic:
apply join_map_ret

Premises used: Stream'.WSeq.join_map_ret
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
a : α
f : α → WSeq β
⊢ (ret a).bind f ~ʷ f a

Tactic:
simp [bind]

Premises used: Stream'.WSeq.bind
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join = append nil (append nil SS.join).join

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS).join = append nil (append (join nil) (map join SS).join)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 :
  ∀ {s t : WSeq α},
    (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))
        s t →
      Computation.LiftRel
        (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))
        s.destruct t.destruct
⊢ SS.join.join ~ʷ (map join SS).join

Tactic:
refine
    ⟨fun s1 s2 =>
      ∃ s S SS,
        s1 = append s (join (append S (join SS))) ∧
          s2 = append s (append (join S) (join (map join SS))),
      ⟨nil, nil, SS, by simp, by simp⟩, ?_⟩
-- 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)
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]
-- 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)
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)
⊢ s2.destruct = (s.append (S.join.append (map join SS).join)).destruct

Tactic:
simp [h2]
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS : 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 :
  ∀ {ca cb : Computation (Option (α × WSeq α))},
    (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)
        ca cb →
      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)
        ca.destruct cb.destruct
⊢ Computation.LiftRel
    (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))
    s1.destruct s2.destruct

Tactic:
apply
    liftRel_rec
      (fun c1 c2 =>
        ∃ s S SS,
          c1 = destruct (append s (join (append S (join SS)))) ∧
            c2 = destruct (append s (append (join S) (join (map join SS)))))
      _ (destruct s1) (destruct s2)
      (let ⟨s, S, SS, h1, h2⟩ := h
      ⟨s, S, SS, by simp [h1], by simp [h2]⟩)

Premises used: Stream'.WSeq.join, Stream'.WSeq.destruct, Exists, And, And.intro, Stream'.WSeq.map, Exists.intro, Computation.liftRel_rec, _private.0.Stream'.WSeq.join_join.match_1, Eq, Stream'.WSeq.append
-- 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 α))
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)
    SS.join.join.destruct.destruct (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)
    (append WSeq.nil (append WSeq.nil SS.join).join).destruct.destruct
    (append WSeq.nil (append (join WSeq.nil) (map join SS).join)).destruct.destruct

Tactic:
simp only [nil_append, join_nil]

Premises used: Stream'.WSeq.nil_append, Stream'.WSeq.join_nil
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS : 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 α))
⊢ LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (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)
    (Computation.destruct (destruct (join (join nil)))) (Computation.destruct (destruct (join (map join nil))))

Tactic:
simp
-- 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 (WSeq α)
SS : WSeq (WSeq (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)
    (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct

Tactic:
⟨nil, S, SS, ?_, ?_⟩

Premises used: Computation.LiftRelAux, And.intro, Exists.intro, Stream'.WSeq.nil
-- 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
nil : (cons S SS).join.join.destruct.tail = (append WSeq.nil (S.append SS.join).join).destruct
nil₁ : (map join (cons S SS)).join.destruct.tail = (append WSeq.nil (S.join.append (map join SS).join)).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)
    (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct

Tactic:
refine ⟨nil, S, SS, ?_, ?_⟩
-- 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (cons S SS).join.join.destruct.tail = (append nil (S.append SS.join).join).destruct

Tactic:
simp
-- 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 (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (map join (cons S SS)).join.destruct.tail = (append nil (S.join.append (map join SS).join)).destruct

Tactic:
simp
-- 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 α))
SS : WSeq (WSeq (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)
    SS.think.join.join.destruct.destruct (map join SS.think).join.destruct.destruct

Tactic:
⟨nil, nil, SS, ?_, ?_⟩

Premises used: Computation.LiftRelAux, And.intro, Exists.intro, Stream'.WSeq.nil
-- 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 α))
SS : WSeq (WSeq (WSeq α))
nil : SS.think.join.join.destruct.tail = (append WSeq.nil (append WSeq.nil SS.join).join).destruct
nil₁ : (map join SS.think).join.destruct.tail = (append WSeq.nil (append (join WSeq.nil) (map join SS).join)).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)
    SS.think.join.join.destruct.destruct (map join SS.think).join.destruct.destruct

Tactic:
refine ⟨nil, nil, SS, ?_, ?_⟩
-- 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 α))
SS : WSeq (WSeq (WSeq α))
⊢ SS.think.join.join.destruct.tail = (append nil (append nil SS.join).join).destruct

Tactic:
simp
-- 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 α))
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS.think).join.destruct.tail = (append nil (append (join nil) (map join SS).join)).destruct

Tactic:
simp