awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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_1 : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a_1 n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2_1 : (destruct_join.aux o).Results a_1 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_1 k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a_1 k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5_1 : (destruct_append.aux S'.join o').Results a_1 n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt_1 : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
h_1 : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a_1 n1
mt : some (b, t') ∈ t.destruct
⊢ Membership.mem (γ := Computation (Option (β × WSeq β)))
    (T.destruct.bind fun (x : Option (WSeq β × WSeq (WSeq β))) ↦
      match (motive := Option (WSeq β × WSeq (WSeq β)) → Computation (Option (β × WSeq β))) x with
      | none => Computation.pure none
      | some (s, S) => (s.append S.join).destruct.think)
    (some (b, t'.append T'.join))
have refine_1 : Membership.mem (γ := Computation (Option (β × WSeq β)))
  (match (motive := Option (WSeq β × WSeq (WSeq β)) → Computation (Option (β × WSeq β))) some (t, T') with
    | none => Computation.pure none
    | some (s, S) => (s.append S.join).destruct.think :
    Computation (Option (β × WSeq β)))
  (some (b, t'.append T'.join))
Tactic: apply mem_bind mT
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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_1 : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a_1 n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2_1 : (destruct_join.aux o).Results a_1 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_1 k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a_1 k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5_1 : (destruct_append.aux S'.join o').Results a_1 n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt_1 : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
h_1 : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a_1 n1
mt : some (b, t') ∈ t.destruct
⊢ Membership.mem (γ := Computation (Option (β × WSeq β)))
    (match (motive := Option (WSeq β × WSeq (WSeq β)) → Computation (Option (β × WSeq β))) some (t, T') with
      | none => Computation.pure none
      | some (s, S) => (s.append S.join).destruct.think :
      Computation (Option (β × WSeq β)))
    (some (b, t'.append T'.join))
have refine_1 : some (b, t'.append T'.join) ∈ (t.destruct.bind (destruct_append.aux T'.join)).think
Tactic: simp only [destruct_append]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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_1 : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a_1 n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2_1 : (destruct_join.aux o).Results a_1 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_1 k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a_1 k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5_1 : (destruct_append.aux S'.join o').Results a_1 n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt_1 : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
h_1 : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a_1 n1
mt : some (b, t') ∈ t.destruct
⊢ some (b, t'.append T'.join) ∈ (t.destruct.bind (destruct_append.aux T'.join)).think
have refine_1 : some (b, t'.append T'.join) ∈ t.destruct.bind (destruct_append.aux T'.join)
Tactic: apply think_mem
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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_1 : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a_1 n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2_1 : (destruct_join.aux o).Results a_1 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_1 k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a_1 k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5_1 : (destruct_append.aux S'.join o').Results a_1 n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt_1 : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
h_1 : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a_1 n1
mt : some (b, t') ∈ t.destruct
⊢ some (b, t'.append T'.join) ∈ t.destruct.bind (destruct_append.aux T'.join)
have refine_1 : some (b, t'.append T'.join) ∈ destruct_append.aux T'.join (some (b, t'))
Tactic: apply mem_bind mt
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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_1 : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a_1 n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2_1 : (destruct_join.aux o).Results a_1 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_1 k
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a_1 k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5_1 : (destruct_append.aux S'.join o').Results a_1 n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt_1 : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
a : α
s' : WSeq α
b : β
t' : WSeq β
ab : R a b
st' : LiftRel R s' t'
h_1 : s.destruct.Results (some (a, s')) m1
rs5 : (Computation.pure (some (a, s'.append S'.join))).Results a_1 n1
mt : some (b, t') ∈ t.destruct
⊢ LiftRelO R U a_1 (some (b, t'.append T'.join))
have refine_2 : LiftRelO R U (some (a, s'.append S'.join)) (some (b, t'.append T'.join))
Tactic: rw [eq_of_pure_mem rs5.mem]
-- 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 : 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
⊢ 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
have 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
Tactic: rw [h1, h2]
-- 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 : 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
⊢ 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
have 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))
Tactic: rw [destruct_append, destruct_append]
-- 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 : 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
⊢ 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))
have 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)
Tactic: apply Computation.liftRel_bind _ _ (liftRel_destruct st)
-- 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
⊢ (∀ {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
have 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
Tactic: constructor
-- 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
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
⊢ (∀ {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
have 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
Tactic: constructor
-- 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
⊢ ∃ 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
have 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
Tactic: rw [← LiftRelO.swap]
-- 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
⊢ ∃ 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
have right : LiftRel (LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)) T S
Tactic: apply liftRel_join.lem (swap R)
-- 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
right : LiftRel (LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)) T S
⊢ ∃ 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
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 ∧
          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: apply liftRel_join.lem (swap R)
-- 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
⊢ LiftRel (LiftRel (swap (φ := fun (a : α) (a_1 : β) ↦ Prop) R)) T S
have right : swap (φ := fun (x : WSeq (WSeq α)) (y : WSeq (WSeq β)) ↦ Prop) (LiftRel (LiftRel R)) T S
Tactic: rw [← LiftRel.swap R, ← LiftRel.swap]