mathlib

96ee2a69 - feat(order/filter/basic): prove `@cofinite ℕ = at_top` (#1888)

feat(order/filter/basic): prove `@cofinite ℕ = at_top` (#1888) * feat(order/filter/basic): prove `@cofinite ℕ = at_top` Also generalize `not_injective_(nat/int)_fintype`, and use `[infinite α]` instead of `set.infinite (@univ α)` as an argument. * Update src/data/equiv/basic.lean Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * Drop a duplicate definition, thanks @ChrisHughes24 Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>