awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
simp :
  Computation.LiftRel
    (LiftRelO S fun (s1 : WSeq γ) (s2 : WSeq δ) ↦
      ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Computation.map (Option.map (Prod.map f1 (map f1))) s.destruct)
    (Computation.map (Option.map (Prod.map f2 (map f2))) t.destruct)
⊢ Computation.LiftRel
    (LiftRelO S fun (s1 : WSeq γ) (s2 : WSeq δ) ↦
      ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t)
    (map f1 s).destruct (map f2 t).destruct

Tactic:
simp only [exists_and_left, destruct_map]

Premises used: Stream'.WSeq.destruct_map, exists_and_left
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
apply :
  ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO S
        (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦
          ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
        (Option.map (Prod.map f1 (map f1)) a) (Option.map (Prod.map f2 (map f2)) b)
⊢ Computation.LiftRel
    (LiftRelO S fun (s1 : WSeq γ) (s2 : WSeq δ) ↦
      ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Computation.map (Option.map (Prod.map f1 (map f1))) s.destruct)
    (Computation.map (Option.map (Prod.map f2 (map f2))) t.destruct)

Tactic:
apply Computation.liftRel_map _ _ (liftRel_destruct h)

Premises used: Stream'.WSeq.liftRel_destruct, Computation.liftRel_map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
none :
  ∀ (h : LiftRelO R (LiftRel R) Option.none p),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) Option.none) (Option.map (Prod.map f2 (map f2)) p)
some :
  ∀ (a : α × WSeq α) (h : LiftRelO R (LiftRel R) (Option.some a) p),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) (Option.some a)) (Option.map (Prod.map f2 (map f2)) p)
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) o) (Option.map (Prod.map f2 (map f2)) p)

Tactic:
rcases o with - | a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) Option.none p
none :
  ∀ (h : LiftRelO R (LiftRel R) Option.none Option.none),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) Option.none) (Option.map (Prod.map f2 (map f2)) Option.none)
none₁ :
  ∀ (b : β × WSeq β) (h : LiftRelO R (LiftRel R) Option.none (some b)),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) Option.none) (Option.map (Prod.map f2 (map f2)) (some b))
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) Option.none) (Option.map (Prod.map f2 (map f2)) p)

Tactic:
rcases p with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
p : Option (β × WSeq β)
a : α × WSeq α
h : LiftRelO R (LiftRel R) (Option.some a) p
some :
  ∀ (h : LiftRelO R (LiftRel R) (Option.some a) none),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) (Option.some a)) (Option.map (Prod.map f2 (map f2)) none)
some₁ :
  ∀ (b : β × WSeq β) (h : LiftRelO R (LiftRel R) (Option.some a) (Option.some b)),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) (Option.some a)) (Option.map (Prod.map f2 (map f2)) (Option.some b))
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (Option.some a)) (Option.map (Prod.map f2 (map f2)) p)

Tactic:
rcases p with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
h : LiftRelO R (LiftRel R) none none
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) none)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
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))),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) Option.none) (Option.map (Prod.map f2 (map f2)) (some (fst, snd)))
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) Option.none) (Option.map (Prod.map f2 (map f2)) (some b))

Tactic:
cases b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
fst : β
snd : WSeq β
h : LiftRelO R (LiftRel R) none (some (fst, snd))
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) none) (Option.map (Prod.map f2 (map f2)) (some (fst, snd)))

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
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),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) (Option.some (fst, snd))) (Option.map (Prod.map f2 (map f2)) none)
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (Option.some a)) (Option.map (Prod.map f2 (map f2)) none)

Tactic:
cases a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
fst : α
snd : WSeq α
h : LiftRelO R (LiftRel R) (some (fst, snd)) none
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some (fst, snd))) (Option.map (Prod.map f2 (map f2)) none)

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h_2 : LiftRel R s t
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)),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) (Option.some (a, s))) (Option.map (Prod.map f2 (map f2)) (Option.some b))
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (Option.some a)) (Option.map (Prod.map f2 (map f2)) (Option.some b))

