mathlib

466b8922 - feat(analysis/asymptotics/asymptotics): generalize, golf (#15010)

feat(analysis/asymptotics/asymptotics): generalize, golf (#15010) * add `is_o_iff_nat_mul_le`, `is_o_iff_nat_mul_le'`, `is_o_irrefl`, `is_O.not_is_o`, `is_o.not_is_O`; * generalize lemmas about `1 = o(f)`, `1 = O(f)`, `f = o(1)`, `f = O(1)` to `[has_one F] [norm_one_class F]`, add some `@[simp]` attrs; * rename `is_O_one_of_tendsto` to `filter.tendsto.is_O_one`; * golf some proofs