awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c : Computation (WSeq α)
⊢ (flatten c).destruct = c >>= destruct
have c1 : Computation.IsBisimulation.{u} (α := Option (α × WSeq α)) fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
  c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
Tactic: refine
    Computation.eq_of_bisim
      (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct) ?_
      (Or.inr ⟨c, rfl, rfl⟩)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    c.destruct c.destruct
have inl : ∀ (val : Option (α × WSeq α)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (Sum.inl val) (Sum.inl val)
Tactic: cases c.destruct
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
inl :
  ∀ (val : Option (α × WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
      (Sum.inl val) (Sum.inl val)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    c.destruct c.destruct
have inr : ∀ (val : Computation (Option (α × WSeq α))),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (Sum.inr val) (Sum.inr val)
Tactic: cases c.destruct
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct
have pure : match (motive :=
  Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
  a.destruct.destruct, a.destruct.destruct with
| Sum.inl a, Sum.inl a' => a = a'
| Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
| x, x_1 => False
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
have pure : ∀ (val : Option (α × WSeq α)),
  match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    Sum.inl val, Sum.inl val with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
Tactic: cases (destruct a).destruct
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
pure :
  ∀ (val : Option (α × WSeq α)),
    match (motive :=
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
        Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
      Sum.inl val, Sum.inl val with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
    | x, x_1 => False
⊢ match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
have pure₁ : ∀ (val : Computation (Option (α × WSeq α))),
  match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    Sum.inr val, Sum.inr val with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
Tactic: cases (destruct a).destruct
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c).destruct.destruct (c.bind destruct).destruct
have pure : ∀ (a : WSeq α),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct
Tactic: induction c using Computation.recOn with
      | pure a => simp; cases (destruct a).destruct <;> simp
      | think c' => simpa using Or.inr ⟨c', rfl, rfl⟩
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (WSeq α)
pure :
  ∀ (a : WSeq α),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
      (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c).destruct.destruct (c.bind destruct).destruct
have think : ∀ (c' : Computation (WSeq α)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c'.think).destruct.destruct (c'.think.bind destruct).destruct
Tactic: induction c using Computation.recOn with
      | pure a => simp; cases (destruct a).destruct <;> simp
      | think c' => simpa using Or.inr ⟨c', rfl, rfl⟩
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := WSeq α) (drop nil n) nil
have zero : Eq.{u + 1} (α := WSeq α) (drop nil 0) nil
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
n : ℕ
zero : Eq.{u + 1} (α := WSeq α) (drop nil 0) nil
⊢ Eq.{u + 1} (α := WSeq α) (drop nil n) nil
have succ : ∀ (n : ℕ), Eq.{u + 1} (α := WSeq α) (drop nil n) nil → Eq.{u + 1} (α := WSeq α) (drop nil (n + 1)) nil
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
n : ℕ
⊢ (cons a s).drop (n + 1) = s.drop n
have zero : (cons a s).drop (HAdd.hAdd (α := ℕ) 0 1) = s.drop 0
Tactic: induction n with
  | zero => simp [drop]
  | succ n n_ih =>
    simp [drop, ← n_ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
n : ℕ
zero : (cons a s).drop (HAdd.hAdd (α := ℕ) 0 1) = s.drop 0
⊢ (cons a s).drop (n + 1) = s.drop n
have succ : ∀ (n : ℕ) (n_ih : (cons a s).drop (n + 1) = s.drop n), (cons a s).drop (n + 1 + 1) = s.drop (n + 1)
Tactic: induction n with
  | zero => simp [drop]
  | succ n n_ih =>
    simp [drop, ← n_ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ s.think.drop n = (s.drop n).think
have zero : s.think.drop 0 = (s.drop 0).think
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
n : ℕ
zero : s.think.drop 0 = (s.drop 0).think
⊢ s.think.drop n = (s.drop n).think
have succ : ∀ (n : ℕ), s.think.drop n = (s.drop n).think → s.think.drop (n + 1) = (s.drop (n + 1)).think
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)
have rw : s.tail.drop n = s.drop (1 + n)
Tactic: rw [Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
have symm : s.drop (1 + n) = s.tail.drop n
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
⊢ s.tail.destruct = s.destruct >>= tail.aux
have simp : (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o) <$>
      s.destruct >>=
    destruct =
  s.destruct >>= tail.aux
Tactic: simp only [tail, destruct_flatten]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
⊢ (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o) <$>
        s.destruct >>=
      destruct =
    s.destruct >>= tail.aux
have rw : (s.destruct >>= fun (x : Option (α × WSeq α)) ↦
    Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) : Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α)))) =
  s.destruct >>= tail.aux
Tactic: rw [← bind_pure_comp, LawfulMonad.bind_assoc]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
⊢ (s.destruct >>= fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α)))) =
    s.destruct >>= tail.aux
