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

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n
⊢ is_decent (Stream'.take n a)
Tactic:
cases' n with n
State after:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ is_decent (Stream'.take 0 a)

case succ
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n + 1
⊢ is_decent (Stream'.take (n + 1) a)

State before:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ is_decent (Stream'.take 0 a)
Tactic:
exfalso
State after:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ False

State before:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ False
Tactic:
exact Nat.lt_asymm hn hn
State after:
no goals

State before:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n + 1
⊢ is_decent (Stream'.take (n + 1) a)
Tactic:
have ht := ha n
State after:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n + 1
ht : is_decent (a.inits.get n)
⊢ is_decent (Stream'.take (n + 1) a)

State before:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
n : ℕ
hn : 0 < n + 1
ht : is_decent (a.inits.get n)
⊢ is_decent (Stream'.take (n + 1) a)
Tactic:
rwa [Stream'.get_inits] at ht
State after:
no goals