Matthew Robert Ballard

chore(Algebra.Ring.InjSurj): remove redundant `mul` and `add` fields

1

Lean can figure these out and if inferred instance of `Mul` (or `Add`) contains non-reducible terms, it will block unification. --- - [ ] depends on: #11521 [](https://gitpod.io/from-referrer/)

Trace class `Meta.synthInstance.answer` is not registered

4

### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....

Configuration option for `synthPendingDepth`

3

Currently there is the following in `Lean.Meta.SynthInstance` ```lean /- TODO: use a configuration option instead of the hard-coded limit `1`. -/ if (← read).synthPendingDepth > 1 then trace[Meta.synthPending] "too many...

chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s

2

These are wrappers around the constructor and projection for `Opposite Quiver.Hom _ _`. The projection itself is reducible and with structure eta built in to defeq it seems like we...

change

2

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

test

2

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

chore (Algebra.PUnitInstances): split file into `Algebra`, `Order`, and `Module` instance files

1

When we need algebra structures on `PUnit`, we should be more surgical about what we are importing. --- [](https://gitpod.io/from-referrer/)

chore (Algebra.Order.Nonneg.Ring): split into unbundled and bundled ordered algebra files

4

We split `Algebra.Order.Nonneg.Ring` into `Algebra.Order.Nonneg.Ring` which uses unbundled ordered algebra typeclasses, eg `CovariantClass`, and `Algebra.Order.Nonneg.OrderedRing` which uses bundled class, eg `OrderedAddComm`. Using this we can avoid importing bundled ordered algebra...

chore (Algebra.Order.Field.Defs): split off results about unbundled ordered algebra

4

We should be able to use these results about unbundled ordered algebra without importing the heavy machinery of the bundled typeclasses. --- - [ ] depends on: #14393 [![Open in...

chore (Data.Fintype.Basic): de-simp `Fintype.univ_ofSubsingleton`

3

In principle, `Fintype.univ_ofSubsingleton` could be a `simp` theorem but it applies to any occurence of `univ` and requires unification of the (possibly very complex) `Fintype` instances. It appears to not...