awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (Option.some a) p
some :
  ∀ (h : LiftRelO R (LiftRel R) (Option.some a) none),
    Computation.LiftRel
      (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      (destruct_append.aux s2 (Option.some a)) (destruct_append.aux t2 none)
some₁ :
  ∀ (b : β × WSeq β) (h : LiftRelO R (LiftRel R) (Option.some a) (Option.some b)),
    Computation.LiftRel
      (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      (destruct_append.aux s2 (Option.some a)) (destruct_append.aux t2 (Option.some b))
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (Option.some a)) (destruct_append.aux t2 p)

Tactic:
rcases p with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
apply :
  ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R
        (fun (s : WSeq α) (t : WSeq β) ↦
          LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
        a b
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    s2.destruct t2.destruct

Tactic:
apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h2)

Premises used: Stream'.WSeq.liftRel_destruct, Computation.LiftRel.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
H :
  ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R
      (fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      a b

Tactic:
apply LiftRelO.imp_right

Premises used: Stream'.WSeq.LiftRelO.imp_right
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s_1 : WSeq α
t_1 : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s_1 t_1
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
h : LiftRelO R (LiftRel R) none none
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x

Tactic:
apply Or.inl

Premises used: Or.inl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
b : β × WSeq β
h : LiftRelO R (LiftRel R) Option.none (some b)
none :
  ∀ (fst : β) (snd : WSeq β) (h : LiftRelO R (LiftRel R) Option.none (some (fst, snd))),
    Computation.LiftRel
      (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      (destruct_append.aux s2 Option.none) (destruct_append.aux t2 (some (fst, snd)))
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 Option.none) (destruct_append.aux t2 (some b))

Tactic:
cases b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
fst : β
snd : WSeq β
h : LiftRelO R (LiftRel R) none (some (fst, snd))
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 none) (destruct_append.aux t2 (some (fst, snd)))

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
a : α × WSeq α
h : LiftRelO R (LiftRel R) (Option.some a) none
some :
  ∀ (fst : α) (snd : WSeq α) (h : LiftRelO R (LiftRel R) (Option.some (fst, snd)) none),
    Computation.LiftRel
      (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      (destruct_append.aux s2 (Option.some (fst, snd))) (destruct_append.aux t2 none)
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (Option.some a)) (destruct_append.aux t2 none)

Tactic:
cases a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
fst : α
snd : WSeq α
h : LiftRelO R (LiftRel R) (some (fst, snd)) none
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some (fst, snd))) (destruct_append.aux t2 none)

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
a : α × WSeq α
b : β × WSeq β
h : LiftRelO R (LiftRel R) (Option.some a) (Option.some b)
some :
  ∀ (a : α) (s : WSeq α) (h : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some b)),
    Computation.LiftRel
      (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      (destruct_append.aux s2 (Option.some (a, s))) (destruct_append.aux t2 (Option.some b))
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (Option.some a)) (destruct_append.aux t2 (Option.some b))

Tactic:
obtain ⟨a, s⟩ := a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s_1 : WSeq α
t : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s_1 t
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
b : β × WSeq β
a : α
s : WSeq α
h : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some b)
some :
  ∀ (b : β) (t : WSeq β) (h : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some (b, t))),
    Computation.LiftRel
      (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
        LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
      (destruct_append.aux s2 (Option.some (a, s))) (destruct_append.aux t2 (Option.some (b, t)))
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (Option.some (a, s))) (destruct_append.aux t2 (Option.some b))

Tactic:
obtain ⟨b, t⟩ := b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s_1 : WSeq α
t_1 : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s_1 t_1
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ R a b

Tactic:
obtain ⟨r, h⟩ := h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s_1 : WSeq α
t_1 : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s_1 t_1
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
h : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
r : R a b
⊢ LiftRel R s t

