mathlib3

a372dfce - chore(*): don't assume `sub_eq_add_neg` and `div_eq_mul_inv` are defeq (#5302)

chore(*): don't assume `sub_eq_add_neg` and `div_eq_mul_inv` are defeq (#5302) This PR prepares for a follow-up PR (#5303) that adds `div` and `sub` fields to (`add_`)`group`(`_with_zero`). That follow-up PR is intended to fix the following kind of diamonds: Let `foo X` be a type with a `∀ X, has_div (foo X)` instance but no `∀ X, has_inv (foo X)`, e.g. when `foo X` is a `euclidean_domain`. Suppose we also have an instance `∀ X [cromulent X], group_with_zero (foo X)`. Then the `(/)` coming from `group_with_zero_has_div` cannot be defeq to the `(/)` coming from `foo.has_div`. As a consequence of making the `has_div` instances defeq, we can no longer assume that `(div_eq_mul_inv a b : a / b = a * b⁻¹) = rfl` for all groups. This preparation PR should have changed all places in mathlib that assumed defeqness, to rewrite explicitly instead. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60div.60.20as.20a.20field.20in.20.60group(_with_zero).60 Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>