Theorem: KolmogorovStreams.not_all_prefixes (Compfiles/KolmogorovStreams.lean)

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ¬all_prefixes is_decent a
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)
Tactic:
simp[all_prefixes, Stream'.all_def] at h
State after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∃ x, ¬is_decent (Stream'.take (x + 1) a)
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∃ x, ¬is_decent (Stream'.take (x + 1) a)
⊢ ∃ n, ¬is_decent (Stream'.take n.succ a)
Tactic:
exact h
State after:
no goals