feat: deriving optics

[EdAyers]

This file defines the derive_optics T command where T is an inductive datatype. For each constructor 𝑐 of T and each field 𝑎 : α of 𝑐, this will create the following definitions:

1. T.𝑐.𝑎? : T → Option α
2. T.𝑐.𝑎! : T → α
3. T.𝑐.with𝑎 : α → T → T
4. T.𝑐.modify𝑎 : (α → α) → T → T
5. T.𝑐.modifyM𝑎 : (α → M α) → T → M T

This eliminates some boilerplate when defining new inductive datatypes.

Additionally, if T has multiple constructors with the same field name 𝑎, it will create shortened versions of these (T.𝑎?, T.𝑎! etc).

[kim-em]

Oops, @EdAyers, I see you removed the awaiting-review tag yourself. What is the status of this PR?

[EdAyers]

Basically, I wasn't sure what the protocol was for mathlib4. I am also not sure whether this belongs in mathlib4.

[urkud]

How does modify behave if other fields depend on this one?

A semi-offtopic idea. There is .copy function used many times in mathlib that updates data fields to propositionally (but probably not definitionally) equal terms. See, e.g., local_equiv.copy. How hard would it be for you to write a command that generates this copy command (plus copy_eq and something like coe_copy/copy_apply/...)? Ideally, it should use simp-normal forms for projections (e.g., coercion instead to toFun) based on simps machinery.