awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ Computation.LiftRel (LiftRelO R S) (flatten c1).destruct (flatten c2).destruct
have simp : Computation.LiftRel (LiftRelO R S) (c1 >>= destruct) (c2 >>= destruct)
Tactic: simp only [destruct_flatten]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
⊢ Computation.LiftRel (LiftRelO R S) (c1 >>= destruct) (c2 >>= destruct)
have apply : ∀ {a : WSeq α} {b : WSeq β}, LiftRel R a b → Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
Tactic: apply liftRel_bind _ _ h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
ab : LiftRel R a b
⊢ Computation.LiftRel (LiftRelO R S) a.destruct b.destruct
have apply : ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R S a b
Tactic: apply Computation.LiftRel.imp _ _ _ (liftRel_destruct ab)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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 : WSeq α
t : WSeq β
h_2 : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : 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 β)
⊢ LiftRelO R (LiftRel R) a b → LiftRelO R S a b
have H : ∀ (s : WSeq α) (t : WSeq β), LiftRel R s t → S s t
Tactic: apply LiftRelO.imp_right
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ S s t
have H : s = flatten (Computation.pure s)
Tactic: refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
H : s = flatten (Computation.pure s)
⊢ S s t
have H₁ : t = flatten (Computation.pure t)
Tactic: refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
H : s = flatten (Computation.pure s)
H₁ : t = flatten (Computation.pure t)
⊢ S s t
have H₂ : Computation.LiftRel (LiftRel R) (Computation.pure s) (Computation.pure t)
Tactic: refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.tail ~ʷ t.tail
have 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)
Tactic: apply flatten_congr
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ 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)
have 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))
Tactic: rw [← Computation.bind_pure, ← Computation.bind_pure]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ 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))
have 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)
Tactic: apply liftRel_bind _ _ (destruct_congr h)
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a b : Option (α × WSeq α)
h : 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)
have 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)
Tactic: simp only [comp_apply, liftRel_pure]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a b : Option (α × WSeq α)
h : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a 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)
have 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)
Tactic: rcases a with - | a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have 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)
Tactic: rcases a with - | a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
b : Option (α × WSeq α)
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)
have 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)
Tactic: rcases b with - | b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have 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))
Tactic: rcases b with - | b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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
⊢ 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)
have 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)
Tactic: rcases b with - | b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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)
have 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))
Tactic: rcases b with - | b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h_1 : s ~ʷ t
a : α × WSeq α
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)
have 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)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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))
have 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))
Tactic: obtain ⟨a, s'⟩ := a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
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)
⊢ 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))
have 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')))
Tactic: obtain ⟨b, t'⟩ := b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
⊢ s.drop n ~ʷ t.drop n
have zero : s.drop 0 ~ʷ t.drop 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
zero : s.drop 0 ~ʷ t.drop 0
⊢ s.drop n ~ʷ t.drop n
have succ : ∀ (n : ℕ), s.drop n ~ʷ t.drop n → s.drop (n + 1) ~ʷ t.drop (n + 1)
Tactic: induction n
Cleared hypotheses: 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
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n)
    s.destruct t.destruct
have refine_1 : s.destruct.Terminates ↔ t.destruct.Terminates
Tactic: refine liftRel_def.2 ⟨?_, ?_⟩
-- 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
refine_1 : s.destruct.Terminates ↔ t.destruct.Terminates
⊢ Computation.LiftRel (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n)
    s.destruct t.destruct
have 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
Tactic: refine liftRel_def.2 ⟨?_, ?_⟩
-- 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
⊢ s.destruct.Terminates ↔ t.destruct.Terminates
have refine_1 : s.head.Terminates ↔ t.head.Terminates
Tactic: rw [← head_terminates_iff, ← head_terminates_iff]
-- 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 b : Option (α × WSeq α)
ma : a ∈ s.destruct
mb : b ∈ t.destruct
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b
have 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
Tactic: rcases a with - | a
Cleared hypotheses: a, ma
-- 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 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
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) a b
have 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
Tactic: rcases a with - | a
Cleared hypotheses: a, ma
-- 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
b : Option (α × WSeq α)
mb : b ∈ t.destruct
ma : none ∈ s.destruct
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none b
have 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
Tactic: rcases b with - | b
Cleared hypotheses: b, mb
-- 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
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
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) none b
have 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)
Tactic: rcases b with - | b
Cleared hypotheses: b, mb
-- 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
b : Option (α × WSeq α)
mb : b ∈ t.destruct
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
have 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
Tactic: rcases b with - | b
Cleared hypotheses: b, mb
-- 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
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
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some a) b
have 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)
Tactic: rcases b with - | b
Cleared hypotheses: b, mb
-- 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 : α × WSeq α
ma : some a ∈ 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) (some a) (some b)
have 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)
Tactic: obtain ⟨a, s'⟩ := a
Cleared hypotheses: a, ma
-- 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
b : α × WSeq α
mb : some b ∈ t.destruct
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)
have 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'))
Tactic: obtain ⟨b, t'⟩ := b
Cleared hypotheses: b, mb
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
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
⊢ LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) (fun (s t : WSeq α) ↦ ∀ (n : ℕ), s.get? n ~ t.get? n) (some (a, s'))
    (some (b, t'))
have ab : (a, s').1 = (b, t').1
Tactic: injection mem_unique (Computation.mem_map _ ma) ((h 0 _).2 (Computation.mem_map _ mb)) with
          ab