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

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x)
    (break_into_words (fun i => ((choose_indecent_words is_decent a h).get i).length) a)
Tactic:
rw [break_into_words_closed_form]
State after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop (∑ j ∈ Finset.range i, ((choose_indecent_words is_decent a h).get j).length) a)

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop (∑ j ∈ Finset.range i, ((choose_indecent_words is_decent a h).get j).length) a)
Tactic:
simp_rw [←chosen_indecent_closed_form]
State after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a)

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
⊢ Stream'.All (fun x => ¬is_decent x) fun i =>
    Stream'.take ((choose_indecent_words is_decent a h).get i).length
      (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a)
Tactic:
intro j
State after:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
j : ℕ
⊢ ¬is_decent
      (Stream'.get
        (fun i =>
          Stream'.take ((choose_indecent_words is_decent a h).get i).length
            (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a))
        j)

State before:
α : Type
is_decent : List α → Prop
a : Stream' α
h : ∀ (k : ℕ), ¬all_prefixes is_decent (Stream'.drop k a)
j : ℕ
⊢ ¬is_decent
      (Stream'.get
        (fun i =>
          Stream'.take ((choose_indecent_words is_decent a h).get i).length
            (Stream'.drop ((choose_indecent_words is_decent a h).get i).start a))
        j)
Tactic:
exact ((choose_indecent_words is_decent a h).get j).h
State after:
no goals