have h : Eq.{u + 1} (α := (x : Option (α × WSeq α)) → Computation (Option (α × WSeq α)))
  (fun (x : Option (α × WSeq α)) ↦
    Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) : Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))))
  tail.aux
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
⊢ Eq.{u + 1} (α := (x : Option (α × WSeq α)) → Computation (Option (α × WSeq α)))
    (fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α))))
    tail.aux
have h : Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
  (Bind.bind (α := WSeq α)
    (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none) : Computation (WSeq α))
    (destruct : WSeq α → Computation (Option (α × WSeq α))))
  (tail.aux none)
Tactic: ext1 (_ | ⟨a, s⟩)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
h :
  Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
    (Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))))
    (tail.aux none)
⊢ Eq.{u + 1} (α := (x : Option (α × WSeq α)) → Computation (Option (α × WSeq α)))
    (fun (x : Option (α × WSeq α)) ↦
      Bind.bind (α := WSeq α)
        (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd x) :
          Computation (WSeq α))
        (destruct : WSeq α → Computation (Option (α × WSeq α))))
    tail.aux
have h₁ : ∀ (a : α) (s : WSeq α),
  Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))) =
    tail.aux (some (a, s))
Tactic: ext1 (_ | ⟨a, s⟩)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
    (Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))))
    (tail.aux none)
have apply : Eq.{u + 1} (α := Computation (Option (α × WSeq α)))
  (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (tail.aux none)
Tactic: apply (@pure_bind Computation _ _ _ _ _ _).trans _
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s_1 : WSeq α
a : α
s : WSeq α
⊢ Bind.bind (α := WSeq α)
      (Pure.pure (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) :
        Computation (WSeq α))
      (destruct : WSeq α → Computation (Option (α × WSeq α))) =
    tail.aux (some (a, s))
have apply : destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some (a, s))) =
  tail.aux (some (a, s))
Tactic: apply (@pure_bind Computation _ _ _ _ _ _).trans _
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (Computation.bind (Computation.pure none) (aux n))
    (Computation.pure none)
have rw : Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (aux n none) (Computation.pure none)
Tactic: rw [ret_bind, drop.aux_none n]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
n : ℕ
rw : Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (aux n none) (Computation.pure none)
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (Computation.bind (Computation.pure none) (aux n))
    (Computation.pure none)
