awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
S_1 : WSeq (WSeq α)
T_1 : WSeq (WSeq β)
h_1 : LiftRel (LiftRel R) S_1 T_1
s1 : WSeq α
s2 : WSeq β
h_2 :
  (fun (s1 : WSeq α) (s2 : WSeq β) ↦
      ∃ (s : WSeq α) (t : WSeq β) (S : WSeq (WSeq α)) (T : WSeq (WSeq β)),
        s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
h_3 : LiftRelO R (LiftRel R) none none
b : Option (β × WSeq β)
mb : b ∈ T.join.destruct
⊢ ∀ (s1 : WSeq β) (s2 : WSeq α),
    (∃ (s : WSeq β) (t : WSeq α) (S : WSeq (WSeq β)) (T : WSeq (WSeq α)),
        s1 = s.append S.join ∧
          s2 = t.append T.join ∧
            LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R) s t ∧
              LiftRel (LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)) S T) →
      ∃ (s : WSeq α) (t : WSeq β) (S : WSeq (WSeq α)) (T : WSeq (WSeq β)),
        s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T
have right : ∀ (s1 : WSeq β) (s2 : WSeq α),
  (∃ (s : WSeq β) (t : WSeq α) (S : WSeq (WSeq β)) (T : WSeq (WSeq α)),
      s1 = s.append S.join ∧
        s2 = t.append T.join ∧
          swap (φ := fun (x : WSeq α) (y : WSeq β) ↦ Prop) (LiftRel R) s t ∧
            swap (φ := fun (x : WSeq (WSeq α)) (y : WSeq (WSeq β)) ↦ Prop) (LiftRel (LiftRel R)) S T) →
    ∃ (s : WSeq α) (t : WSeq β) (S : WSeq (WSeq α)) (T : WSeq (WSeq β)),
      s2 = s.append S.join ∧ s1 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T
Tactic: rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
s1 s2 : WSeq α
f1 f2 : α → WSeq β
h1 : s1 ~ʷ s2
h2 : ∀ (a : α), f1 a ~ʷ f2 a
a b : α
h : a = b
⊢ LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (f1 a) (f2 b)
have rw : LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (f1 b) (f2 b)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s : WSeq α
⊢ (map ret s).join ~ʷ s
have refine : ∀ {s t : WSeq α},
  (fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1) s t →
    Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1) s.destruct
      t.destruct
Tactic: refine ⟨fun s1 s2 => join (map ret s2) = s1, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1) s'.destruct
    s.destruct
have rw : Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
  (map ret s).join.destruct s.destruct
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (map ret s).join.destruct s.destruct
have H : ∀ {ca cb : Computation (Option (α × WSeq α))},
  (∃ (s : WSeq α), ca = (map ret s).join.destruct ∧ cb = s.destruct) →
    LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
      ca.destruct cb.destruct
Tactic: apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
H :
  ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ (s : WSeq α), ca = (map ret s).join.destruct ∧ cb = s.destruct) →
      LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
        (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
          ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
        ca.destruct cb.destruct
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (map ret s).join.destruct s.destruct
have Hc : ∃ (s_2 : WSeq α), (map ret s).join.destruct = (map ret s_2).join.destruct ∧ s.destruct = s_2.destruct
Tactic: apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
s_1 s' s_2 : WSeq α
h : (map ret s_2).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
⊢ LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (map ret s).join.destruct.destruct s.destruct.destruct
have this : ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
Tactic: have (s : WSeq α) : ∃ s' : WSeq α,
            (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
          ⟨s, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 s' s_2 : WSeq α
h : (map ret s_2).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this :
  ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (map ret s).join.destruct.destruct s.destruct.destruct
have nil : LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
  (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
  (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
  (Computation.destruct (destruct (join (map ret nil)))) (Computation.destruct (destruct nil))
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 s' s_2 : WSeq α
h : (map ret s_2).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this :
  ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
nil :
  LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (Computation.destruct (destruct (join (map ret WSeq.nil)))) (Computation.destruct (destruct WSeq.nil))
⊢ LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (map ret s).join.destruct.destruct s.destruct.destruct
have cons : ∀ (x : α) (s : WSeq α),
  LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (map ret (cons x s)).join.destruct.destruct (cons x s).destruct.destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 s' s_2 : WSeq α
h : (map ret s_2).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this :
  ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
nil :
  LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (Computation.destruct (destruct (join (map ret WSeq.nil)))) (Computation.destruct (destruct WSeq.nil))
cons :
  ∀ (x : α) (s : WSeq α),
    LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
      (map ret (WSeq.cons x s)).join.destruct.destruct (WSeq.cons x s).destruct.destruct
⊢ LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (map ret s).join.destruct.destruct s.destruct.destruct
have think : ∀ (s : WSeq α),
  LiftRelAux (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1)
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦ ∃ (s : WSeq α), c1 = (map ret s).join.destruct ∧ c2 = s.destruct)
    (map ret s.think).join.destruct.destruct s.think.destruct.destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join ~ʷ S.join.append T.join
have s1 : ∀ {s t : WSeq α},
  (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))
      s t →
    Computation.LiftRel
      (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))
      s.destruct t.destruct
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⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
S T : 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)
⊢ Computation.LiftRel
    (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))
    s1.destruct s2.destruct
