Commit 2026-03-25 18:55 4f7dd0bc

View on Github →

chore: remove unnecessary backward.inferInstanceAs.wrap (#37154) Try to remove backward.inferInstanceAs.wrap options, because these lead to leaky types.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Limits.lean

Modified Mathlib/AlgebraicGeometry/Cover/Directed.lean

Modified Mathlib/AlgebraicGeometry/Cover/Over.lean

Modified Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean

Modified Mathlib/CategoryTheory/Triangulated/TStructure/ETrunc.lean

Modified Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean