awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t : WSeq α
h1_2 : LiftRel R s_2 t
h2_2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
b : Option (α × WSeq α)
hb : b ∈ t.destruct
c : α × WSeq α
hc : Option.some c ∈ u.destruct
t2 : LiftRelO R (LiftRel R) b (Option.some c)
a : α
s : WSeq α
ha : Option.some (a, s) ∈ s_2.destruct
t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) b
some :
  ∀ (hb : none ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) none (Option.some c))
    (t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) none),
    LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)
have some₁ : ∀ (b : α × WSeq α) (hb : Option.some b ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) (Option.some b) (Option.some c))
  (t1 : LiftRelO R (LiftRel R) (Option.some (a, s)) (Option.some b)),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (Option.some (a, s)) (Option.some c)
Tactic: rcases b with - | b
Cleared hypotheses: b, hb, t2, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t : WSeq α
h1_2 : LiftRel R s_2 t
h2_2 : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some b)
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
have some : ∀ (b : α) (t_2 : WSeq α) (hb : some (b, t_2) ∈ t.destruct) (t2 : LiftRelO R (LiftRel R) (some (b, t_2)) (some c))
  (t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t_2))),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
Tactic: obtain ⟨b, t⟩ := b
Cleared hypotheses: b, hb, t2, t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u.destruct
c : α × WSeq α
hc : some c ∈ u.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some c)
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some c)
have some : ∀ (c : α) (u_2 : WSeq α) (hc : some (c, u_2) ∈ u.destruct) (t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u_2))),
  LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u_2))
Tactic: obtain ⟨c, u⟩ := c
Cleared hypotheses: c, hc, t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
have ab : R a b
Tactic: obtain ⟨ab, st⟩ := t1
Cleared hypotheses: t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
t1 : LiftRelO R (LiftRel R) (some (a, s)) (some (b, t))
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
have st : LiftRel R s t
Tactic: obtain ⟨ab, st⟩ := t1
Cleared hypotheses: t1
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
have bc : R b c
Tactic: obtain ⟨bc, tu⟩ := t2
Cleared hypotheses: t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst : IsTrans α R
s_1 t_1 u_1 : WSeq α
h1_1 : LiftRel R s_1 t_1
h2_1 : LiftRel R t_1 u_1
s_2 u_2 t_2 : WSeq α
h1_2 : LiftRel R s_2 t_2
h2_2 : LiftRel R t_2 u_2
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s_2.destruct t_2.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t_2.destruct u_2.destruct
a : α
s : WSeq α
ha : some (a, s) ∈ s_2.destruct
b : α
t : WSeq α
hb : some (b, t) ∈ t_2.destruct
c : α
u : WSeq α
hc : some (c, u) ∈ u_2.destruct
t2 : LiftRelO R (LiftRel R) (some (b, t)) (some (c, u))
ab : R a b
st : LiftRel R s t
bc : R b c
⊢ LiftRelO R (fun (s u : WSeq α) ↦ ∃ (t : WSeq α), LiftRel R s t ∧ LiftRel R t u) (some (a, s)) (some (c, u))
have tu : LiftRel R t u
Tactic: obtain ⟨bc, tu⟩ := t2
Cleared hypotheses: t2
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop (n + 1)).destruct (t.drop (n + 1)).destruct
have simp : Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)
Tactic: simp only [drop, destruct_tail]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)
have h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop n).destruct (t.drop n).destruct
Tactic: apply liftRel_bind
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop n).destruct (t.drop n).destruct
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)
have h2 : ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
  LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)
Tactic: apply liftRel_bind
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) (s.drop n).destruct (t.drop n).destruct
h2 :
  ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b → Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux a) (tail.aux b)
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) ((s.drop n).destruct >>= tail.aux) ((t.drop n).destruct >>= tail.aux)
have R₁ : Option (α × WSeq α) → Option (β × WSeq β) → Prop
Tactic: apply liftRel_bind
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h : a ∈ s
⊢ ∃ b ∈ t, R a b
have let : ∀ (n : ℕ) (h : some a ∈ s.get? n), ∃ b ∈ t, R a b
Tactic: let ⟨n, h⟩ := exists_get?_of_mem h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ b ∈ t, R a b
have let : ∀ (s' : WSeq α) (sd : some (a, s') ∈ (s.drop n).destruct), ∃ b ∈ t, R a b
Tactic: let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
s' : WSeq α
sd : some (a, s') ∈ (s.drop n).destruct
⊢ ∃ b ∈ t, R a b
have let : ∀ (b : β) (t' : WSeq β) (td : some (b, t') ∈ (t.drop n).destruct) (ab : R a b), LiftRel R s' t' → ∃ b ∈ t, R a b
Tactic: let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
b : β
h : b ∈ t
⊢ ∃ a ∈ s, R a b
have rw : ∀ (H : swap (φ := fun (x : WSeq β) (y : WSeq α) ↦ Prop) (LiftRel fun (x : β) (y : α) ↦ R y x) s t) {b : β} (h : b ∈ t),
  ∃ a ∈ s, R a b
Tactic: rw [← LiftRel.swap] at H
Cleared hypotheses: H, b, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ LiftRel R s.think t ↔ LiftRel R s t
have rw : Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
  Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Tactic: rw [liftRel_destruct_iff, liftRel_destruct_iff]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
⊢ ∀ {s t : WSeq α}, s ~ʷ t → s.head ~ t.head
have suffices : ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ s.head → o ∈ t.head
Tactic: suffices ∀ {s t : WSeq α}, s ~ʷ t → ∀ {o}, o ∈ head s → o ∈ head t from fun s t h o =>
    ⟨this h, this h.symm⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
⊢ o ∈ t.head
have rcases : ∀ (ds : Option (α × WSeq α)) (dsm : ds ∈ s.destruct) (dse : Prod.fst <$> ds = o), o ∈ t.head
Tactic: rcases @Computation.exists_of_mem_map _ _ _ _ (destruct s) ho with ⟨ds, dsm, dse⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
⊢ o ∈ t.head
have rw : Prod.fst <$> ds ∈ t.head
Tactic: rw [← dse]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
⊢ Prod.fst <$> ds ∈ t.head
have l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
Tactic: obtain ⟨l, r⟩ := destruct_congr h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (hypothesis)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
⊢ Prod.fst <$> ds ∈ t.head
have r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
Tactic: obtain ⟨l, r⟩ := destruct_congr h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
⊢ Prod.fst <$> ds ∈ t.head
have rcases : ∀ (dt : Option (α × WSeq α)) (dtm : dt ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) ds dt),
  Prod.fst <$> ds ∈ t.head
Tactic: rcases l dsm with ⟨dt, dtm, dst⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) ds dt
⊢ Prod.fst <$> ds ∈ t.head
have none : ∀ (dsm : none ∈ s.destruct) (dse : Functor.map (α := α × WSeq α) Prod.fst none = o)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none dt), Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head
Tactic: rcases ds with - | a
Cleared hypotheses: ds, dsm, dse, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
ds : Option (α × WSeq α)
dsm : ds ∈ s.destruct
dse : Prod.fst <$> ds = o
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) ds dt
none :
  ∀ (dsm : Option.none ∈ s.destruct) (dse : Functor.map (α := α × WSeq α) Prod.fst Option.none = o)
    (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none dt),
    Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
