awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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
have 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
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
Cleared hypotheses: T
-- 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)
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
have nil : (append nil (S.think.append T).join).destruct.tail = (append nil (S.append T).join).destruct
Tactic: refine ⟨nil, S, T, ?_, ?_⟩
-- 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)
T S : WSeq (WSeq α)
nil : (append WSeq.nil (S.think.append T).join).destruct.tail = (append WSeq.nil (S.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
have nil₁ : (append WSeq.nil (S.think.join.append T.join)).destruct.tail = (append WSeq.nil (S.join.append T.join)).destruct
Tactic: refine ⟨nil, S, T, ?_, ?_⟩
-- 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 α)
⊢ 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.append T).join).destruct.destruct (append nil (S.join.append T.join)).destruct.destruct
have 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 nil (append nil T).join).destruct.destruct (append nil (append (join nil) 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
-- 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
⊢ 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 α) (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
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
-- 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 : WSeq α
S 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)
    (s.append (S.append T).join).destruct.destruct (s.append (S.join.append T.join)).destruct.destruct
have 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 nil (S.append T).join).destruct.destruct (append nil (S.join.append T.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 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
  | cons a s => simpa using ⟨s, S, T, rfl, rfl⟩
  | think s => simpa using ⟨s, S, T, rfl, rfl⟩
Cleared hypotheses: s
-- 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 : WSeq α
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 (S.append T).join).destruct.destruct (append WSeq.nil (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)
    (s.append (S.append T).join).destruct.destruct (s.append (S.join.append T.join)).destruct.destruct
have cons : ∀ (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: induction s using WSeq.recOn with
  | nil =>
    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
  | cons a s => simpa using ⟨s, S, T, rfl, rfl⟩
  | think s => simpa using ⟨s, S, T, rfl, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map (ret ∘ f) s).join ~ʷ map f s
have rw : (map ret (map f s)).join ~ʷ map f s
Tactic: rw [map_comp]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join ~ʷ (map join SS).join
have 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
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⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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
have 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
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]⟩)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
    (append nil (append nil SS.join).join).destruct.destruct
    (append nil (append (join nil) (map join SS).join)).destruct.destruct
have 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
Tactic: simp only [nil_append, join_nil]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
have nil : (cons S SS).join.join.destruct.tail = (append nil (S.append SS.join).join).destruct
Tactic: refine ⟨nil, S, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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
have nil₁ : (map join (cons S SS)).join.destruct.tail = (append WSeq.nil (S.join.append (map join SS).join)).destruct
Tactic: refine ⟨nil, S, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
have nil : SS.think.join.join.destruct.tail = (append nil (append nil SS.join).join).destruct
Tactic: refine ⟨nil, nil, SS, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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
have nil₁ : (map join SS.think).join.destruct.tail = (append WSeq.nil (append (join WSeq.nil) (map join SS).join)).destruct
Tactic: refine ⟨nil, nil, SS, ?_, ?_⟩