Yury G. Kudryashov

chore(Data/List/Enum): move from `Basic`

1

--- [](https://gitpod.io/from-referrer/)

Also, these `simp` calls are better compatible with a future refactor using `FunLike` for measures. --- [](https://gitpod.io/from-referrer/)

Go over suggestions in #51

2

In #51, @akirak made some suggestions that were deemed out of the scope of that PR. Go over these suggestions and decide whether to implement them.

feat: backport `Function.Injective` etc from Mathlib

7

Also move `Std.Logic` to `Std.Logic.Basic`.

feat(Order/FunLike): define `PointwiseLE`

9

- introduce a mixin class `DFunLike.PointwiseLE`, use it to define `DFunLike.instPartialOrder`; - add a generic `DFunLike.orderEmbeddingCoe` - add `DFunLike.PointwiseLE` instances here and there. With this refactor and #13022, I'm going...

--- [](https://gitpod.io/from-referrer/)

--- I don't understand why linter fails. [](https://gitpod.io/from-referrer/)

feat(MeasureTheory): generalize `ae` to `OuterMeasureClass`

2

- Move definition and some lemmas from `MeasureSpaceDef` to `OuterMeasure.AE`. - Rename `MeasureTheory.Measure.ae` to `MeasureTheory.ae`. - Generalize the definition and theorems to `[OuterMeasureClass _ _]`. See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.22Almost.20every.22.20on.20outer.20measures and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Order.20on.20measures/near/425729507...

feat: define `AddConstEquiv`

3

--- - [x] depends on: #9725 - [x] depends on: #9724 [](https://gitpod.io/from-referrer/)

Also use it for `Real.sqrt` --- [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60Sqrt.60.20notation.20typeclass/near/400086502) [](https://gitpod.io/from-referrer/)