internlm/Lean-Github huggingface dataset:
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ 0 < a ^ a * b ^ b * c ^ c
Tactic:
positivity
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ c * b ^ a * c ^ b ≤ a ^ a * b ^ b * c ^ c
Tactic:
rw [←(Real.log_le_log_iff (by positivity) (by positivity))]
Proof state after:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ c * b ^ a * c ^ b).log ≤ (a ^ a * b ^ b * c ^ c).log
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ c * b ^ a * c ^ b).log ≤ (a ^ a * b ^ b * c ^ c).log
Tactic:
simp (discharger := positivity) only [Real.log_mul, Real.log_rpow]
Proof state after:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ c * a.log + a * b.log + b * c.log ≤ a * a.log + b * b.log + c * c.log
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ c * a.log + a * b.log + b * c.log ≤ a * a.log + b * b.log + c * c.log
Tactic:
nlinarith only [hab', hbc', hab, hbc]
Proof state after:
no goals
Theorem: Usa1974P2.usa1974_p2_wlog
Proof state before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ 0 < a ^ c * b ^ a * c ^ b
Tactic:
positivity
Proof state after:
no goals
Theorem: Usa1998P1.zmod_eq
Proof state before:
a b c : ℤ
⊢ a ≡ b [ZMOD c] ↔ a % c = b % c
Tactic:
rfl
Proof state after:
no goals
Theorem: Usa1998P1.mod2_abs
Proof state before:
a : ℤ
⊢ |a| % 2 = a % 2
Tactic:
cases' abs_cases a with h h <;> rw [h.1]
Proof state after:
case inr
a : ℤ
h : |a| = -a ∧ a < 0
⊢ -a % 2 = a % 2
Theorem: Usa1998P1.mod2_abs
Proof state before:
case inr
a : ℤ
h : |a| = -a ∧ a < 0
⊢ -a % 2 = a % 2
Tactic:
rw [Int.neg_emod_two]
Proof state after:
no goals
Theorem: Usa1998P1.mod2_diff
Proof state before:
a b : ℤ
⊢ |a - b| % 2 = (a + b) % 2
Tactic:
rw [mod2_abs, Int.sub_eq_add_neg, Int.add_emod, Int.neg_emod_two, ←Int.add_emod]
Proof state after:
no goals
Theorem: KolmogorovStreams.break_into_words_cons
Proof state before:
α : Type
lengths : Stream' ℕ
first_length : ℕ
a : Stream' α
⊢ (break_into_words (first_length :: lengths) a).tail = break_into_words lengths (Stream'.drop first_length a)
Tactic:
simp [break_into_words, Stream'.corec, Stream'.tail_map, Stream'.tail_iterate]
Proof state after:
no goals
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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)
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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)
Proof 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)
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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]
Proof 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)
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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)
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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)
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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]
Proof 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)
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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']
Proof 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
Theorem: KolmogorovStreams.break_into_words_closed_form
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.take_prefix
Proof 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
Proof 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)
Theorem: KolmogorovStreams.take_prefix
Proof 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
Proof state after:
case zero
α : Type
is_decent : List α → Prop
a : Stream' α
ha : all_prefixes is_decent a
hn : 0 < 0
⊢ False
Theorem: KolmogorovStreams.take_prefix
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.take_prefix
Proof 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
Proof 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)
Theorem: KolmogorovStreams.take_prefix
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.chosen_decent_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.chosen_decent_closed_form
Proof 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
Proof 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
Theorem: KolmogorovStreams.chosen_decent_closed_form
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.chosen_decent_closed_form
Proof 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]
Proof 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
Theorem: KolmogorovStreams.chosen_decent_closed_form
Proof 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
Proof state after:
no goals
Theorem: KolmogorovStreams.check_decent_words
Proof 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)
⊢ Stream'.All is_decent (break_into_words (fun i => ((choose_decent_words is_decent a hinit hnot).get i).length) a)
Tactic:
rw [break_into_words_closed_form]
Proof 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)
⊢ Stream'.All is_decent fun i =>
    Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
      (Stream'.drop (∑ j ∈ Finset.range i, ((choose_decent_words is_decent a hinit hnot).get j).length) a)
Theorem: KolmogorovStreams.check_decent_words
Proof 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)
⊢ Stream'.All is_decent fun i =>
    Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
      (Stream'.drop (∑ j ∈ Finset.range i, ((choose_decent_words is_decent a hinit hnot).get j).length) a)
Tactic:
simp_rw [←chosen_decent_closed_form]
Proof 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)
⊢ Stream'.All is_decent fun i =>
    Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
      (Stream'.drop ((choose_decent_words is_decent a hinit hnot).get i).start a)
Theorem: KolmogorovStreams.check_decent_words
Proof 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)
⊢ Stream'.All is_decent fun i =>
    Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
      (Stream'.drop ((choose_decent_words is_decent a hinit hnot).get i).start a)
Tactic:
intro j
Proof 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)
j : ℕ
⊢ is_decent
    (Stream'.get
      (fun i =>
        Stream'.take ((choose_decent_words is_decent a hinit hnot).get i).length
          (Stream'.drop ((choose_decent_words is_decent a hinit hnot).get i).start a))
      j)