English
A further form of length_take_of_le_length asserting equal length for bounded take.
Русский
Ещё одна форма утверждения о длине take, устанавливающая равную длину при ограничении.
LaTeX
$$$\mathrm{length}(\mathrm{take}(n, s)) = n$$$
Lean4
theorem length_take_of_le_length {s : Seq α} {n : ℕ} (hle : ∀ h : s.Terminates, n ≤ s.length h) :
(s.take n).length = n := by
induction n generalizing s with
| zero => simp [take]
| succ n ih =>
rw [take, destruct]
let ⟨a, ha⟩ := lt_length_iff'.1 (fun ht => lt_of_lt_of_le (Nat.succ_pos _) (hle ht))
simp [Option.mem_def.1 ha]
rw [ih]
intro h
simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]
intro m hmn hs
have := lt_length_iff'.1 (fun ht => (Nat.lt_of_succ_le (hle ht)))
rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this
simp at this
