awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
h_1 : ∀ (n : ℕ), s_1.get? n ~ t_1.get? n
s t : WSeq α
h : (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s'))
    (some (b, t'))
have refine_2 : ∀ (n : ℕ), s'.get? n ~ t'.get? n
Tactic: refine ⟨ab, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
h_1 : ∀ (n : ℕ), s_1.get? n ~ t_1.get? n
s t : WSeq α
h : (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s'.get? n ~ t'.get? n
have refine_2 : s.tail.get? n ~ t.tail.get? n
Tactic: refine
          (get?_congr (flatten_equiv (Computation.mem_map _ ma)) n).symm.trans
            ((?_ : get? (tail s) n ~ get? (tail t) n).trans
              (get?_congr (flatten_equiv (Computation.mem_map _ mb)) n))
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s_1 t_1 : WSeq α
h_1 : ∀ (n : ℕ), s_1.get? n ~ t_1.get? n
s t : WSeq α
h : (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) s t
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
b : α
t' : WSeq α
mb : some (b, t') ∈ t.destruct
ab : (a, s').1 = (b, t').1
n : ℕ
⊢ s.tail.get? n ~ t.tail.get? n
have refine_2 : s.get? (n + 1) ~ t.get? (n + 1)
Tactic: rw [get?_tail, get?_tail]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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
have 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)
Tactic: simp only [exists_and_left, destruct_map]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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)
have 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)
Tactic: apply Computation.liftRel_map _ _ (liftRel_destruct h)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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)
have none : ∀ (h : LiftRelO R (LiftRel R) 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)) none) (Option.map (Prod.map f2 (map f2)) p)
Tactic: rcases o with - | a
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have some : ∀ (a : α × WSeq α) (h : LiftRelO R (LiftRel R) (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)) (some a)) (Option.map (Prod.map f2 (map f2)) p)
Tactic: rcases o with - | a
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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) 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)) none) (Option.map (Prod.map f2 (map f2)) p)
have none : ∀ (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: rcases p with - | b
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have 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))
Tactic: rcases p with - | b
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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) (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)) (some a)) (Option.map (Prod.map f2 (map f2)) p)
have some : ∀ (h : LiftRelO R (LiftRel R) (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)) (some a)) (Option.map (Prod.map f2 (map f2)) none)
Tactic: rcases p with - | b
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have 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))
Tactic: rcases p with - | b
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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) 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)) none) (Option.map (Prod.map f2 (map f2)) (some b))
have none : ∀ (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 b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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) (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)) (some a)) (Option.map (Prod.map f2 (map f2)) none)
have some : ∀ (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 a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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) (some a) (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)) (some a)) (Option.map (Prod.map f2 (map f2)) (some b))
have some : ∀ (a : α) (s : WSeq α) (h : LiftRelO R (LiftRel R) (some (a, s)) (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)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some b))
Tactic: obtain ⟨a, s⟩ := a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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) (some (a, s)) (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)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some b))
have some : ∀ (b : β) (t : WSeq β) (h : LiftRelO R (LiftRel R) (some (a, s)) (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)) (some (a, s))) (Option.map (Prod.map f2 (map f2)) (some (b, t)))
Tactic: obtain ⟨b, t⟩ := b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
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))
⊢ 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)))
have r : R a b
Tactic: obtain ⟨r, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
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
⊢ 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)))
have h₁ : LiftRel R s t
Tactic: obtain ⟨r, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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
have 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
Tactic: apply Computation.LiftRel.imp _ _ _ (liftRel_destruct h)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 β)
⊢ 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
have 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
Tactic: apply LiftRelO.imp_right
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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
have 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))
Tactic: simp only [exists_and_left, destruct_append]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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))
have 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)
Tactic: apply Computation.liftRel_bind _ _ (liftRel_destruct h)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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)
have none : ∀ (h : LiftRelO R (LiftRel R) 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 none) (destruct_append.aux t2 p)
Tactic: rcases o with - | a
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have some : ∀ (a : α × WSeq α) (h : LiftRelO R (LiftRel R) (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 (some a)) (destruct_append.aux t2 p)
Tactic: rcases o with - | a
Cleared hypotheses: o, h