theorem Std.Iterators.Iter.step_repeat {α : Type w} {f : α → α} {init : α} : («repeat» f init).step = PlausibleIterStep.yield («repeat» f (f init)) init ⋯

theorem Std.Iterators.Iter.atIdxSlow?_zero_repeat {α : Type w} {f : α → α} {init : α} : atIdxSlow? 0 («repeat» f init) = some init

theorem Std.Iterators.Iter.atIdxSlow?_succ_repeat {α : Type w} {f : α → α} {init : α} {k : Nat} : atIdxSlow? (k + 1) («repeat» f init) = atIdxSlow? k («repeat» f (f init))

theorem Std.Iterators.Iter.atIdxSlow?_succ_repeat_eq_map {α : Type w} {f : α → α} {init : α} {k : Nat} : atIdxSlow? (k + 1) («repeat» f init) = f <$> atIdxSlow? k («repeat» f init)

@[simp]

theorem Std.Iterators.Iter.atIdxSlow?_repeat {α : Type w} {f : α → α} {init : α} {n : Nat} : atIdxSlow? n («repeat» f init) = some (Nat.repeat f n init)

theorem Std.Iterators.Iter.isSome_atIdxSlow?_repeat {α : Type w} {f : α → α} {init : α} {k : Nat} : (atIdxSlow? k («repeat» f init)).isSome = true

@[simp]

theorem Std.Iterators.Iter.toList_take_repeat_succ {α : Type w} {f : α → α} {init : α} {k : Nat} : (take (k + 1) («repeat» f init)).toList = init :: (take k («repeat» f (f init))).toList