have rw₁ : Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (Computation.pure none) (Computation.pure none)
Tactic: rw [ret_bind, drop.aux_none n]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.drop (n + 1)).destruct = s.destruct >>= drop.aux (n + 1)
have rw : (s.destruct >>= fun (x : Option (α × WSeq α)) ↦ tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)
Tactic: rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
⊢ s.destruct.Terminates
have rcases : ∀ (a : Option (α × WSeq α)) (h : a ∈ s.tail.destruct), s.destruct.Terminates
Tactic: rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ s.destruct.Terminates
have h₁ : Membership.mem (γ := Computation (Option (α × WSeq α)))
  (do
    let a ← s.destruct
    destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
  a
Tactic: simp only [tail, destruct_flatten, bind_map_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h : a ∈ s.tail.destruct
⊢ s.destruct.Terminates
have h₁ : Membership.mem (γ := Computation (Option (α × WSeq α)))
  (do
    let a ← s.destruct
    destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
  a
Tactic: simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
T : s.tail.head.Terminates
a : Option (α × WSeq α)
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (do
      let a ← s.destruct
      destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd a))
    a
⊢ s.destruct.Terminates
have rcases : ∀ (s' : Option (α × WSeq α)) (h1 : s' ∈ s.destruct),
  Membership.mem (γ := Computation (Option (α × WSeq α)))
      (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd s')) a →
    s.destruct.Terminates
Tactic: rcases exists_of_mem_bind h with ⟨s', h1, _⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct
      (flatten
        ((Applicative.toFunctor : Functor Computation).1
          (fun (o : Option (α × WSeq α)) ↦
            Option.recOn (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) o nil Prod.snd)
          s.destruct)))
    (some a)
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have h₁ : Membership.mem (γ := Computation (Option (α × WSeq α)))
  ((Applicative.toFunctor : Functor Computation).1
      (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      s.destruct >>=
    destruct)
  (some a)
Tactic: simp only [destruct_flatten] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
h :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    ((Applicative.toFunctor : Functor Computation).1
        (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
        s.destruct >>=
      destruct)
    (some a)
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have rcases : ∀ (t : WSeq α)
  (tm :
    Membership.mem (γ := Computation (WSeq α))
      ((Applicative.toFunctor : Functor Computation).1
        (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
        s.destruct)
      t)
  (td : some a ∈ t.destruct), ∃ (a' : α × WSeq α), some a' ∈ s.destruct
Tactic: rcases exists_of_mem_bind h with ⟨t, tm, td⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
tm :
  Membership.mem (γ := Computation (WSeq α))
    ((Applicative.toFunctor : Functor Computation).1
      (fun (o : Option (α × WSeq α)) ↦ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd o)
      s.destruct)
    t
td : some a ∈ t.destruct
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have rcases : ∀ (t' : Option (α × WSeq α)) (ht' : t' ∈ s.destruct)
  (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd t' = t),
  ∃ (a' : α × WSeq α), some a' ∈ s.destruct
Tactic: rcases Computation.exists_of_mem_map tm with ⟨t', ht', ht2⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd t' = t
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have none : ∀ (ht' : none ∈ s.destruct) (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t),
  ∃ (a' : α × WSeq α), some a' ∈ s.destruct
Tactic: rcases t' with - | t'
Cleared hypotheses: t', ht', ht2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : Option (α × WSeq α)
ht' : t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd t' = t
none :
  ∀ (ht' : Option.none ∈ s.destruct)
    (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd Option.none = t),
    ∃ (a' : α × WSeq α), some a' ∈ s.destruct
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have some : ∀ (t' : α × WSeq α) (ht' : some t' ∈ s.destruct)
  (ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t),
  ∃ (a' : α × WSeq α), some a' ∈ s.destruct
Tactic: rcases t' with - | t'
Cleared hypotheses: t', ht', ht2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have td₁ : Membership.mem (γ := Computation (Option (α × WSeq α)))
  (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (some a)
Tactic: rw [← ht2] at td
Cleared hypotheses: td, ht', ht2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td : some a ∈ t.destruct
t' : α × WSeq α
ht' : some t' ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t') = t
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have td₁ : Membership.mem (γ := Computation (Option (α × WSeq α)))
  (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd (some t'))) (some a)
Tactic: rw [← ht2] at td
Cleared hypotheses: td, ht', ht2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
td :
  Membership.mem (γ := Computation (Option (α × WSeq α)))
    (destruct (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none)) (some a)
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have td₁ : Membership.mem (γ := Computation (Option (α × WSeq α))) (Computation.pure none) (some a)
Tactic: simp only [destruct_nil] at td
Cleared hypotheses: td
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd none = t
td : Membership.mem (γ := Computation (Option (α × WSeq α))) (Computation.pure none) (some a)
⊢ ∃ (a' : α × WSeq α), some a' ∈ s.destruct
have this : some a = none
Tactic: have := mem_unique td (ret_mem _)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h :
  Membership.mem (γ := Computation (Option α))
    (Computation.map (fun (x : Option (α × WSeq α)) ↦ Prod.fst <$> x) s.tail.destruct) (some a)
⊢ ∃ (a' : α), some a' ∈ s.head
have rcases : ∀ (o : Option (α × WSeq α)) (md : o ∈ s.tail.destruct) (e : Prod.fst <$> o = some a), ∃ (a' : α), some a' ∈ s.head
Tactic: rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