mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ corec f g a = f a :: corec f g (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
⊢ corec id id a = const a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
g : α → β
f : α → α
a : α
⊢ unfolds g f a = g a :: unfolds g f (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s s' : Computation α
⊢ s.destruct = Sum.inr s' → s = s'.think

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ (unfolds head tail s).get n = s.get n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : Computation α
a : Stream' (Option α)
s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1
H : s.destruct = Sum.inr ⟨a, s'⟩
⊢ motive s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
⊢ Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd) (n + 1) = some a'

Tactic:
change Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).2 n = some a'

Goal state after:
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
n : ℕ
a' : α
h : Stream'.corec' (Corec.f f) (Sum.inr b) n = some a'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd n = some a'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail

Tactic:
rw [interleave_eq s₁ s₂]; rfl

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
⊢ (of G f (Classical.arbitrary ι)) (-1) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (-1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1)) = s₁.get (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.corec' (Corec.f f) o (n + 1) = some a' →
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'

Tactic:
Stream'.corec'_eq (Corec.f f) o

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a' →
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
⊢ Computation α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ s₁ = s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1) + 1) = s₂.get (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₁
n : ℕ
h : (fun b ↦ a = b) (s₁.get n)
⊢ (fun b ↦ a = b) ((s₁ ⋈ s₂).get (2 * n))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s₁ s₂ : Stream' α
x✝ : a ∈ s₂
n : ℕ
h : (fun b ↦ a = b) (s₂.get n)
⊢ (fun b ↦ a = b) ((s₁ ⋈ s₂).get (2 * n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ s.even.tail = s.tail.tail.even

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
⊢ f s = g s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (corec f b).destruct = rmap (corec f) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a₁ a₂ : α
s : Stream' α
⊢ (a₁ :: a₂ :: s).even = a₁ :: s.even

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
⊢ s.TerminatedAt n ↔ (s.get? n).isNone = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ ¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ ¬(cons x s).TerminatedAt 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x : α
s : Seq α
n : ℕ
⊢ (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s.tail.val = s.val.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).Terminates ↔ s.Terminates

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s'.tail.val = s'.val.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.TerminatedAt 0 ↔ s = nil

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : x ∈ s
⊢ ∃ i, some x = s.get? i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
x✝ : a ∈ nil
w✝ : ℕ
h : some a = none
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a b : α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
h✝ : a ∈ cons b ⟨val✝, property✝⟩
h : some a = some b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a b : α
s : Seq α
⊢ a = b ∨ a ∈ s → a ∈ cons b s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.tail = (s₁.tail ⋈ s₂.tail).even

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ s₁'.head = s₁.head ∧ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁'.tail s₁.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ s = cons a s.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
⊢ ↑(cons b s') k.succ = ↑s' k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
⊢ C s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ s'.head = s.head ∧ (fun s' s ↦ s' = s.even ⋈ s.odd) s'.tail s.tail

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : (fun x ↦ l[x]?) n = none
⊢ (fun x ↦ l[x]?) (n + 1) = none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ↑(a :: l) = cons a ↑l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Stream' α
n : ℕ
h : map some s n = none
⊢ map some s (n + 1) = none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n.succ)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
⊢ Stream'.map (Option.map f) s n = none → Stream'.map (Option.map f) s (n + 1) = none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.odd.get n = s.get (2 * n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
⊢ IsSeq (Function.update (↑s) n (Option.map f (↑s n)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.even
n : ℕ
h : (fun b ↦ a = b) (s.even.get n)
⊢ (fun b ↦ a = b) (s.get (2 * n))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Basic

Goal state before:
pp: α : Type u_1
inst✝ : One α
a : α
n : ℕ
aₙ : α
h : (GenContFract.ofInteger a).partNums.get? n = some aₙ
⊢ aₙ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Basic

Goal state before:
pp: α : Type u_1
inst✝² : One α
inst✝¹ : Zero α
inst✝ : LT α
a : α
n : ℕ
bₙ : α
h : (↑(SimpContFract.ofInteger a)).partDens.get? n = some bₙ
⊢ 0 < bₙ

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ENatToNat

Goal state before:
pp: x : ℕ∞
⊢ ¬⊤ < x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.odd
n : ℕ
h : (fun b ↦ a = b) (s.odd.get n)
⊢ (fun b ↦ a = b) (s.get (2 * n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ n < x.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n < x.length
⊢ (x ++ₛ a).get n = x[n]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ (x ++ₛ a).get (x.length + n) = a.get n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
⊢ a = b → x ++ₛ a = x ++ₛ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l : List α
s : Stream' α
⊢ drop (a :: l).length (a :: l ++ₛ s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ s₁ = s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ [s.head] ++ₛ s.tail = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ (take n s).length = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ s.val m = some a → s.val n = some a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m : ℕ
ha : (fun b ↦ some a = b) (s.val.get m)
n : ℕ
hb : (fun b_1 ↦ some b = b_1) (s.val.get n)
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
m n : ℕ
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n✝ : ℕ
x✝ : 0 < n✝ + 1
⊢ (take (n✝ + 1) s)[0]? = some (s.get 0)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : (fun b ↦ some a = b) (s.val.get n)
⊢ (s.val n).isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
k n : ℕ
h : k + 1 < n + 1
⊢ (take (n + 1) s)[k + 1]? = some (s.get (k + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
xs : Stream' α
⊢ (take n xs).dropLast = take (n - 1) xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : (fun b ↦ some a = b) (s.think.val.get n)
⊢ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
x✝ : a ∈ empty α
n : ℕ
h : (fun b ↦ some a = b) ((empty α).val.get n)
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ take n s ++ₛ drop n s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ x ++ take n a = take (x.length + n) (x ++ₛ a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = a.get m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ (take n (x ++ₛ a)).length = (List.take n x).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
H : ¬s.Terminates
⊢ s = empty α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
a : α
⊢ s.get = a → a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
a : α
p : s ~> a
⊢ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ take n (x ++ₛ a) = List.take n x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
T : s.Terminates
a : α
h : a ∈ s
⊢ s.Results a s.length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
⊢ take (m + n) a = take m a ++ take n (drop m a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a = List.take m (take n a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
⊢ m = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a <+: take n a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h : s.Terminates
⊢ s.think.length = s.length + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ List.map f (take n a) = take n (map f a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
this : s.Terminates
⊢ s.think.length = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
⊢ s.Results a n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
n : ℕ
⊢ ((pure a).thinkN n).Results a n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
⊢ take n (drop m a) = List.drop m (take (m + n) a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s = (pure a).thinkN n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
⊢ C s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ s.length' = ↑(s.length h)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : ¬s.Terminates
⊢ s.length' = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
⊢ nil.length' = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
h : s.Terminates
⊢ (cons x s).length ⋯ = s.length h + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
m : ℕ
hm : x.length = n + m
p : ℕ
hk : m ≤ m + p
⊢ m = (List.drop n x).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ (cons x s).length' = s.length' + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ s.length h = 0 ↔ s = nil

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.length' = 0 ↔ s = nil

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.length' ≠ 0 ↔ ∃ x s', s = cons x s'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
⊢ some (s₁.get n.succ) = some (s₂.get n.succ)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (∃ (h : s.Terminates), s.length h ≤ n) ↔ s.TerminatedAt n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ s.TerminatedAt n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
⊢ Stream'.map (fun o ↦ Option.casesOn o none (some ∘ f)) s n = some b →
    Stream'.map (fun o ↦ Option.casesOn o none (some ∘ f)) s (n + 1) = some b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l : List α
x✝ : a :: l ≠ []
l' : List α
a' : α
⊢ corec Stream'.cycleF Stream'.cycleG (a', l', a, l) = a' :: l' ++ₛ corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

Tactic:
by

Goal state after: