no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
n : ℕ
⊢ List.take 0 (take n s) = take (min n 0) s
rw [min_zero, List.take_zero, take_zero]
no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
m : ℕ
⊢ List.take m (take 0 s) = take (min 0 m) s
rw [zero_min, take_zero, List.take_nil]
no goals
α : Type u
β : Type v
δ : Type w
s : Stream' α
m n : ℕ
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
rw [take_succ, List.take_cons, Nat.min_succ_succ, take_succ, take_take]