Commit 2026-03-28 11:48 15f86323

chore: avoid dsimp; infer_instance (#37288) This PR cleans up a bunch of instances using inferInstanceAs and deriving. It seems that when in a noncomputable section, derived instances will always be noncomputable, while manual instances can still end up being computable. So this PR also adds some now transitively required noncomputable annotations.