mathlib3

3bbb847e - chore(*): remove instance arguments that are inferrable from earlier (#13386)

chore(*): remove instance arguments that are inferrable from earlier (#13386) Some lemmas have typeclass arguments that are in fact inferrable from the earlier ones, at least when everything is Prop valued this is unecessary so we clean up a few cases as they likely stem from typos or library changes. - `src/field_theory/finiteness.lean` it wasn't known at the time (#7644) that a division ring was noetherian, but now it is (#7661) - `src/category_theory/simple.lean` any abelian category has all cokernels so no need to assume it seperately - `src/analysis/convex/extreme.lean` assumed `linear_ordered_field` and `no_smul_zero_divisors` which is unnecessary, we take this as a sign that this and a couple of other convexity results should be generalized to densely ordered linear ordered rings (of which there are examples that are not fields) cc @YaelDillies