awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
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
⊢ b ∈ T.join.destruct

Tactic:
exact mb
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
S_1 : WSeq (WSeq α)
T_1 : WSeq (WSeq β)
h : LiftRel (LiftRel R) S_1 T_1
s1 : WSeq α
s2 : WSeq β
h_1 :
  (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
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      Computation.LiftRel
        (LiftRelO R 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)
        (destruct_append.aux S.join a) (destruct_append.aux T.join b)

Tactic:
exact fun {o p} h =>
      match o, p, h with
      | some (a, s), some (b, t), ⟨h1, h2⟩ => by
        simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
      | none, none, _ => by
        -- We do not `dsimp` with `LiftRelO` since `liftRel_join.lem` uses `LiftRelO`.
        dsimp only [destruct_append.aux, Computation.LiftRel]; constructor
        · intro
          apply liftRel_join.lem _ ST fun _ _ => id
        · intro b mb
          rw [← LiftRelO.swap]
          apply liftRel_join.lem (swap R)
          · rw [← LiftRel.swap R, ← LiftRel.swap]
            apply ST
          · rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
            exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
          · exact mb
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
S T : WSeq (WSeq α)
h : LiftRel Equiv S T
⊢ S.join ~ʷ T.join

Tactic:
liftRel_join _ h

Premises used: Stream'.WSeq.liftRel_join, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : WSeq α
s2 : WSeq β
f1 : α → WSeq γ
f2 : β → WSeq δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → LiftRel S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind f1) (s2.bind f2)

Tactic:
liftRel_join _ (liftRel_map _ _ h1 @h2)

Premises used: Stream'.WSeq.liftRel_join, Stream'.WSeq.liftRel_map, Stream'.WSeq.bind
-- Module: Mathlib.Data.WSeq.Relation
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
rw : LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (f1 b) (f2 b)
⊢ LiftRel (fun (x1 x2 : β) ↦ x1 = x2) (f1 a) (f2 b)

Tactic:
rw [h]
-- Module: Mathlib.Data.WSeq.Relation
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 b) (f2 b)

Tactic:
apply h2
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s : WSeq α
⊢ (ret s).join ~ʷ s

Tactic:
simpa [ret] using think_equiv _

Premises used: Stream'.WSeq.ret, Stream'.WSeq.think_equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s : WSeq α
⊢ (map ret s).join ~ʷ s

Tactic:
⟨fun s1 s2 => join (map ret s2) = s1, rfl, ?_⟩

Premises used: Stream'.WSeq.join, Stream'.WSeq.LiftRel, And.intro, Stream'.WSeq.map, Exists.intro, Eq, Stream'.WSeq.Equiv, Stream'.WSeq.ret, rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s : WSeq α
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
⊢ (map ret s).join ~ʷ s

Tactic:
refine ⟨fun s1 s2 => join (map ret s2) = s1, rfl, ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
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
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦ (map ret s2).join = s1) s'.destruct
    s.destruct

Tactic:
rw [← h]
-- Module: Mathlib.Data.WSeq.Relation
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
Hc : ∃ (s_2 : WSeq α), (map ret s).join.destruct = (map ret s_2).join.destruct ∧ s.destruct = s_2.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

Tactic:
apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s

Premises used: Stream'.WSeq.join, Stream'.WSeq.destruct, Exists, And, Stream'.WSeq.map, Computation.liftRel_rec, Eq, Stream'.WSeq.ret
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s_2 : WSeq α
h : (map ret s_2).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
⊢ ∀ (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⟩
-- Module: Mathlib.Data.WSeq.Relation
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
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
⊢ 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

Tactic:
induction s using WSeq.recOn
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this :
  ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ 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:
simp [ret, this]

Premises used: Stream'.WSeq.ret
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this :
  ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
x : α
s_2 : 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_2)).join.destruct.destruct (cons x s_2).destruct.destruct

Tactic:
simp [ret, this]

Premises used: Stream'.WSeq.ret
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this :
  ∀ (s : WSeq α), ∃ (s' : WSeq α), (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
s_2 : 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_2.think).join.destruct.destruct s_2.think.destruct.destruct

Tactic:
simp [ret, this]

Premises used: Stream'.WSeq.ret
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
⊢ ∀ {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:
exact fun {c1 c2} h =>
      match c1, c2, h with
      | _, _, ⟨s, rfl, rfl⟩ => by
        clear h
        have (s : WSeq α) : ∃ s' : WSeq α,
            (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
          ⟨s, rfl, rfl⟩
        induction s using WSeq.recOn <;> simp [ret, this]
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ (s_2 : WSeq α), (map ret s).join.destruct = (map ret s_2).join.destruct ∧ s.destruct = s_2.destruct

Tactic:
⟨s, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s_1 s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ (s_2 : WSeq α), (map ret s).join.destruct = (map ret s_2).join.destruct ∧ s.destruct = s_2.destruct

Tactic:
exact ⟨s, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join = append nil (S.append T).join

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

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
S T : WSeq (WSeq α)
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
⊢ (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⟩, ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
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)
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
⊢ 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

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⟩)

Premises used: Stream'.WSeq.join, Stream'.WSeq.destruct, Exists, _private.0.Stream'.WSeq.join_append.match_1, congr_arg, And, And.intro, Exists.intro, Computation.liftRel_rec, Eq, Stream'.WSeq.append
-- 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
    (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
⊢ 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

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
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)
⊢ 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:
simp
-- 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)
s : WSeq α
T : WSeq (WSeq α)
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
⊢ 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:
simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]

Premises used: Computation.liftRelAux_inr_inr, Stream'.WSeq.join_cons, Computation.destruct_think, Stream'.WSeq.destruct_think
-- 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)
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

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

Premises used: And.intro, Exists.intro, Stream'.WSeq.nil
-- 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)
s : WSeq α
T : WSeq (WSeq α)
nil : (s.append T.join).destruct = (s.append (append WSeq.nil T).join).destruct
nil₁ : (s.append T.join).destruct = (s.append (append (join 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

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

Tactic:
simp
-- 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)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (append (join nil) T.join)).destruct

Tactic:
simp
-- 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 :
  ∃ (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
⊢ 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:
simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]

Premises used: Computation.liftRelAux_inr_inr, Stream'.WSeq.join_think, Computation.destruct_think, Stream'.WSeq.destruct_think
-- 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 α)
⊢ ∃ (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:
⟨nil, nil, T, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Stream'.WSeq.nil
-- 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 : T.join.destruct = (append WSeq.nil (append WSeq.nil T).join).destruct
nil₁ : T.join.destruct = (append WSeq.nil (append (join 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

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

Tactic:
simp
-- 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 α)
⊢ T.join.destruct = (append nil (append (join nil) T.join)).destruct

Tactic:
simp