awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s_1 : WSeq α
t_1 : WSeq β
h_2 : S s_1 t_1
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h_3 : Computation.LiftRel (LiftRel R) c1 c2
a_1 : WSeq α
b_1 : WSeq β
ab : LiftRel R a_1 b_1
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ t = flatten (Computation.pure t)

Tactic:
simp [h]
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
R : α → β → Prop
c1_1 : Computation (WSeq α)
c2_1 : Computation (WSeq β)
h_1 : Computation.LiftRel (LiftRel R) c1_1 c2_1
S : (s : WSeq α) → (t : WSeq β) → Prop :=
  fun (s : WSeq α) (t : WSeq β) ↦
    ∃ (c1 : Computation (WSeq α)) (c2 : Computation (WSeq β)),
      s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s_1 : WSeq α
t_1 : WSeq β
h_2 : S s_1 t_1
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h_3 : Computation.LiftRel (LiftRel R) c1 c2
a_1 : WSeq α
b_1 : WSeq β
ab : LiftRel R a_1 b_1
a : Option (α × WSeq α)
b : Option (β × WSeq β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRel R) (Computation.pure s) (Computation.pure t)

Tactic:
simp [h]
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
c1 c2 : Computation (WSeq α)
⊢ Computation.LiftRel Equiv c1 c2 → flatten c1 ~ʷ flatten c2

Tactic:
liftRel_flatten

Premises used: Stream'.WSeq.liftRel_flatten, Stream'.WSeq.Equiv
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
a :
  Computation.LiftRel (α := WSeq α) Equiv
    ((fun (o : Option (α × WSeq α)) ↦
        Option.recOn (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) o nil Prod.snd) <$>
      s.destruct)
    ((fun (o : Option (α × WSeq α)) ↦
        Option.recOn (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) o nil Prod.snd) <$>
      t.destruct)
⊢ s.tail ~ʷ t.tail

Tactic:
apply flatten_congr

Premises used: Stream'.WSeq.flatten_congr
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
a :
  Computation.LiftRel (α := WSeq α) Equiv
    (s.destruct.bind
      (Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
        Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o))
    (t.destruct.bind
      (Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
        Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o))
⊢ Computation.LiftRel (α := WSeq α) Equiv
    (Computation.map
      (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      s.destruct)
    (Computation.map
      (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      t.destruct)

Tactic:
rw [← Computation.bind_pure, ← Computation.bind_pure]

Premises used: Computation.bind_pure
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
a :
  ∀ {a b : Option (α × WSeq α)},
    BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b →
      Computation.LiftRel (α := WSeq α) Equiv
        ((Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
            Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
          a)
        ((Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
            Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
          b)
⊢ Computation.LiftRel (α := WSeq α) Equiv
    (s.destruct.bind
      (Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
        Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o))
    (t.destruct.bind
      (Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
        Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o))

Tactic:
apply liftRel_bind _ _ (destruct_congr h)

Premises used: Stream'.WSeq.destruct_congr, Computation.liftRel_bind
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a₁ :
  Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd b)
⊢ Computation.LiftRel (α := WSeq α) Equiv
    ((Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
        Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      a)
    ((Computation.pure ∘ fun (o : Option (α × WSeq α)) ↦
        Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      b)

Tactic:
simp only [comp_apply, liftRel_pure]

Premises used: Computation.liftRel_pure, Function.comp_apply
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a₁ :
  ∀ (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none b),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd b)
a₂ :
  ∀ (a : α × WSeq α) (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) b),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some a))
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd b)
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd b)

Tactic:
rcases a with - | a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
b : Option (α × WSeq α)
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none b
a :
  ∀ (h : BisimO.{u} (α := α) (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none none),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
a₁ :
  ∀ (b : α × WSeq α) (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none (some b)),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some b))
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd b)

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
b : Option (α × WSeq α)
a : α × WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) b
a₁ :
  ∀ (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) none),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some a))
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
a₂ :
  ∀ (b : α × WSeq α) (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) (some b)),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some a))
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some b))
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some a))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd b)

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
h : BisimO.{u} (α := α) (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none none
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)

