awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
⊢ motive' s₁ s₂

Tactic:
grind
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
apply :
  ∀ (s₁ s₂ : Seq α),
    motive' s₁ s₂ →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'
⊢ s₁ = s₂

Tactic:
apply eq_of_bisim' motive' (by grind)

Premises used: Stream'.Seq.eq_of_bisim'
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive' s₁ s₂
simp :
  s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₂ = nil ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'

Tactic:
simp only [motive'] at ih ⊢
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : s₁ = s₂ ∨ motive s₁ s₂
inl :
  s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
inr :
  ∀ (ih : motive s₁ s₂),
    s₁ = nil ∧ s₂ = nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
rcases ih with (rfl | ih)

Premises used: rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
inl :
  Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
inl₁ :
  ∀ (x : α) (s : Seq α),
    cons x s = nil ∧ cons x s = nil ∨
      ∃ (x_1 : α),
        ∃ (s₁' : Seq α),
          ∃ (s₂' : Seq α), cons x s = cons x_1 s₁' ∧ cons x s = cons x_1 s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
cases s₁
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
⊢ Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
grind
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
x : α
s : Seq α
⊢ cons x s = nil ∧ cons x s = nil ∨
    ∃ (x_1 : α),
      ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), cons x s = cons x_1 s₁' ∧ cons x s = cons x_1 s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
grind
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
inr :
  ∀ (ih : motive s₁ s₁),
    s₁ = nil ∧ s₁ = nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
inr₁ :
  ∀ (hd : α) (s₁' s₂' : Seq α),
    s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂' →
      s₁ = nil ∧ s₂ = nil ∨
        ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
rcases step s₁ s₂ ih with (rfl | ⟨hd, s₁', s₂', _⟩)

Premises used: rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
ih : motive s₁ s₁
inr :
  ∀ (ih : motive nil nil),
    Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
      ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
inr₁ :
  ∀ (x : α) (s : Seq α) (ih : motive (cons x s) (cons x s)),
    cons x s = nil ∧ cons x s = nil ∨
      ∃ (x_1 : α),
        ∃ (s₁' : Seq α),
          ∃ (s₂' : Seq α), cons x s = cons x_1 s₁' ∧ cons x s = cons x_1 s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')
⊢ s₁ = nil ∧ s₁ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₁ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
cases s₁
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
ih : motive nil nil
⊢ Eq.{u + 1} (α := Seq α) nil nil ∧ Eq.{u + 1} (α := Seq α) nil nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
grind
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
x : α
s : Seq α
ih : motive (cons x s) (cons x s)
⊢ cons x s = nil ∧ cons x s = nil ∨
    ∃ (x_1 : α),
      ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), cons x s = cons x_1 s₁' ∧ cons x s = cons x_1 s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
grind
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s₁_1 s₂_1 : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁_1 s₂_1
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ →
      s₁ = s₂ ∨ ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun (s₁ s₂ : Seq α) ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
ih : motive s₁ s₂
hd : α
s₁' s₂' : Seq α
h : s₁ = cons hd s₁' ∧ s₂ = cons hd s₂' ∧ motive s₁' s₂'
⊢ s₁ = nil ∧ s₂ = nil ∨
    ∃ (x : α), ∃ (s₁' : Seq α), ∃ (s₂' : Seq α), s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
grind
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ f s = g s

Tactic:
eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) ?_ ⟨s, rfl, rfl⟩

Premises used: Stream'.Seq.eq_of_bisim, Exists, And, And.intro, Exists.intro, Eq, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
refine : IsBisimulation.{v} (α := β) fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s
⊢ f s = g s

Tactic:
refine eq_of_bisim (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) ?_ ⟨s, rfl, rfl⟩

Premises used: Stream'.Seq.eq_of_bisim, Exists, And, And.intro, Exists.intro, Eq, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
h : ∃ (s : Seq α), s1 = f s ∧ s2 = g s
rcases :
  ∀ (s : Seq α) (h1 : s1 = f s) (h2 : s2 = g s),
    BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Tactic:
rcases h with ⟨s, h1, h2⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
s_1 : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
rw : BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) s1.destruct s2.destruct

Tactic:
rw [h1, h2]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
s_1 : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
s : Seq α
h1 : s1 = f s
h2 : s2 = g s
⊢ BisimO (fun (s1 s2 : Seq β) ↦ ∃ (s : Seq α), s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct

Tactic:
apply H
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
none : Eq.{u + 1} (α := Option α) Option.none Option.none ↔ Option.isNone.{u} (α := α) Option.none = true
some : ∀ (val : α), Option.some val = Option.none ↔ (Option.some val).isNone = true
⊢ s.get? n = Option.none ↔ (s.get? n).isNone = true

Tactic:
cases s.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ Eq.{u + 1} (α := Option α) none none ↔ Option.isNone.{u} (α := α) none = true

Tactic:
simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
val : α
⊢ some val = none ↔ (some val).isNone = true

Tactic:
simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ ∀ (s : Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n

Tactic:
le_stable

Premises used: Stream'.Seq.le_stable, Stream'.Seq.TerminatedAt
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
⊢ ¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true

Tactic:
simp only [Terminates, TerminatedAt, ← Ne.eq_def, Option.ne_none_iff_isSome, not_exists, iff_self]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.Terminates, not_exists, Ne.eq_def, iff_self, Option.ne_none_iff_isSome
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
n : ℕ
⊢ TerminatedAt.{u} (α := α) nil n

Tactic:
rfl

Premises used: Stream'.Seq.TerminatedAt, Stream'.const, rfl, Stream'.Seq.get?
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
⊢ ¬(cons x s).TerminatedAt 0

Tactic:
simp [TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
⊢ (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n

Tactic:
simp [TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ Terminates.{u} (α := α) nil

Tactic:
⟨0, rfl⟩

Premises used: Stream'.Seq.Terminates, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
mp : (cons x s).Terminates → s.Terminates
mpr : s.Terminates → (cons x s).Terminates
⊢ (cons x s).Terminates ↔ s.Terminates

Tactic:
constructor
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates

Tactic:
⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩

Premises used: Stream'.Seq.cons_terminatedAt_succ_iff, Stream'.Seq.Terminates, Nat.le_succ, Exists.intro, Stream'.Seq.terminated_stable, Iff.mp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates

Tactic:
exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩

Premises used: Iff.mpr, Stream'.Seq.cons_terminatedAt_succ_iff, Stream'.Seq.Terminates, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 ↔ s = nil

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
refine_1 : s.TerminatedAt 0 → s = nil
refine_2 : s = nil → s.TerminatedAt 0
⊢ s.TerminatedAt 0 ↔ s = nil

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.TerminatedAt 0
refine_1 : ∀ (n : ℕ) (a : α), s.get? n = some a ↔ get? nil n = some a
⊢ s = nil

Tactic:
ext n
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a : α
refine_1 : none = some a ↔ get? nil n = some a
⊢ s.get? n = some a ↔ get? nil n = some a

Tactic:
rw [le_stable _ (Nat.zero_le _) h]

Premises used: Nat.zero_le, Stream'.Seq.le_stable
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a : α
⊢ none = some a ↔ get? nil n = some a

Tactic:
simp
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
⊢ TerminatedAt.{u} (α := α) nil 0

Tactic:
simp [TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
n : ℕ
x : α
h : s.get? n = some x
⊢ x ∈ s

Tactic:
⟨n, h.symm⟩

Premises used: Exists.intro, Stream'.Seq.Mem, Eq.symm, Stream'.Any
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : x ∈ s
⊢ some x ∈ (↑s : Stream' (Option α))

Tactic:
change (some x ∈ s.1) at h

Premises used: Option.some, Membership.mem, Subtype.val
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
s : Seq α
x : α
h : some x ∈ (↑s : Stream' (Option α))
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : ∃ (n : ℕ), some x = (↑s : Stream' (Option α)).get n), ∃ (i : ℕ), some x = s.get? i
⊢ ∃ (i : ℕ), some x = s.get? i

Tactic:
rwa [Stream'.mem_iff_exists_get_eq] at h

Premises used: Stream'.mem_iff_exists_get_eq
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
h_1 : Membership.mem (γ := Seq α) nil a
w : ℕ
h : some a = none
⊢ False

Tactic:
injection h
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a b : α
val : Stream' (Option α)
property : val.IsSeq
h_1 : a ∈ cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)
h : some a = some b
⊢ a = b

Tactic:
injection h
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a : α
s : Seq α
⊢ a ∈ cons a s

Tactic:
apply mem_cons

Premises used: Stream'.Seq.mem_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a b : α
s : Seq α
m : a ∈ s
⊢ a ∈ cons b s

Tactic:
mem_cons_of_mem _ m

Premises used: Stream'.Seq.mem_cons_of_mem
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
a b : α
s : Seq α
m : a ∈ s
⊢ a ∈ cons b s

Tactic:
exact mem_cons_of_mem _ m

Premises used: Stream'.Seq.mem_cons_of_mem
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
obtain : ∀ (k : ℕ) (e : some a = (↑s : Stream' (Option α)).get k), C s
⊢ C s

Tactic:
obtain ⟨k, e⟩ := M
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
a₁ : s.destruct = some (a, s.tail)
⊢ s = cons a s.tail

Tactic:
apply destruct_eq_cons

Premises used: Stream'.Seq.destruct_eq_cons
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
a₁ : instFunctorOption.1 (fun (a' : α) ↦ (a', s.tail)) (some a) = some (a, s.tail)
⊢ instFunctorOption.1 (fun (a' : α) ↦ (a', s.tail)) ((↑s : Stream' (Option α)) 0) = some (a, s.tail)

Tactic:
rw [← e]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
⊢ instFunctorOption.1 (fun (a' : α) ↦ (a', s.tail)) (some a) = some (a, s.tail)

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
zero : ∀ (TH : s = cons a s.tail), C s
⊢ C s

Tactic:
have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
TH : s = cons a s.tail
zero : C (cons a s.tail)
⊢ C s

Tactic:
rw [TH]
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = (↑s : Stream' (Option α)) 0
TH : s = cons a s.tail
⊢ C (cons a s.tail)

Tactic:
apply h1 _ _ (Or.inl rfl)

Premises used: Or.inl, rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
e : some a = (↑nil : Stream' (Option α)) (k + 1)
⊢ C nil

Tactic:
injection e
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
mk :
  ∀ (val : Stream' (Option α)) (property : val.IsSeq)
    (e :
      some a =
        (↑(cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α))
          (k + 1)),
    (↑(cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) k.succ =
      (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)) k
⊢ (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k

Tactic:
cases s' using Subtype.recOn
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
val : Stream' (Option α)
property : val.IsSeq
e :
  some a =
    (↑(cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) (k + 1)
⊢ (↑(cons b (Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property)) : Stream' (Option α)) k.succ =
    (↑(Subtype.mk (p := fun (f : Stream' (Option α)) ↦ f.IsSeq) val property) : Stream' (Option α)) k

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
succ : ∀ (h_eq : (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k), C (cons b s')
⊢ C (cons b s')

Tactic:
have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
h_eq : (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k
⊢ some a = (↑s' : Stream' (Option α)) k

Tactic:
rw [h_eq] at e
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)
h_eq : (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k
e₁ : some a = (↑s' : Stream' (Option α)) k
⊢ (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k

Tactic:
rw [h_eq] at e
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
b : α
s' : Seq α
e : some a = (↑s' : Stream' (Option α)) k
h_eq : (↑(cons b s') : Stream' (Option α)) k.succ = (↑s' : Stream' (Option α)) k
⊢ C (cons b s')

Tactic:
apply h1 _ _ (Or.inr (IH e))

Premises used: Or.inr
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s
s : Seq α
e : some a = (↑s : Stream' (Option α)) (k + 1)
succ : ∀ (e : some a = (↑nil : Stream' (Option α)) (k + 1)), C nil
succ₁ : ∀ (b : α) (s' : Seq α) (e : some a = (↑(cons b s') : Stream' (Option α)) (k + 1)), C (cons b s')
⊢ C s

Tactic:
cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))

Premises used: Stream'.Seq.nil, Stream'.Seq.cons, Or.inr
-- Module: Mathlib.Data.Seq.Defs
Goal:
α : Type u
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : some a = (↑s : Stream' (Option α)) k
zero : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) 0), C s
succ :
  ∀ (k : ℕ) (IH : ∀ {s : Seq α} (e : some a = (↑s : Stream' (Option α)) k), C s) {s : Seq α}
    (e : some a = (↑s : Stream' (Option α)) (k + 1)), C s
⊢ C s

Tactic:
induction k generalizing s with
  | zero =>
    have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
    rw [TH]
    apply h1 _ _ (Or.inl rfl)
  | succ k IH =>
    cases s with
    | nil => injection e
    | cons b s' =>
      have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
      rw [h_eq] at e
      apply h1 _ _ (Or.inr (IH e))

Premises used: Stream'.Seq.nil, Stream'.Seq.cons, Or.inl, rfl