⊢ Prod.fst <$> ds ∈ t.head
have some : ∀ (a : α × WSeq α) (dsm : some a ∈ s.destruct) (dse : Prod.fst <$> some a = o)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) dt), Prod.fst <$> some a ∈ t.head
Tactic: rcases ds with - | a
Cleared hypotheses: ds, dsm, dse, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dsm : none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst none = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none dt
⊢ Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head
have none : ∀ (dtm : none ∈ t.destruct) (dst : BisimO.{u} (α := α) (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none none),
  Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head
Tactic: rcases dt with - | b
Cleared hypotheses: dt, dtm, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
dsm : Option.none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst Option.none = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none dt
none :
  ∀ (dtm : Option.none ∈ t.destruct)
    (dst : BisimO.{u} (α := α) (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none Option.none),
    Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
⊢ Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
have none₁ : ∀ (b : α × WSeq α) (dtm : some b ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) Option.none (some b)),
  Functor.map (α := α × WSeq α) Prod.fst Option.none ∈ t.head
Tactic: rcases dt with - | b
Cleared hypotheses: dt, dtm, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) dt
⊢ Prod.fst <$> some a ∈ t.head
have some : ∀ (dtm : none ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) none), Prod.fst <$> some a ∈ t.head
Tactic: rcases dt with - | b
Cleared hypotheses: dt, dtm, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dt : Option (α × WSeq α)
dtm : dt ∈ t.destruct
a : α × WSeq α
dsm : Option.some a ∈ s.destruct
dse : Prod.fst <$> Option.some a = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) dt
some :
  ∀ (dtm : none ∈ t.destruct) (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) none),
    Prod.fst <$> Option.some a ∈ t.head
⊢ Prod.fst <$> Option.some a ∈ t.head
have some₁ : ∀ (b : α × WSeq α) (dtm : Option.some b ∈ t.destruct)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (Option.some a) (Option.some b)), Prod.fst <$> Option.some a ∈ t.head
Tactic: rcases dt with - | b
Cleared hypotheses: dt, dtm, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
dsm : none ∈ s.destruct
dse : Functor.map (α := α × WSeq α) Prod.fst none = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none (some b)
⊢ Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head
have none : ∀ (fst : α) (snd : WSeq α) (dtm : some (fst, snd) ∈ t.destruct)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) none (some (fst, snd))),
  Functor.map (α := α × WSeq α) Prod.fst none ∈ t.head
Tactic: cases b
Cleared hypotheses: b, dtm, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
dtm : none ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) none
⊢ Prod.fst <$> some a ∈ t.head
have some : ∀ (fst : α) (snd : WSeq α) (dsm : some (fst, snd) ∈ s.destruct) (dse : Prod.fst <$> some (fst, snd) = o)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (fst, snd)) none), Prod.fst <$> some (fst, snd) ∈ t.head
Tactic: cases a
Cleared hypotheses: a, dsm, dse, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α × WSeq α
dsm : some a ∈ s.destruct
dse : Prod.fst <$> some a = o
b : α × WSeq α
dtm : some b ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some a) (some b)
⊢ Prod.fst <$> some a ∈ t.head
have some : ∀ (a : α) (s' : WSeq α) (dsm : some (a, s') ∈ s.destruct) (dse : Prod.fst <$> some (a, s') = o)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some b)), Prod.fst <$> some (a, s') ∈ t.head
Tactic: obtain ⟨a, s'⟩ := a
Cleared hypotheses: a, dsm, dse, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
b : α × WSeq α
dtm : some b ∈ t.destruct
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some b)
⊢ Prod.fst <$> some (a, s') ∈ t.head
have some : ∀ (b : α) (t' : WSeq α) (dtm : some (b, t') ∈ t.destruct)
  (dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))), Prod.fst <$> some (a, s') ∈ t.head
Tactic: obtain ⟨b, t'⟩ := b
Cleared hypotheses: b, dtm, dst
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun (x1 x2 : WSeq α) ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ t.head
have some : Prod.fst <$> some (b, s') ∈ t.head
Tactic: rw [dst.left]
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten c ~ʷ s
have h1 : flatten (Computation.pure s) ~ʷ s
Tactic: apply Computation.memRecOn h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
h1 : flatten (Computation.pure s) ~ʷ s
⊢ flatten c ~ʷ s
have h2 : ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s
Tactic: apply Computation.memRecOn h
-- Lean 4 proof step from Mathlib.Data.WSeq.Relation (goal)
Goal:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s' ~ʷ s → flatten s'.think ~ʷ s
have h2 : flatten s'.think ~ʷ flatten s'
Tactic: apply Equiv.trans