awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (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) →
      U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} (ST : LiftRel (LiftRel R) S T) {a : Option (α × WSeq α)}
      (h : S.join.destruct.Results a m), ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2_1 : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT_1 : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
s : WSeq α
S' : WSeq (WSeq α)
t : WSeq β
T' : WSeq (WSeq β)
st : LiftRel R s t
ST' : LiftRel (LiftRel R) S' T'
h : S.destruct.Results (some (s, S')) m
mT : some (t, T') ∈ T.destruct
rs2 : (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
exact
        let ⟨k1, rs3, ek⟩ := of_results_think rs2
        let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
        let ⟨p', mt, rop'⟩ := Computation.exists_of_liftRel_left (liftRel_destruct st) rs4.mem
        match o', p', rop', rs4, rs5, mt with
        | none, none, _, _, rs5', mt => by
          have : n1 < n := by
            rw [en, ek, ek1]
            apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
            apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
          let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
          refine ⟨ob, ?_, rob⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            exact mb
        | some (a, s'), some (b, t'), ⟨ab, st'⟩, _, rs5, mt => by
          simp only [destruct_append.aux] at rs5
          refine ⟨some (b, append t' (join T')), ?_, ?_⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            apply ret_mem
          rw [eq_of_pure_mem rs5.mem]
          exact ⟨ab, HU _ _ ⟨s', t', S', T', rfl, rfl, st', ST'⟩⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (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) →
      U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} (ST : LiftRel (LiftRel R) S T) {a : Option (α × WSeq α)}
      (h : S.join.destruct.Results a m), ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
exact
    let ⟨o, m, k, rs1, rs2, en⟩ := of_results_bind ra
    let ⟨p, mT, rop⟩ := Computation.exists_of_liftRel_left (liftRel_destruct ST) rs1.mem
    match o, p, rop, rs1, rs2, mT with
    | none, none, _, _, rs2, mT => by
      simp only [destruct_join]
      exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩
    | some (s, S'), some (t, T'), ⟨st, ST'⟩, _, rs2, mT => by
      simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2
      exact
        let ⟨k1, rs3, ek⟩ := of_results_think rs2
        let ⟨o', m1, n1, rs4, rs5, ek1⟩ := of_results_bind rs3
        let ⟨p', mt, rop'⟩ := Computation.exists_of_liftRel_left (liftRel_destruct st) rs4.mem
        match o', p', rop', rs4, rs5, mt with
        | none, none, _, _, rs5', mt => by
          have : n1 < n := by
            rw [en, ek, ek1]
            apply lt_of_lt_of_le _ (Nat.le_add_right _ _)
            apply Nat.lt_succ_of_le (Nat.le_add_right _ _)
          let ⟨ob, mb, rob⟩ := IH _ this ST' rs5'
          refine ⟨ob, ?_, rob⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            exact mb
        | some (a, s'), some (b, t'), ⟨ab, st'⟩, _, rs5, mt => by
          simp only [destruct_append.aux] at rs5
          refine ⟨some (b, append t' (join T')), ?_, ?_⟩
          · simp +unfoldPartialApp only [destruct_join, destruct_join.aux]
            apply mem_bind mT
            simp only [destruct_append]
            apply think_mem
            apply mem_bind mt
            apply ret_mem
          rw [eq_of_pure_mem rs5.mem]
          exact ⟨ab, HU _ _ ⟨s', t', S', T', rfl, rfl, st', ST'⟩⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h : LiftRel (LiftRel R) S T
⊢ S.join = append nil S.join

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h : LiftRel (LiftRel R) S T
⊢ T.join = append nil T.join

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h : LiftRel (LiftRel R) S T
⊢ LiftRel R nil nil

Tactic:
simp
-- 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
rw :
  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)
    (s.append S.join).destruct (t.append T.join).destruct
⊢ 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)
    s1.destruct s2.destruct

Tactic:
rw [h1, h2]
-- 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
rw :
  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)
    (s.destruct.bind (destruct_append.aux S.join)) (t.destruct.bind (destruct_append.aux T.join))
⊢ 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)
    (s.append S.join).destruct (t.append T.join).destruct

