Commit 2025-06-16 13:31 6d589992

View on Github →

chore: whitespace fixes (#25956) Found by #24465.

Estimated changes

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Analysis/Analytic/Order.lean

modified theorem AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top

Modified Mathlib/Analysis/RCLike/TangentCone.lean

modified theorem tangentConeAt_real_subset_isRCLikeNormedField

Modified Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean

modified def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj

Modified Mathlib/Combinatorics/Quiver/Path.lean

Modified Mathlib/Deprecated/RingHom.lean

Modified Mathlib/Order/RelClasses.lean

modified theorem GCongr.ssuperset_imp_ssuperset_left

modified theorem GCongr.ssuperset_imp_ssuperset_right

Modified Mathlib/Tactic/GRewrite/Core.lean