Tactic:
obtain ⟨r, h⟩ := h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1_1 s2 : WSeq α
t1_1 t2 : WSeq β
h1 : LiftRel R s1_1 t1_1
h2 : LiftRel R s2 t2
s_1 : WSeq α
t_1 : WSeq β
h_1 :
  (fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
    s_1 t_1
s1 : WSeq α
t1 : WSeq β
h_2 : LiftRel R s1 t1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ Computation.LiftRel
    (LiftRelO R fun (s : WSeq α) (t : WSeq β) ↦
      LiftRel R s t ∨ ∃ (s1 : WSeq α), s = s1.append s2 ∧ ∃ (x : WSeq β), t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 (some (a, s))) (destruct_append.aux t2 (some (b, t)))

Tactic:
simpa using ⟨r, Or.inr ⟨s, rfl, t, rfl, h⟩⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
U : WSeq α → WSeq β → Prop
ST : LiftRel (LiftRel R) S T
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
a : Option (α × WSeq α)
ma : a ∈ S.join.destruct
obtain : ∀ (n : ℕ) (h : S.join.destruct.Results a n), ∃ b ∈ T.join.destruct, LiftRelO R U a b
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
obtain ⟨n, h⟩ := exists_results_of_mem ma

Premises used: Computation.exists_results_of_mem
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
U : WSeq α → WSeq β → Prop
ST : LiftRel (LiftRel R) S T
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
a : Option (α × WSeq α)
n : ℕ
h : S.join.destruct.Results a n
revert :
  ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} (ST : LiftRel (LiftRel R) S T) {a : Option (α × WSeq α)}
    (h : S.join.destruct.Results a n), ∃ b ∈ T.join.destruct, LiftRelO R U a b
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
revert S T ST a
-- 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 : ℕ
ind :
  ∀ (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 α)}
    (h : S.join.destruct.Results a n), ∃ b ∈ T.join.destruct, LiftRelO R U a b
⊢ ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)} (ST : LiftRel (LiftRel R) S T) {a : Option (α × WSeq α)}
    (h : S.join.destruct.Results a n), ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
induction n using Nat.strongRecOn with | _ n IH
-- 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.join.destruct.Results a n
⊢ (S.destruct.bind destruct_join.aux).Results a n

Tactic:
simp only [destruct_join] at ra

Premises used: Stream'.WSeq.destruct_join
-- 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
h : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
h_1 : S.destruct.Results none m
rs2 : Results (destruct_join.aux none) a k
mT : none ∈ T.destruct
simp : ∃ b ∈ T.destruct.bind destruct_join.aux, LiftRelO R U a b
⊢ ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
simp only [destruct_join]

Premises used: Stream'.WSeq.destruct_join
-- 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
h : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
h_1 : S.destruct.Results none m
rs2 : Results (destruct_join.aux none) a k
mT : none ∈ T.destruct
rw : LiftRelO R U none none
⊢ LiftRelO R U a none

Tactic:
rw [eq_of_pure_mem rs2.mem]

Premises used: Computation.Results.mem, Computation.eq_of_pure_mem
-- 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
h : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
h_1 : S.destruct.Results none m
rs2 : Results (destruct_join.aux none) a k
mT : none ∈ T.destruct
⊢ LiftRelO R U none none

Tactic:
trivial
-- 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
h : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
h_1 : S.destruct.Results none m
rs2 : Results (destruct_join.aux none) a k
mT : none ∈ T.destruct
⊢ ∃ b ∈ T.destruct.bind destruct_join.aux, LiftRelO R U a b

Tactic:
exact ⟨none, mem_bind mT (ret_mem _), by rw [eq_of_pure_mem rs2.mem]; trivial⟩
-- 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
rs2 : (destruct_join.aux (some (s, S'))).Results a k
mT : some (t, T') ∈ T.destruct
⊢ (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k

Tactic:
simp only [destruct_join.aux, destruct_append] at rs2

Premises used: Stream'.WSeq.destruct_join.aux, Stream'.WSeq.destruct_append
-- 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
rs2 : (destruct_join.aux (some (s, S'))).Results a k
mT : some (t, T') ∈ T.destruct
⊢ (s.destruct.bind (destruct_append.aux S'.join)).think.Results a k

Tactic:
simp? [destruct_append] at rs2 says simp only [destruct_join.aux, destruct_append] at rs2

Premises used: Stream'.WSeq.destruct_join.aux, Stream'.WSeq.destruct_append
-- 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
k1 : ℕ
rs3 : (s.destruct.bind (destruct_append.aux S'.join)).Results a k1
ek : k = k1 + 1
o' : Option (α × WSeq α)
m1 n1 : ℕ
rs4 : s.destruct.Results o' m1
rs5 : (destruct_append.aux S'.join o').Results a n1
ek1 : k1 = n1 + m1
p' : Option (β × WSeq β)
mt_1 : p' ∈ t.destruct
rop' : LiftRelO R (LiftRel R) o' p'
h_1 : LiftRelO R (LiftRel R) none none
h_2 : s.destruct.Results none m1
rs5' : (destruct_append.aux S'.join none).Results a n1
mt : none ∈ t.destruct
rw : n1 < n1 + m1 + 1 + m
⊢ n1 < n

Tactic:
rw [en, ek, ek1]