awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ (a' : α), some a' ∈ s.head
have none : ∀ (md : none ∈ s.tail.destruct) (e : Functor.map (α := α × WSeq α) Prod.fst none = some a), ∃ (a' : α), some a' ∈ s.head
Tactic: rcases o with - | o
Cleared hypotheses: o, md, e
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
none :
  ∀ (md : Option.none ∈ s.tail.destruct) (e : Functor.map (α := α × WSeq α) Prod.fst Option.none = some a),
    ∃ (a' : α), some a' ∈ s.head
⊢ ∃ (a' : α), some a' ∈ s.head
have some : ∀ (o : α × WSeq α) (md : some o ∈ s.tail.destruct) (e : Prod.fst <$> some o = some a), ∃ (a' : α), some a' ∈ s.head
Tactic: rcases o with - | o
Cleared hypotheses: o, md, e
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
e : Prod.fst <$> some o = some a
⊢ ∃ (a' : α), some a' ∈ s.head
have h' : o.1 = a
Tactic: injection e with h'
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ (a' : α), some a' ∈ s.head
have some : ∀ (o : α × WSeq α) (md : some o ∈ s.tail.destruct) (h' : o.1 = a), ∃ (a' : α), some a' ∈ s.head
Tactic: rcases o with - | o <;> [injection e; injection e with h']
Cleared hypotheses: o, md, e
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
⊢ ∃ (a' : α), some a' ∈ s.head
have some : ∀ (a : α × WSeq α) (am : some a ∈ s.destruct), ∃ (a' : α), some a' ∈ s.head
Tactic: obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α} (h : some a ∈ s.get? n), ∃ (a' : α), some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
⊢ ∃ (a' : α), some a' ∈ s.head
have succ : ∀ (a' : α) (h' : some a' ∈ (s.drop n).head), ∃ (a' : α), some a' ∈ s.head
Tactic: let ⟨a', h'⟩ := head_some_of_head_tail_some h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ (a' : α), some a' ∈ s.head
have zero : ∀ {a : α} (h : some a ∈ s.get? 0), ∃ (a' : α), some a' ∈ s.head
Tactic: induction n generalizing a with
  | zero => exact ⟨_, h⟩
  | succ n IH =>
      let ⟨a', h'⟩ := head_some_of_head_tail_some h
      exact IH h'
Cleared hypotheses: a, n, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
n : ℕ
h : some a ∈ s.get? n
zero : ∀ {a : α} (h : some a ∈ s.get? 0), ∃ (a' : α), some a' ∈ s.head
⊢ ∃ (a' : α), some a' ∈ s.head
have succ : ∀ (n : ℕ) (IH : ∀ {a : α} (h : some a ∈ s.get? n), ∃ (a' : α), some a' ∈ s.head) {a : α} (h : some a ∈ s.get? (n + 1)),
  ∃ (a' : α), some a' ∈ s.head
Tactic: induction n generalizing a with
  | zero => exact ⟨_, h⟩
  | succ n IH =>
      let ⟨a', h'⟩ := head_some_of_head_tail_some h
      exact IH h'
Cleared hypotheses: a, n, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
⊢ (s.get? n).Terminates → (s.get? m).Terminates
have refl : (s.get? m).Terminates → (s.get? m).Terminates
Tactic: induction h with
  | refl => exact id
  | step _ IH => exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
m n : ℕ
h : m ≤ n
refl : (s.get? m).Terminates → (s.get? m).Terminates
⊢ (s.get? n).Terminates → (s.get? m).Terminates
have step : ∀ {m_1 : ℕ},
  m.le m_1 →
    ∀ (IH : (s.get? m_1).Terminates → (s.get? m).Terminates), (s.get? m_1.succ).Terminates → (s.get? m).Terminates
Tactic: induction h with
  | refl => exact id
  | step _ IH => exact fun T ↦ IH (@head_terminates_of_head_tail_terminates _ _ T)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
⊢ C s
have apply : ∀ (b : Option α) (s' : Seq (Option α)), some a = b ∨ C s' → C (Seq.cons b s')
Tactic: apply Seq.mem_rec_on M
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
s' : Seq (Option α)
h : some a = o ∨ C s'
⊢ C (Seq.cons o s')
have none : ∀ (h : some a = none ∨ C s'), C (Seq.cons none s')
Tactic: rcases o with - | b
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
o : Option α
s' : Seq (Option α)
h : some a = o ∨ C s'
none : ∀ (h : some a = Option.none ∨ C s'), C (Seq.cons Option.none s')
⊢ C (Seq.cons o s')
have some : ∀ (b : α) (h : some a = some b ∨ C s'), C (Seq.cons (some b) s')
Tactic: rcases o with - | b
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C (Seq.cons none s')
have none : C s'
Tactic: apply h2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = none ∨ C s'
⊢ C s'
have none : some a = none → C s'
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
h : some a = Option.none ∨ C s'
none : some a = Option.none → C s'
⊢ C s'
have none₁ : C s' → C s'
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ C (Seq.cons (some b) s')
have some : a = b ∨ C s'
Tactic: apply h1
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h : some a = some b ∨ C s'
⊢ a = b ∨ C s'
have apply : some a = some b → a = b
Tactic: apply Or.imp_left _ h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
⊢ a ∈ s.think ↔ a ∈ s
have obtain : ∀ (f : Stream' (Option (Option α))) (al : f.IsSeq),
  a ∈ think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al) ↔
    a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al
Tactic: obtain ⟨f, al⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ a ∈ think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al) ↔
    a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) f al
have change : some (some a) ∈ some none :: f ↔ some (some a) ∈ f
Tactic: change (some (some a) ∈ some none::f) ↔ some (some a) ∈ f
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f
have mp : some (some a) ∈ some none :: f → some (some a) ∈ f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
mp : some (some a) ∈ some none :: f → some (some a) ∈ f
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f
have mpr : some (some a) ∈ f → some (some a) ∈ some none :: f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f
have mp : ¬some (some a) = some none
Tactic: apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
⊢ some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')
have generalize : ∀ (c : Computation (Option (α × WSeq α))) (e : s.destruct = c), some (a', s') ∈ c → (a ∈ s ↔ a = a' ∨ a ∈ s')
Tactic: generalize e : destruct s = c
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
e : s.destruct = c
h : some (a', s') ∈ c
⊢ a ∈ s ↔ a = a' ∨ a ∈ s'
have revert : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
Tactic: revert s
Cleared hypotheses: s, e
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
have h1 : ∀ {s : WSeq α} (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
Tactic: apply Computation.memRecOn h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
h1 : ∀ {s : WSeq α} (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
⊢ ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
have h2 : ∀ (s : Computation (Option (α × WSeq α))),
  (∀ {s_1 : WSeq α} (e : s_1.destruct = s), a ∈ s_1 ↔ a = a' ∨ a ∈ s') →
    ∀ {s_1 : WSeq α} (e : s_1.destruct = s.think), a ∈ s_1 ↔ a = a' ∨ a ∈ s'
Tactic: apply Computation.memRecOn h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
have h1 : ∀ {s : WSeq α} (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
Tactic: apply Computation.memRecOn h <;> [skip; intro c IH]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
h1 : ∀ {s : WSeq α} (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
⊢ ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
have h2 : ∀ (c : Computation (Option (α × WSeq α))) (IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s')
  {s : WSeq α} (e : s.destruct = c.think), a ∈ s ↔ a = a' ∨ a ∈ s'
Tactic: apply Computation.memRecOn h <;> [skip; intro c IH]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
⊢ ∀ (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
have h1 : ∀ (e : destruct nil = Computation.pure (some (a', s'))), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
h1 : ∀ (e : destruct nil = Computation.pure (some (a', s'))), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
⊢ ∀ (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
have h1₁ : ∀ (x : α) (s : WSeq α) (e : (cons x s).destruct = Computation.pure (some (a', s'))), a ∈ cons x s ↔ a = a' ∨ a ∈ s'
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
h1 : ∀ (e : destruct nil = Computation.pure (some (a', s'))), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
h1₁ :
  ∀ (x : α) (s : WSeq α) (e : (cons x s).destruct = Computation.pure (some (a', s'))), a ∈ cons x s ↔ a = a' ∨ a ∈ s'
⊢ ∀ (e : s.destruct = Computation.pure (some (a', s'))), a ∈ s ↔ a = a' ∨ a ∈ s'
have h1₂ : ∀ (s : WSeq α) (e : s.think.destruct = Computation.pure (some (a', s'))), a ∈ s.think ↔ a = a' ∨ a ∈ s'
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
⊢ ∀ (e : s.destruct = c.think), a ∈ s ↔ a = a' ∨ a ∈ s'
have h2 : ∀ (e : destruct nil = c.think), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
h2 : ∀ (e : destruct nil = c.think), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
⊢ ∀ (e : s.destruct = c.think), a ∈ s ↔ a = a' ∨ a ∈ s'
have h2₁ : ∀ (x : α) (s : WSeq α) (e : (cons x s).destruct = c.think), a ∈ cons x s ↔ a = a' ∨ a ∈ s'
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
h2 : ∀ (e : destruct nil = c.think), Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
h2₁ : ∀ (x : α) (s : WSeq α) (e : (cons x s).destruct = c.think), a ∈ cons x s ↔ a = a' ∨ a ∈ s'
⊢ ∀ (e : s.destruct = c.think), a ∈ s ↔ a = a' ∨ a ∈ s'
have h2₂ : ∀ (s : WSeq α) (e : s.think.destruct = c.think), a ∈ s.think ↔ a = a' ∨ a ∈ s'
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : destruct nil = Computation.pure (some (a', s'))
⊢ Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
have this : Computation.destruct (destruct nil) = (Computation.pure (some (a', s'))).destruct
Tactic: have := congr_arg Computation.destruct m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
have this : (cons x s).destruct.destruct = (Computation.pure (some (a', s'))).destruct
Tactic: have := congr_arg Computation.destruct m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s : WSeq α
m : s.think.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s.think ↔ a = a' ∨ a ∈ s'
have this : s.think.destruct.destruct = (Computation.pure (some (a', s'))).destruct
Tactic: have := congr_arg Computation.destruct m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
m : destruct nil = c.think
⊢ Membership.mem (γ := WSeq α) nil a ↔ a = a' ∨ a ∈ s'
have this : Computation.destruct (destruct nil) = c.think.destruct
Tactic: have := congr_arg Computation.destruct m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
x : α
s : WSeq α
m : (cons x s).destruct = c.think
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
have this : (cons x s).destruct.destruct = c.think.destruct
Tactic: have := congr_arg Computation.destruct m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
m : s.think.destruct = c.think
⊢ a ∈ s.think ↔ a = a' ∨ a ∈ s'
have this : s.think.destruct.destruct = c.think.destruct
Tactic: have := congr_arg Computation.destruct m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : (cons x s).destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
have this₁ : x = a' ∧ s = s'
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c_1 : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c_1
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α} (e : s.destruct = c), a ∈ s ↔ a = a' ∨ a ∈ s'
s : WSeq α
m : s.think.destruct = c.think
this : s.think.destruct.destruct = c.think.destruct
⊢ a ∈ s.think ↔ a = a' ∨ a ∈ s'
have this₁ : s.destruct = c
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
have i1 : x = a'
Tactic: obtain ⟨i1, i2⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
this : x = a' ∧ s = s'
i1 : x = a'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
have i2 : s = s'
Tactic: obtain ⟨i1, i2⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ a ∈ cons x s ↔ a = a' ∨ a ∈ s'
have h1 : a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'
Tactic: rw [i1, i2]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α)))) ↔
    a = a' ∨ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
have h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
Tactic: have h_a_eq_a' : a = a' ↔ some (some a) = some (some a') := by simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α)))) ↔
    a = a' ∨ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
have h1 : Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α)))) ↔
  some (some a) = some (some a') ∨
    Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
Tactic: rw [h_a_eq_a']
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α)))) ↔
    some (some a) = some (some a') ∨
      Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
have h1 : ∀
  (o :
    some (some a) = some (some a') ∨
      Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))),
  Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
Tactic: refine ⟨Stream'.eq_or_mem_of_mem_cons, fun o => ?_⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
o :
  some (some a) = some (some a') ∨
    Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
have h1 : ∀ (e : some (some a) = some (some a')),
  Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
Tactic: rcases o with e | m
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
o :
  some (some a) = some (some a') ∨
    Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))
h1 :
  ∀ (e : some (some a) = some (some a')),
    Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
have h1₁ : ∀ (m : Any (fun (b : Option (Option α)) ↦ some (some a) = b) (↑s' : Stream' (Option (Option α)))),
  Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
Tactic: rcases o with e | m
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x : α
s : WSeq α
m : (cons x s).destruct = Computation.pure (some (a', s'))
i1 : x = a'
i2 : s = s'
h_a_eq_a' : a = a' ↔ some (some a) = some (some a')
e : some (some a) = some (some a')
⊢ Any (fun (b : Option (Option α)) ↦ some (some a) = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
have h1 : Any (fun (b : Option (Option α)) ↦ some (some a') = b) (some (some a') :: (↑s' : Stream' (Option (Option α))))
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h this : a ∈ s.tail
⊢ a ∈ s
have obtain : ∀ (n : ℕ) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))).get n), a ∈ s
Tactic: obtain ⟨n, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
this : a ∈ s.tail
n : ℕ
e : some (some a) = (↑s.tail : Stream' (Option (Option α))).get n
⊢ a ∈ s
have revert : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))).get n), a ∈ s
Tactic: revert s
Cleared hypotheses: s, this, e