awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h h' : (cons x s).Terminates
⊢ s.Terminates

Tactic:
rw [terminates_cons_iff] at h'

Premises used: Stream'.Seq.terminates_cons_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h h' : ¬(cons x s).Terminates
⊢ ¬s.Terminates

Tactic:
rw [terminates_cons_iff] at h'

Premises used: Stream'.Seq.terminates_cons_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
simp [length'_of_terminates h, length'_of_terminates h', length_cons h']

Premises used: Stream'.Seq.length'_of_terminates, Stream'.Seq.length_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
simp [length'_of_not_terminates h, length'_of_not_terminates h']

Premises used: Stream'.Seq.length'_of_not_terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
h : s.Terminates
⊢ s.length h = 0 ↔ s = nil

Tactic:
simp [length, TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.length
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
nil : length'.{u} (α := α) Seq.nil = 0 ↔ Eq.{u + 1} (α := Seq α) Seq.nil Seq.nil
cons : ∀ (x : α) (s : Seq α), (Seq.cons x s).length' = 0 ↔ Seq.cons x s = Seq.nil
⊢ s.length' = 0 ↔ s = Seq.nil

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ length'.{u} (α := α) nil = 0 ↔ Eq.{u + 1} (α := Seq α) nil nil

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
⊢ (cons x s).length' = 0 ↔ cons x s = nil

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
nil : length'.{u} (α := α) Seq.nil ≠ 0 ↔ ∃ (x : α) (s' : Seq α), Seq.nil = Seq.cons x s'
cons : ∀ (x : α) (s : Seq α), (Seq.cons x s).length' ≠ 0 ↔ ∃ (x_1 : α) (s' : Seq α), Seq.cons x s = Seq.cons x_1 s'
⊢ s.length' ≠ 0 ↔ ∃ (x : α) (s' : Seq α), s = Seq.cons x s'

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ length'.{u} (α := α) nil ≠ 0 ↔ ∃ (x : α) (s' : Seq α), nil = cons x s'

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
⊢ (cons x s).length' ≠ 0 ↔ ∃ (x_1 : α) (s' : Seq α), cons x s = cons x_1 s'

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
simp : ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none
⊢ (∃ (h : s.Terminates), s.length h ≤ n) ↔ s.TerminatedAt n