Tactic:
obtain ⟨a, s⟩ := a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s_1 : WSeq α
t : WSeq β
h_2 : LiftRel R s_1 t
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))),
    LiftRelO S
      (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
      (Option.map (Prod.map f1 (map f1)) (Option.some (a, s))) (Option.map (Prod.map f2 (map f2)) (Option.some (b, t)))
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (Option.some (a, s))) (Option.map (Prod.map f2 (map f2)) (Option.some b))

Tactic:
obtain ⟨b, t⟩ := b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s_1 : WSeq α
t_1 : WSeq β
h_2 : LiftRel R s_1 t_1
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
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s_1 : WSeq α
t_1 : WSeq β
h_2 : LiftRel R s_1 t_1
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
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s_1 : WSeq α
t_1 : WSeq β
h_2 : LiftRel R s_1 t_1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some (b, t)))

Tactic:
⟨h2 r, s, rfl, t, rfl, h⟩

Premises used: Stream'.WSeq.LiftRelO, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1_1 : WSeq α
s2_1 : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1_1 s2_1
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h_1 :
  (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α) (t : WSeq β), s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s_1 : WSeq α
t_1 : WSeq β
h_2 : LiftRel R s_1 t_1
a : α
s : WSeq α
b : β
t : WSeq β
r : R a b
h : LiftRel R s t
⊢ LiftRelO S
    (fun (s1 : WSeq γ) (s2 : WSeq δ) ↦ ∃ (s : WSeq α), s1 = map f1 s ∧ ∃ (x : WSeq β), s2 = map f2 x ∧ LiftRel R s x)
    (Option.map (Prod.map f1 (map f1)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some (b, t)))

Tactic:
exact ⟨h2 r, s, rfl, t, rfl, h⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
f : α → β
s t : WSeq α
h : s ~ʷ t
⊢ map f s ~ʷ map f t

Tactic:
liftRel_map _ _ h fun {_ _} => congr_arg _

Premises used: Stream'.WSeq.liftRel_map, congr_arg, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
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
s : WSeq α
t : WSeq β
h : LiftRel R s t
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 α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1)
        a b
⊢ Computation.LiftRel
    (LiftRelO R 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.destruct t.destruct

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

Premises used: Stream'.WSeq.liftRel_destruct, Computation.LiftRel.imp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
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
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
H :
  ∀ (s : WSeq α) (t : WSeq β),
    LiftRel R s t → LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R
      (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)
      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 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
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
s_2 : WSeq α
t_2 : WSeq β
h : LiftRel R s_2 t_2
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ ∃ (s1 : WSeq α) (t1 : WSeq β), s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1

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 : LiftRel R s1 t1
simp :
  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)
    (s1.destruct.bind (destruct_append.aux s2)) (t1.destruct.bind (destruct_append.aux t2))
⊢ Computation.LiftRel
    (LiftRelO R 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)
    (s1.append s2).destruct (t1.append t2).destruct

Tactic:
simp only [exists_and_left, destruct_append]

Premises used: exists_and_left, Stream'.WSeq.destruct_append
-- 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 : LiftRel R s1 t1
apply :
  ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) 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)
        (destruct_append.aux s2 a) (destruct_append.aux t2 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)
    (s1.destruct.bind (destruct_append.aux s2)) (t1.destruct.bind (destruct_append.aux t2))

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

Premises used: Stream'.WSeq.liftRel_destruct, Computation.liftRel_bind
-- 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
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
none :
  ∀ (h : LiftRelO R (LiftRel R) Option.none p),
    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 p)
some :
  ∀ (a : α × WSeq α) (h : LiftRelO R (LiftRel R) (Option.some a) p),
    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)
⊢ 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 o) (destruct_append.aux t2 p)

Tactic:
rcases o with - | 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
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) Option.none p
none :
  ∀ (h : LiftRelO R (LiftRel R) Option.none Option.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.none) (destruct_append.aux t2 Option.none)
none₁ :
  ∀ (b : β × WSeq β) (h : LiftRelO R (LiftRel R) Option.none (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.none) (destruct_append.aux t2 (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.none) (destruct_append.aux t2 p)

Tactic:
rcases p with - | b