Tactic:
trivial
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
b : α × WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none (some b)
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some b))

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a : α × WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) none
a₁ :
  ∀ (fst : α) (snd : WSeq α) (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (fst, snd)) none),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (fst, snd)))
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some a))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)

Tactic:
cases a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
fst : α
snd : WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (fst, snd)) none
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (fst, snd)))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)

Tactic:
cases h
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a b : α × WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) (some b)
a₁ :
  ∀ (a : α) (s' : WSeq α) (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some b)),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s')))
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some b))
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some a))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some b))

Tactic:
obtain ⟨a, s'⟩ := a
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
b : α × WSeq α
a : α
s' : WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some b)
a₁ :
  ∀ (b : α) (t' : WSeq α) (h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))),
    Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s')))
      (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (b, t')))
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s')))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some b))

Tactic:
obtain ⟨b, t'⟩ := b
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s')))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (b, t')))

Tactic:
h.right

Premises used: And.right
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a : α
s' : WSeq α
b : α
t' : WSeq α
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Equiv.{u} (α := α) (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s')))
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (b, t')))

Tactic:
exact h.right

Premises used: And.right
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
zero : s.drop 0 ~ʷ t.drop 0
succ : ∀ (n : ℕ), s.drop n ~ʷ t.drop n → s.drop (n + 1) ~ʷ t.drop (n + 1)
⊢ s.drop n ~ʷ t.drop n

Tactic:
induction n
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.drop 0 ~ʷ t.drop 0

Tactic:
simp [*, tail_congr, drop]

Premises used: Stream'.WSeq.drop, Stream'.WSeq.tail_congr
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
h_1 : s.drop n ~ʷ t.drop n
⊢ s.drop (n + 1) ~ʷ t.drop (n + 1)

Tactic:
simp [*, tail_congr, drop]

Premises used: Stream'.WSeq.drop, Stream'.WSeq.tail_congr
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
⊢ s.get? n ~ t.get? n

Tactic:
head_congr (dropn_congr h _)

Premises used: Stream'.WSeq.head_congr, Stream'.WSeq.get?, Stream'.WSeq.dropn_congr
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
a : α
⊢ a ∈ s ↔ a ∈ t

Tactic:
suffices ∀ {s t : WSeq α}, s ~ʷ t → a ∈ s → a ∈ t from ⟨this h, this h.symm⟩
  fun {_ _} h as =>
  let ⟨_, hn⟩ := exists_get?_of_mem as
  get?_mem ((get?_congr h _ _).1 hn)

Premises used: Stream'.WSeq.get?_mem, Stream'.WSeq.exists_get?_of_mem, Option.some, Membership.mem, Stream'.WSeq.get?_congr, _private.0.Stream'.WSeq.mem_congr.match_1, Stream'.WSeq.Equiv.symm, Iff.intro, Iff.mp
-- Module: Mathlib.Data.WSeq.Relation
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
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n)
    s.destruct t.destruct

Tactic:
liftRel_def.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, Computation.liftRel_def
-- Module: Mathlib.Data.WSeq.Relation
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
refine_1 : s.destruct.Terminates ↔ t.destruct.Terminates
refine_2 :
  ∀ {a b : Option (α × WSeq α)},
    a ∈ s.destruct →
      b ∈ t.destruct → LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n)
    s.destruct t.destruct

Tactic:
refine liftRel_def.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, And.intro, Computation.liftRel_def
-- Module: Mathlib.Data.WSeq.Relation
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
refine_1 : s.head.Terminates ↔ t.head.Terminates
⊢ s.destruct.Terminates ↔ t.destruct.Terminates

Tactic:
rw [← head_terminates_iff, ← head_terminates_iff]

Premises used: Stream'.WSeq.head_terminates_iff
-- Module: Mathlib.Data.WSeq.Relation
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
⊢ s.head.Terminates ↔ t.head.Terminates

Tactic:
terminates_congr (h 0)

Premises used: Computation.terminates_congr, OfNat.ofNat
-- Module: Mathlib.Data.WSeq.Relation
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
⊢ s.head.Terminates ↔ t.head.Terminates

Tactic:
exact terminates_congr (h 0)