Tactic:
simp only [length, Nat.find_le_iff, TerminatedAt, Terminates, exists_prop]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.Terminates, Stream'.Seq.length, exists_prop, Nat.find_le_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
refine_1 : ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none
refine_2 : s.get? n = none → (∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none
⊢ ((∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) ↔ s.get? n = none

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
left : ∃ (n : ℕ), s.get? n = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ s.get? n = none

Tactic:
le_stable s hkn hk

Premises used: Stream'.Seq.le_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
left : ∃ (n : ℕ), s.get? n = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ s.get? n = none

Tactic:
exact le_stable s hkn hk

Premises used: Stream'.Seq.le_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
hn : s.get? n = none
⊢ (∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none

Tactic:
⟨⟨n, hn⟩, ⟨n, le_rfl, hn⟩⟩

Premises used: le_rfl, And.intro, Exists.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
hn : s.get? n = none
⊢ (∃ (n : ℕ), s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none

Tactic:
exact ⟨⟨n, hn⟩, ⟨n, le_rfl, hn⟩⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
rw : s.length h ≤ n ↔ ∃ (h : s.Terminates), s.length h ≤ n
⊢ s.length h ≤ n ↔ s.TerminatedAt n

Tactic:
rw [← length_le_iff']

Premises used: Stream'.Seq.length_le_iff'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ ∃ (h : s.Terminates), s.length h ≤ n

Tactic:
simp [h]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
pos : ∀ (h : s.Terminates), s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
neg : ∀ (h : ¬s.Terminates), s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n
⊢ s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n

Tactic:
by_cases h : s.Terminates

Premises used: Stream'.Seq.Terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n

Tactic:
simpa [length'_of_terminates h] using length_le_iff

Premises used: Stream'.Seq.length_le_iff, Stream'.Seq.length'_of_terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ (↑n : ℕ∞) ↔ s.TerminatedAt n

Tactic:
simpa [length'_of_not_terminates h] using forall_not_of_not_exists h n

Premises used: forall_not_of_not_exists, Stream'.Seq.length'_of_not_terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
simp : (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) ↔ ¬s.get? n = none
⊢ (∀ (h : s.Terminates), n < s.length h) ↔ ∃ (a : α), a ∈ s.get? n

Tactic:
simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
    ← Option.ne_none_iff_exists', ne_eq]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.Terminates, Option.ne_none_iff_exists', forall_exists_index, Stream'.Seq.length, ne_eq, Nat.lt_find_iff, Option.mem_def
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) ↔ ¬s.get? n = none

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
refine_1 : (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) → ¬s.get? n = none
refine_2 : ¬s.get? n = none → ∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none
⊢ (∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none) ↔ ¬s.get? n = none

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none
hn : s.get? n = none
⊢ False

Tactic:
h n hn n le_rfl hn

Premises used: le_rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none
hn : s.get? n = none
⊢ False

Tactic:
exact h n hn n le_rfl hn

Premises used: le_rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
refine_2 : ∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none
⊢ ∀ (x : ℕ) (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none

Tactic:
_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x : ℕ
refine_2 : s.get? x = none → ∀ m ≤ n, ¬s.get? m = none
⊢ ∀ (h : s.get? x = none), ∀ m ≤ n, ¬s.get? m = none

Tactic:
_
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x : ℕ
h : s.get? x = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ False

Tactic:
hn <| le_stable s hkn hk

Premises used: Stream'.Seq.le_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x : ℕ
h : s.get? x = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ False

Tactic:
exact hn <| le_stable s hkn hk

Premises used: Stream'.Seq.le_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
rw : n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h
⊢ n < s.length h ↔ ∃ (a : α), a ∈ s.get? n

Tactic:
rw [← lt_length_iff']

Premises used: Stream'.Seq.lt_length_iff'
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h

Tactic:
simp [h]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
pos : ∀ (h : s.Terminates), (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
neg : ∀ (h : ¬s.Terminates), (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n
⊢ (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n

Tactic:
by_cases h : s.Terminates

Premises used: Stream'.Seq.Terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n

Tactic:
simpa [length'_of_terminates h] using lt_length_iff

Premises used: Stream'.Seq.lt_length_iff, Stream'.Seq.length'_of_terminates
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
neg : ∃ (a : α), s.get? n = some a
⊢ (↑n : ℕ∞) < s.length' ↔ ∃ (a : α), a ∈ s.get? n

Tactic:
simp only [length'_of_not_terminates h, ENat.coe_lt_top, Option.mem_def, true_iff]

Premises used: true_iff, Stream'.Seq.length'_of_not_terminates, Option.mem_def, ENat.coe_lt_top
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ∀ (n : ℕ), (s.get? n).isSome = true

Tactic:
rw [not_terminates_iff] at h

Premises used: Stream'.Seq.not_terminates_iff
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
neg : (s.get? n).isSome = true
⊢ ∃ (a : α), s.get? n = some a

Tactic:
rw [← Option.isSome_iff_exists]

Premises used: Option.isSome_iff_exists
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ (s.get? n).isSome = true

Tactic:
h n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
n : ℕ
h : ∀ (n : ℕ), (s.get? n).isSome = true
⊢ (s.get? n).isSome = true

Tactic:
exact h n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Stream' α
a₁ : (↑(↑(a :: s) : Seq α) : Stream' (Option α)) = (↑(cons a (↑s : Seq α)) : Stream' (Option α))
⊢ (↑(a :: s) : Seq α) = cons a (↑s : Seq α)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
a : α
s : Stream' α
a₁ a₂ : some a :: Stream'.map some s = some a :: Stream'.map some s
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s

Tactic:
rw [Stream'.map_cons]

Premises used: Stream'.map_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l : List α
⊢ (↑l : Seq α).TerminatedAt l.length

Tactic:
simp [ofList, TerminatedAt]

Premises used: Stream'.Seq.TerminatedAt, Stream'.Seq.ofList
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
l : List α
⊢ (↑l : Seq α).Terminates

Tactic:
⟨_, terminatedAt_ofList l⟩

Premises used: Stream'.Seq.Terminates, Exists.intro, Stream'.Seq.terminatedAt_ofList
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
zero : Eq.{u + 1} (α := List α) (take 0 nil) []
succ : ∀ (n : ℕ), Eq.{u + 1} (α := List α) (take (n + 1) nil) []
⊢ Eq.{u + 1} (α := List α) (take n nil) []

Tactic:
cases n
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List α) (take 0 nil) []

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := List α) (take (n + 1) nil) []

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
nil : Eq.{u + 1} (α := List α) (take 0 Seq.nil) []
cons : ∀ (x : α) (s : Seq α), take 0 (Seq.cons x s) = []
⊢ take 0 s = []

Tactic:
cases s
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
⊢ take 0 (cons x s) = []

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
x : α
s : Seq α
⊢ take (n + 1) (cons x s) = x :: take n s

Tactic:
rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n : ℕ
s : Seq α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take 0 s) n = if n < 0 then s.get? n else none

Tactic:
simp [take]

Premises used: Stream'.Seq.take
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
rw :
  getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) s.destruct with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take (k + 1) s) n =
    if n < k + 1 then s.get? n else none

Tactic:
rw [take]

Premises used: Stream'.Seq.take
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
h : s.destruct = none
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) none with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none

Tactic:
simp [destruct_eq_none h]

Premises used: Stream'.Seq.destruct_eq_none
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
rw :
  getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then (cons x r).get? n else none
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none

Tactic:
rw [destruct_eq_cons h]

Premises used: Stream'.Seq.destruct_eq_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ getElem? (coll := List α) (idx := ℕ) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      0 =
    if 0 < k + 1 then (cons x r).get? 0 else none

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n_1 k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
n : ℕ
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      (n + 1) =
    if n + 1 < k + 1 then (cons x r).get? (n + 1) else none

Tactic:
simp [List.getElem?_cons_succ, getElem?_take]

Premises used: List.getElem?_cons_succ
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
x : α
r : Seq α
h : s.destruct = some (x, r)
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some (x, r) with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then (cons x r).get? n else none

Tactic:
match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
a : Seq1 α
h : s.destruct = some a
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) some a with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none

Tactic:
match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
n k : ℕ
s : Seq α
cases :
  ∀ (x : Option (Seq1 α)) (h : s.destruct = x),
    getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
        (match (motive := Option (Seq1 α) → List α) x with
          | none => []
          | some (x, r) => x :: take k r :
          List α)
        n =
      if n < k + 1 then s.get? n else none
⊢ getElem? (coll := List α) (valid := fun (as : List α) (i : ℕ) ↦ i < as.length)
      (match (motive := Option (Seq1 α) → List α) s.destruct with
        | none => []
        | some (x, r) => x :: take k r :
        List α)
      n =
    if n < k + 1 then s.get? n else none

Tactic:
cases h : destruct s with
    | none =>
      simp [destruct_eq_none h]
    | some a =>
      match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]

Premises used: Option.some, Option.none, Stream'.Seq.destruct
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
zero : ∀ (l : ℕ) (hl : l + 1 = n), x ∈ take n s
⊢ x ∈ take n s

Tactic:
obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn

Premises used: Iff.mpr, Nat.exists_add_one_eq
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
zero :
  Membership.mem (γ := List α)
    (match (motive := Option (Seq1 α) → List α) (cons x s.tail).destruct with
      | none => []
      | some (x, r) => x :: take l r :
      List α)
    x
⊢ x ∈ take n s

Tactic:
rw [← hl, take, head_eq_some h_get]

Premises used: Stream'.Seq.take, Stream'.Seq.head_eq_some
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ Membership.mem (γ := List α)
    (match (motive := Option (Seq1 α) → List α) (cons x s.tail).destruct with
      | none => []
      | some (x, r) => x :: take l r :
      List α)
    x

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
n : ℕ
h_mn : k + 1 < n
h_get : s.get? (k + 1) = some x
succ : ∀ (l : ℕ) (h_mn : k + 1 < k + 1 + l + 1), x ∈ take (k + 1 + l + 1) s
⊢ x ∈ take n s

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt h_mn

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
apply : 0 ≤ k + 1
⊢ ∃ (y : α), s.get? 0 = some y

Tactic:
apply ge_stable _ _ h_get

Premises used: Stream'.Seq.ge_stable
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
⊢ 0 ≤ k + 1

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
⊢ ∃ (y : α), s.get? 0 = some y

Tactic:
have : ∃ y, s.get? 0 = some y := by
      apply ge_stable _ _ h_get
      simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
this : ∃ (y : α), s.get? 0 = some y
succ : ∀ (y : α) (hy : s.get? 0 = some y), x ∈ take (k + 1 + l + 1) s
⊢ x ∈ take (k + 1 + l + 1) s

Tactic:
obtain ⟨y, hy⟩ := this
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
succ :
  Membership.mem (γ := List α)
    (match (motive := Option (Seq1 α) → List α) (cons y s.tail).destruct with
      | none => []
      | some (x, r) => x :: take (k + 1 + l) r :
      List α)
    x
⊢ x ∈ take (k + 1 + l + 1) s

Tactic:
rw [take, head_eq_some hy]

Premises used: Stream'.Seq.take, Stream'.Seq.head_eq_some
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
succ : x = y ∨ x ∈ take (k + 1 + l) s.tail
⊢ Membership.mem (γ := List α)
    (match (motive := Option (Seq1 α) → List α) (cons y s.tail).destruct with
      | none => []
      | some (x, r) => x :: take (k + 1 + l) r :
      List α)
    x

Tactic:
simp only [destruct_cons, List.mem_cons]

Premises used: Stream'.Seq.destruct_cons, List.mem_cons
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
succ : x ∈ take (k + 1 + l) s.tail
⊢ x = y ∨ x ∈ take (k + 1 + l) s.tail

Tactic:
right
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ k < k + 1 + l

Tactic:
lia
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
succ : s.tail.get? k = some x
⊢ x ∈ take (k + 1 + l) s.tail

Tactic:
apply ih (by lia)
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
succ succ₁ succ₂ succ₃ : s.get? (k + 1) = some x
⊢ s.tail.get? k = some x

Tactic:
rwa [get?_tail]

Premises used: Stream'.Seq.get?_tail
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
m n : ℕ
h_mn : m < n
x : α
h_get : s.get? m = some x
zero : ∀ {s : Seq α} {n : ℕ} (h_mn : 0 < n) (h_get : s.get? 0 = some x), x ∈ take n s
succ :
  ∀ (k : ℕ) (ih : ∀ {s : Seq α} {n : ℕ} (h_mn : k < n) (h_get : s.get? k = some x), x ∈ take n s) {s : Seq α} {n : ℕ}
    (h_mn : k + 1 < n) (h_get : s.get? (k + 1) = some x), x ∈ take n s
⊢ x ∈ take n s

Tactic:
induction m generalizing n s with
  | zero =>
    obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
    rw [← hl, take, head_eq_some h_get]
    simp
  | succ k ih =>
    obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_lt h_mn
    have : ∃ y, s.get? 0 = some y := by
      apply ge_stable _ _ h_get
      simp
    obtain ⟨y, hy⟩ := this
    rw [take, head_eq_some hy]
    simp only [destruct_cons, List.mem_cons]
    right
    apply ih (by lia)
    rwa [get?_tail]

Premises used: Iff.mpr, Stream'.Seq.get?_tail, Stream'.Seq.take, Nat.exists_add_one_eq, Stream'.Seq.destruct_cons, List.mem_cons, Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s : Seq α
⊢ (take 0 s).length ≤ 0

Tactic:
simp
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
succ :
  List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) s.destruct with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1
⊢ (take (m + 1) s).length ≤ m + 1

Tactic:
rw [take]

Premises used: Stream'.Seq.take
-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ List.length.{u} (α := α)
      (match (motive := Option (Seq1 α) → List α) none with
      | none => []
      | some (x, r) => x :: take m r) ≤
    m + 1

Tactic:
simp