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

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
⊢ ∀ (n : ℕ),
    ((choose_decent_words is_decent a hinit hnot).get n).start =
      ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length
Tactic:
intro n
State after:
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
n : ℕ
⊢ ((choose_decent_words is_decent a hinit hnot).get n).start =
    ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
n : ℕ
⊢ ((choose_decent_words is_decent a hinit hnot).get n).start =
    ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length
Tactic:
induction' n with n pn
State after:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
⊢ ((choose_decent_words is_decent a hinit hnot).get 0).start =
    ∑ j ∈ Finset.range 0, ((choose_decent_words is_decent a hinit hnot).get j).length

case succ
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
n : ℕ
pn :
  ((choose_decent_words is_decent a hinit hnot).get n).start =
    ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length
⊢ ((choose_decent_words is_decent a hinit hnot).get (n + 1)).start =
    ∑ j ∈ Finset.range (n + 1), ((choose_decent_words is_decent a hinit hnot).get j).length

State before:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
⊢ ((choose_decent_words is_decent a hinit hnot).get 0).start =
    ∑ j ∈ Finset.range 0, ((choose_decent_words is_decent a hinit hnot).get j).length
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
n : ℕ
pn :
  ((choose_decent_words is_decent a hinit hnot).get n).start =
    ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length
⊢ ((choose_decent_words is_decent a hinit hnot).get (n + 1)).start =
    ∑ j ∈ Finset.range (n + 1), ((choose_decent_words is_decent a hinit hnot).get j).length
Tactic:
rw [Finset.sum_range_succ, ← pn]
State after:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
n : ℕ
pn :
  ((choose_decent_words is_decent a hinit hnot).get n).start =
    ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length
⊢ ((choose_decent_words is_decent a hinit hnot).get (n + 1)).start =
    ((choose_decent_words is_decent a hinit hnot).get n).start +
      ((choose_decent_words is_decent a hinit hnot).get n).length

State before:
case succ
α : Type
is_decent : List α → Prop
a : Stream' α
hinit : all_prefixes is_decent a
hnot : ∀ (n : ℕ), ∃ k, 0 < k ∧ all_prefixes is_decent (Stream'.drop (n + k) a)
n : ℕ
pn :
  ((choose_decent_words is_decent a hinit hnot).get n).start =
    ∑ j ∈ Finset.range n, ((choose_decent_words is_decent a hinit hnot).get j).length
⊢ ((choose_decent_words is_decent a hinit hnot).get (n + 1)).start =
    ((choose_decent_words is_decent a hinit hnot).get n).start +
      ((choose_decent_words is_decent a hinit hnot).get n).length
Tactic:
rfl
State after:
no goals