Premises used: Computation.terminates_congr, OfNat.ofNat
-- Module: Mathlib.Data.WSeq.Relation
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 b : Option (α × WSeq α)
ma : a ∈ s.destruct
mb : b ∈ t.destruct
refine_2 :
  ∀ (ma : none ∈ s.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none b
refine_2₁ :
  ∀ (a : α × WSeq α) (ma : some a ∈ s.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) b
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b

Tactic:
rcases a with - | a
-- Module: Mathlib.Data.WSeq.Relation
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
b : Option (α × WSeq α)
mb : b ∈ t.destruct
ma : none ∈ s.destruct
refine_2 :
  ∀ (mb : none ∈ t.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none none
refine_2₁ :
  ∀ (b : α × WSeq α) (mb : some b ∈ t.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none b

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.WSeq.Relation
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
b : Option (α × WSeq α)
mb : b ∈ t.destruct
a : α × WSeq α
ma : some a ∈ s.destruct
refine_2 :
  ∀ (mb : none ∈ t.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) none
refine_2₁ :
  ∀ (b : α × WSeq α) (mb : some b ∈ t.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) b

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.WSeq.Relation
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
ma : none ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none none

Tactic:
trivial
-- Module: Mathlib.Data.WSeq.Relation
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
ma : none ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none (some b)

Tactic:
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))

Premises used: Iff.mpr, Computation.mem_unique, Computation.mem_map, OfNat.ofNat
-- Module: Mathlib.Data.WSeq.Relation
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 : α × WSeq α
ma : some a ∈ s.destruct
mb : none ∈ t.destruct
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) none

Tactic:
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb))

Premises used: Iff.mpr, Computation.mem_unique, Computation.mem_map, OfNat.ofNat
-- Module: Mathlib.Data.WSeq.Relation
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 : α × WSeq α
ma : some a ∈ s.destruct
b : α × WSeq α
mb : some b ∈ t.destruct
refine_2 :
  ∀ (a : α) (s' : WSeq α) (ma : some (a, s') ∈ s.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some b)
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) (some b)

Tactic:
obtain ⟨a, s'⟩ := a
-- Module: Mathlib.Data.WSeq.Relation
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
b : α × WSeq α
mb : some b ∈ t.destruct
a : α
s' : WSeq α
ma : some (a, s') ∈ s.destruct
refine_2 :
  ∀ (b : α) (t' : WSeq α) (mb : some (b, t') ∈ t.destruct),
    LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s'))
      (some (b, t'))
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s')) (some b)

Tactic:
obtain ⟨b, t'⟩ := b
-- Module: Mathlib.Data.WSeq.Relation
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
⊢ (a, s').1 = (b, t').1

Tactic:
injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab

Premises used: Iff.mpr, Computation.mem_unique, Computation.mem_map, OfNat.ofNat
-- Module: Mathlib.Data.WSeq.Relation
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'))

Tactic:
⟨ab, fun n => ?_⟩

Premises used: Stream'.WSeq.LiftRelO, And.intro
-- Module: Mathlib.Data.WSeq.Relation
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
refine_2 : ∀ (n : ℕ), s'.get? n ~ t'.get? n
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s'))
    (some (b, t'))

Tactic:
refine ⟨ab, fun n => ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
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

Tactic:
(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))

Premises used: Computation.Equiv.symm, Stream'.WSeq.get?_congr, Computation.mem_map, Computation.Equiv.trans, Stream'.WSeq.flatten_equiv
-- Module: Mathlib.Data.WSeq.Relation
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 : ℕ
refine_2 : s.tail.get? n ~ t.tail.get? n
⊢ s'.get? n ~ t'.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))

Premises used: Computation.Equiv.symm, Stream'.WSeq.get?_congr, Computation.mem_map, Computation.Equiv.trans, Stream'.WSeq.flatten_equiv
-- Module: Mathlib.Data.WSeq.Relation
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 : ℕ
refine_2 : s.get? (n + 1) ~ t.get? (n + 1)
⊢ s.tail.get? n ~ t.tail.get? n

Tactic:
rw [get?_tail, get?_tail]

Premises used: Stream'.WSeq.get?_tail
-- Module: Mathlib.Data.WSeq.Relation
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 + 1) ~ t.get? (n + 1)

Tactic:
apply h