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

State before:
α : Type
lengths : Stream' ℕ
a : Stream' α
⊢ break_into_words lengths a = fun i => Stream'.take (lengths i) (Stream'.drop (∑ j ∈ Finset.range i, lengths j) a)
Tactic:
funext n
State after:
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ break_into_words lengths a n = Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)

State before:
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ break_into_words lengths a n = Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)
Tactic:
convert_to ((Stream'.corec (λ x ↦ Stream'.take (x.fst.head) x.snd)
               (λ x ↦ ⟨x.fst.tail, Stream'.drop (x.fst.head) x.snd⟩)) :
                Stream' ℕ × Stream' α → Stream' (List α)) ⟨lengths, a⟩ n =
           Stream'.take (lengths n) (Stream'.drop (∑ j in Finset.range n, lengths j) a)
State after:
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ Stream'.corec (fun x => Stream'.take x.1.head x.2) (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a) n =
    Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)

State before:
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ Stream'.corec (fun x => Stream'.take x.1.head x.2) (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a) n =
    Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)
Tactic:
rw [Stream'.corec_def,Stream'.map]
State after:
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ Stream'.take ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).1.head
      ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
    Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)

State before:
case h
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ Stream'.take ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).1.head
      ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
    Stream'.take (lengths n) (Stream'.drop (∑ j ∈ Finset.range n, lengths j) a)
Tactic:
congr
State after:
case h.e_a
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).1.head = lengths n

case h.e_a
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
    Stream'.drop (∑ j ∈ Finset.range n, lengths j) a

State before:
case h.e_a
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).1.head = lengths n
Tactic:
revert a lengths
State after:
case h.e_a
α : Type
n : ℕ
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).1.head = lengths n

State before:
case h.e_a
α : Type
n : ℕ
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).1.head = lengths n
Tactic:
induction' n with pn hpn
State after:
case h.e_a.zero
α : Type
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get 0).1.head = lengths 0

case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).1.head = lengths pn
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get (pn + 1)).1.head =
      lengths (pn + 1)

State before:
case h.e_a.zero
α : Type
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get 0).1.head = lengths 0
Tactic:
intro a b
State after:
case h.e_a.zero
α : Type
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get 0).1.head = a 0

State before:
case h.e_a.zero
α : Type
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get 0).1.head = a 0
Tactic:
rfl
State after:
no goals

State before:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).1.head = lengths pn
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get (pn + 1)).1.head =
      lengths (pn + 1)
Tactic:
intro a b
State after:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).1.head = lengths pn
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get (pn + 1)).1.head = a (pn + 1)

State before:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).1.head = lengths pn
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get (pn + 1)).1.head = a (pn + 1)
Tactic:
rw [Stream'.get_succ, Stream'.iterate_eq, Stream'.tail_cons, hpn]
State after:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).1.head = lengths pn
a : Stream' ℕ
b : Stream' α
⊢ (a, b).1.tail pn = a (pn + 1)

State before:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).1.head = lengths pn
a : Stream' ℕ
b : Stream' α
⊢ (a, b).1.tail pn = a (pn + 1)
Tactic:
rfl
State after:
no goals

State before:
case h.e_a
α : Type
lengths : Stream' ℕ
a : Stream' α
n : ℕ
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
    Stream'.drop (∑ j ∈ Finset.range n, lengths j) a
Tactic:
revert a lengths
State after:
case h.e_a
α : Type
n : ℕ
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
      Stream'.drop (∑ j ∈ Finset.range n, lengths j) a

State before:
case h.e_a
α : Type
n : ℕ
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get n).2 =
      Stream'.drop (∑ j ∈ Finset.range n, lengths j) a
Tactic:
induction' n with pn hpn
State after:
case h.e_a.zero
α : Type
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get 0).2 =
      Stream'.drop (∑ j ∈ Finset.range 0, lengths j) a

case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get (pn + 1)).2 =
      Stream'.drop (∑ j ∈ Finset.range (pn + 1), lengths j) a

State before:
case h.e_a.zero
α : Type
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get 0).2 =
      Stream'.drop (∑ j ∈ Finset.range 0, lengths j) a
Tactic:
intro a b
State after:
case h.e_a.zero
α : Type
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get 0).2 =
    Stream'.drop (∑ j ∈ Finset.range 0, a j) b

State before:
case h.e_a.zero
α : Type
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get 0).2 =
    Stream'.drop (∑ j ∈ Finset.range 0, a j) b
Tactic:
rfl
State after:
no goals

State before:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
⊢ ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get (pn + 1)).2 =
      Stream'.drop (∑ j ∈ Finset.range (pn + 1), lengths j) a
Tactic:
intro a b
State after:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get (pn + 1)).2 =
    Stream'.drop (∑ j ∈ Finset.range (pn + 1), a j) b

State before:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
a : Stream' ℕ
b : Stream' α
⊢ ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (a, b)).get (pn + 1)).2 =
    Stream'.drop (∑ j ∈ Finset.range (pn + 1), a j) b
Tactic:
rw [Stream'.get_succ, Stream'.iterate_eq, Stream'.tail_cons, hpn,
    Stream'.drop_drop, Finset.sum_range_succ']
State after:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
a : Stream' ℕ
b : Stream' α
⊢ Stream'.drop (∑ j ∈ Finset.range pn, (a, b).1.tail j + (a, b).1.head) (a, b).2 =
    Stream'.drop (∑ k ∈ Finset.range pn, a (k + 1) + a 0) b

State before:
case h.e_a.succ
α : Type
pn : ℕ
hpn :
  ∀ (lengths : Stream' ℕ) (a : Stream' α),
    ((Stream'.iterate (fun x => (x.1.tail, Stream'.drop x.1.head x.2)) (lengths, a)).get pn).2 =
      Stream'.drop (∑ j ∈ Finset.range pn, lengths j) a
a : Stream' ℕ
b : Stream' α
⊢ Stream'.drop (∑ j ∈ Finset.range pn, (a, b).1.tail j + (a, b).1.head) (a, b).2 =
    Stream'.drop (∑ k ∈ Finset.range pn, a (k + 1) + a 0) b
Tactic:
congr
State after:
no goals