Commit 2024-05-07 22:42 294ff6a4

View on Github →

perf(BundledCats): more explicit universe annotations (#12741) Testing for leanprover/lean4#4085 exposed possible regressions typeclass synthesis which can be ameliorated using explicit universes. We do this and we add references to the issue leanprover-community/mathlib4#12737 tracking these changes.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/FunctionField.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

modified theorem RingHom.RespectsIso.basicOpen_iff_localization

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

modified theorem AlgebraicGeometry.IsOpenImmersion.app_eq_invApp_app_of_comp_eq

modified theorem AlgebraicGeometry.IsOpenImmersion.app_eq_inv_app_app_of_comp_eq_aux

modified theorem AlgebraicGeometry.IsOpenImmersion.iff_stalk_iso

modified theorem AlgebraicGeometry.IsOpenImmersion.isOpen_range

modified theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac

modified theorem AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac

modified theorem AlgebraicGeometry.IsOpenImmersion.lift_app

modified theorem AlgebraicGeometry.IsOpenImmersion.of_stalk_iso

modified theorem AlgebraicGeometry.IsOpenImmersion.to_iso

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_eq_of_locallyRingedSpace_eq

modified theorem AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.scheme_toScheme

modified def AlgebraicGeometry.Scheme.Hom.invApp

modified def AlgebraicGeometry.Scheme.Hom.opensRange

modified def AlgebraicGeometry.Scheme.OpenCover.add

modified theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace

modified def AlgebraicGeometry.Scheme.OpenCover.copy

modified def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover

modified theorem AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange

modified theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range

modified def AlgebraicGeometry.Scheme.OpenCover.pullbackCover'

modified def AlgebraicGeometry.Scheme.OpenCover.pullbackCover

modified def AlgebraicGeometry.Scheme.affineBasisCover

modified def AlgebraicGeometry.Scheme.affineBasisCoverOfAffine

modified def AlgebraicGeometry.Scheme.affineBasisCoverRing

modified theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis

modified theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range

modified theorem AlgebraicGeometry.Scheme.affineBasisCover_obj

modified def AlgebraicGeometry.Scheme.affineCover

modified theorem AlgebraicGeometry.Scheme.image_basicOpen

modified def AlgebraicGeometry.Scheme.ofRestrict

modified def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop

modified def AlgebraicGeometry.Scheme.restrict

modified theorem AlgebraicGeometry.isIso_iff_isOpenImmersion

modified theorem AlgebraicGeometry.isIso_iff_stalk_iso

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

modified theorem AlgebraicGeometry.Scheme.eq_restrict_presheaf_map_eqToHom

modified theorem AlgebraicGeometry.Scheme.map_basicOpen'

modified theorem AlgebraicGeometry.Scheme.map_basicOpen

modified theorem AlgebraicGeometry.Scheme.map_basicOpen_map

modified theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app_self

modified def AlgebraicGeometry.Scheme.restrictIsoOfEq

modified def AlgebraicGeometry.Scheme.restrictRestrict

modified def AlgebraicGeometry.Scheme.restrictRestrictComm

modified theorem AlgebraicGeometry.Scheme.restrictRestrict_hom_restrict

modified theorem AlgebraicGeometry.Scheme.restrictRestrict_inv_restrict_restrict

modified theorem AlgebraicGeometry.image_morphismRestrict_preimage

modified theorem AlgebraicGeometry.isPullback_morphismRestrict

modified def AlgebraicGeometry.morphismRestrict

modified def AlgebraicGeometry.morphismRestrictEq

modified def AlgebraicGeometry.morphismRestrictOpensRange

modified def AlgebraicGeometry.morphismRestrictRestrict

modified def AlgebraicGeometry.morphismRestrictRestrictBasicOpen

modified def AlgebraicGeometry.morphismRestrictStalkMap

modified theorem AlgebraicGeometry.morphismRestrict_base_coe

modified theorem AlgebraicGeometry.morphismRestrict_c_app

modified theorem AlgebraicGeometry.morphismRestrict_comp

modified theorem AlgebraicGeometry.morphismRestrict_val_base

modified theorem AlgebraicGeometry.morphismRestrict_ι

modified def AlgebraicGeometry.pullbackRestrictIsoRestrict

modified theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_morphismRestrict

modified theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_restrict

modified theorem AlgebraicGeometry.pullbackRestrictIsoRestrict_inv_fst

modified theorem AlgebraicGeometry.Γ_map_morphismRestrict

Modified Mathlib/AlgebraicGeometry/Scheme.lean

deleted def AlgebraicGeometry.Scheme.empty.{u}

added def AlgebraicGeometry.Scheme.empty

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

modified theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext'

modified structure AlgebraicGeometry.LocallyRingedSpace.Hom

modified theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero

modified def AlgebraicGeometry.LocallyRingedSpace.comp

modified theorem AlgebraicGeometry.LocallyRingedSpace.comp_val

modified theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c

modified theorem AlgebraicGeometry.LocallyRingedSpace.comp_val_c_app

modified def AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace

modified def AlgebraicGeometry.LocallyRingedSpace.forgetToTop

modified def AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso

modified def AlgebraicGeometry.LocallyRingedSpace.id

modified def AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso

modified def AlgebraicGeometry.LocallyRingedSpace.ofRestrict

modified theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen

modified def AlgebraicGeometry.LocallyRingedSpace.restrict

modified def AlgebraicGeometry.LocallyRingedSpace.restrictTopIso

modified def AlgebraicGeometry.LocallyRingedSpace.Γ

modified theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map

modified theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map_op

modified theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj

modified theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op

modified structure AlgebraicGeometry.LocallyRingedSpace