have c1 : ∀ {ca cb : Computation (Option (α × WSeq α))},
  (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)
      ca cb →
    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)
      ca.destruct cb.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⟩)
-- 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 α)
⊢ 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
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)
  T.join.destruct.destruct T.join.destruct.destruct
Tactic: simp only [nil_append, join_nil]
-- 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)
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
have nil : ∃ (s_1 : WSeq α) (S : WSeq (WSeq α)) (T_2 : WSeq (WSeq α)),
  (s.append T.join).destruct = (s_1.append (S.append T_2).join).destruct ∧
    (s.append T.join).destruct = (s_1.append (S.join.append T_2.join)).destruct
Tactic: simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
-- 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)
s : WSeq α
T : WSeq (WSeq α)
⊢ ∃ (s_1 : WSeq α) (S : WSeq (WSeq α)) (T_2 : WSeq (WSeq α)),
    (s.append T.join).destruct = (s_1.append (S.append T_2).join).destruct ∧
      (s.append T.join).destruct = (s_1.append (S.join.append T_2.join)).destruct
have nil : (s.append T.join).destruct = (s.append (append nil T).join).destruct
Tactic: refine ⟨s, nil, T, ?_, ?_⟩
-- 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)
s : WSeq α
T : WSeq (WSeq α)
nil : (s.append T.join).destruct = (s.append (append WSeq.nil T).join).destruct
⊢ ∃ (s_1 : WSeq α) (S : WSeq (WSeq α)) (T_2 : WSeq (WSeq α)),
    (s.append T.join).destruct = (s_1.append (S.append T_2).join).destruct ∧
      (s.append T.join).destruct = (s_1.append (S.join.append T_2.join)).destruct
have nil₁ : (s.append T.join).destruct = (s.append (append (join WSeq.nil) T.join)).destruct
Tactic: refine ⟨s, nil, T, ?_, ?_⟩
-- 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 α)
⊢ 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
have nil : ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T_2 : WSeq (WSeq α)),
  T.join.destruct = (s.append (S.append T_2).join).destruct ∧
    T.join.destruct = (s.append (S.join.append T_2.join)).destruct
Tactic: simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
-- 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 α)
⊢ ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T_2 : WSeq (WSeq α)),
    T.join.destruct = (s.append (S.append T_2).join).destruct ∧
      T.join.destruct = (s.append (S.join.append T_2.join)).destruct
have nil : T.join.destruct = (append nil (append nil T).join).destruct
Tactic: refine ⟨nil, nil, T, ?_, ?_⟩
-- 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 : T.join.destruct = (append WSeq.nil (append WSeq.nil T).join).destruct
⊢ ∃ (s : WSeq α) (S : WSeq (WSeq α)) (T_2 : WSeq (WSeq α)),
    T.join.destruct = (s.append (S.append T_2).join).destruct ∧
      T.join.destruct = (s.append (S.join.append T_2.join)).destruct
have nil₁ : T.join.destruct = (append WSeq.nil (append (join WSeq.nil) T.join)).destruct
Tactic: refine ⟨nil, nil, T, ?_, ?_⟩
-- 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 α)
⊢ 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 : 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 nil))) (Computation.destruct (destruct (join nil)))
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 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)))
⊢ 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₁ : ∀ (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
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