Tactic:
rw [destruct_append, destruct_append]

Premises used: Stream'.WSeq.destruct_append
-- 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
apply :
  ∀ {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)
⊢ 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)
    (s.destruct.bind (destruct_append.aux S.join)) (t.destruct.bind (destruct_append.aux T.join))

Tactic:
apply Computation.liftRel_bind _ _ (liftRel_destruct st)

Premises used: Stream'.WSeq.liftRel_destruct, Computation.liftRel_bind
-- 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_1 : WSeq α
t_1 : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1_1 : s1 = s_1.append S.join
h2_1 : s2 = t_1.append T.join
st : LiftRel R s_1 t_1
ST : LiftRel (LiftRel R) S T
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
a : α
s : WSeq α
b : β
t : WSeq β
h1 : R a b
h2 : LiftRel R s t
⊢ 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 (some (a, s))) (destruct_append.aux T.join (some (b, t)))

Tactic:
simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
-- 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
left :
  ∀ {a : Option (α × WSeq α)},
    a ∈ S.join.destruct →
      ∃ b ∈ T.join.destruct,
        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)
          a b
right :
  ∀ {b : Option (β × WSeq β)},
    b ∈ T.join.destruct →
      ∃ a ∈ S.join.destruct,
        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)
          a b
⊢ (∀ {a : Option (α × WSeq α)},
      a ∈ S.join.destruct →
        ∃ b ∈ T.join.destruct,
          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)
            a b) ∧
    ∀ {b : Option (β × WSeq β)},
      b ∈ T.join.destruct →
        ∃ a ∈ S.join.destruct,
          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)
            a b

Tactic:
constructor
-- 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
a : Option (α × WSeq α)
⊢ a ∈ S.join.destruct →
    ∃ b ∈ T.join.destruct,
      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)
        a b

Tactic:
apply liftRel_join.lem _ ST fun _ _ => id

Premises used: Stream'.WSeq.liftRel_join.lem, id
-- 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
right :
  ∃ a ∈ S.join.destruct,
    swap (φ := fun (x : Option (β × WSeq β)) (y : Option (α × WSeq α)) ↦ Prop)
      (LiftRelO (fun (x : β) (y : α) ↦ R y x) fun (s2 : WSeq β) (s1 : 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)
      a b
⊢ ∃ a ∈ S.join.destruct,
    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)
      a b

Tactic:
rw [← LiftRelO.swap]

Premises used: Stream'.WSeq.LiftRelO.swap
-- 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
right : LiftRel (LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)) T S
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 ∧
            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
right₂ : b ∈ T.join.destruct
apply : WSeq (WSeq β)
⊢ ∃ a ∈ S.join.destruct,
    swap (φ := fun (x : Option (β × WSeq β)) (y : Option (α × WSeq α)) ↦ Prop)
      (LiftRelO (fun (x : β) (y : α) ↦ R y x) fun (s2 : WSeq β) (s1 : 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)
      a b

Tactic:
apply liftRel_join.lem (swap R)

Premises used: Stream'.WSeq.liftRel_join.lem, Function.swap
-- 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
right : swap (φ := fun (x : WSeq (WSeq α)) (y : WSeq (WSeq β)) ↦ Prop) (LiftRel (LiftRel R)) T S
⊢ LiftRel (LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)) T S

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap]

Premises used: Stream'.WSeq.LiftRel.swap
-- 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
⊢ swap (φ := fun (x : WSeq (WSeq α)) (y : WSeq (WSeq β)) ↦ Prop) (LiftRel (LiftRel R)) T S

Tactic:
apply ST
-- 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
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
⊢ ∀ (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

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]

Premises used: Stream'.WSeq.LiftRel, Stream'.WSeq.LiftRel.swap
-- 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
⊢ ∀ (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:
fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩

Premises used: Stream'.WSeq.join, _private.0.Stream'.WSeq.liftRel_join.match_3, Exists, Stream'.WSeq.LiftRel, And, And.intro, Exists.intro, Eq, Stream'.WSeq.append
-- 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
⊢ ∀ (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:
exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
-- 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:
mb