Commit 2026-08-11 12:14 52ee81cb

View on Github →

chore: delete deprecated declarations/modules from January 2026 (#42075) Mathlib.Util.MemoFix is directly removed since all deprecations in it are more than 6 months old.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/Algebra/Epi.lean

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/Category/ModuleCat/Semi.lean

Modified Mathlib/Algebra/Category/Ring/Epi.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Int/Defs.lean

deleted theorem zsmul_int_int

deleted theorem zsmul_int_one

Modified Mathlib/Algebra/GroupWithZero/Action/Defs.lean

deleted def DistribMulAction.toAddMonoidHom

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

deleted structure CancelCommMonoidWithZero

deleted structure CancelMonoidWithZero

Deleted Mathlib/Algebra/GroupWithZero/Int.lean

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

deleted theorem mul_mem_nonZeroDivisorsLeft_of_mem_nonZeroDivisorsLeft

deleted theorem mul_mem_nonZeroDivisorsRight_of_mem_nonZeroDivisorsRight

Modified Mathlib/Algebra/GroupWithZero/Regular.lean

Deleted Mathlib/Algebra/ModEq.lean

Modified Mathlib/Algebra/Module/Hom.lean

Modified Mathlib/Algebra/Module/LinearMap/End.lean

Deleted Mathlib/Algebra/NoZeroSMulDivisors/Prod.lean

Modified Mathlib/Algebra/Order/Archimedean/Real/Basic.lean

deleted theorem Real.exists_floor

Deleted Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.Splits.splits

deleted theorem Polynomial.splits_iff_splits

Modified Mathlib/Algebra/Ring/Regular.lean

Modified Mathlib/AlgebraicGeometry/Artinian.lean

Modified Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyOpen.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

Modified Mathlib/AlgebraicTopology/ModelCategory/CofibrantObjectHomotopy.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

Modified Mathlib/Analysis/Calculus/Deriv/Mul.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Add.lean

Modified Mathlib/Analysis/Calculus/Implicit.lean

Modified Mathlib/Analysis/Calculus/ImplicitContDiff.lean

deleted structure IsContDiffImplicitAt

Modified Mathlib/Analysis/Calculus/TangentCone/Basic.lean

Modified Mathlib/Analysis/Complex/IntegerCompl.lean

Modified Mathlib/Analysis/Complex/Schwarz.lean

Modified Mathlib/Analysis/Complex/TaylorSeries.lean

Modified Mathlib/Analysis/Complex/UnitDisc/Basic.lean

deleted theorem Complex.UnitDisc.conj_conj

deleted theorem Complex.UnitDisc.conj_mul

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

deleted theorem UpperHalfPlane.coe_mk_subtype

Modified Mathlib/Analysis/Convex/Body.lean

Deleted Mathlib/Analysis/Distribution/FourierSchwartz.lean

Deleted Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean

Modified Mathlib/Analysis/Distribution/TemperedDistribution.lean

Modified Mathlib/Analysis/Fourier/Notation.lean

deleted structure FourierInvModule

deleted structure FourierModule

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

deleted theorem Matrix.ofLp_toEuclideanLin_apply

deleted theorem Matrix.piLp_ofLp_toEuclideanLin

deleted theorem Matrix.toEuclideanLin_apply

deleted theorem Matrix.toEuclideanLin_apply_piLp_toLp

deleted theorem Matrix.toEuclideanLin_eq_toLin

deleted theorem Matrix.toEuclideanLin_toLp

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/Analysis/Matrix/Spectrum.lean

deleted theorem Matrix.spectrum_toEuclideanLin

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/Analysis/Normed/Group/Pointwise.lean

Modified Mathlib/Analysis/Normed/Module/Ball/Pointwise.lean

Deleted Mathlib/Analysis/Normed/Order/Basic.lean

Modified Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean

Modified Mathlib/Analysis/Polynomial/MahlerMeasure.lean

Modified Mathlib/Analysis/Real/Hyperreal.lean

deleted theorem Hyperreal.Infinite.mul

deleted theorem Hyperreal.Infinite.ne_real

deleted theorem Hyperreal.Infinite.ne_zero

deleted theorem Hyperreal.Infinite.not_infinitesimal

deleted theorem Hyperreal.Infinite.st_eq

deleted def Hyperreal.Infinite

deleted theorem Hyperreal.InfiniteNeg.lt_zero

deleted theorem Hyperreal.InfiniteNeg.neg

deleted theorem Hyperreal.InfiniteNeg.not_infinitePos

deleted theorem Hyperreal.InfiniteNeg.not_infinitesimal

deleted def Hyperreal.InfiniteNeg

deleted theorem Hyperreal.InfinitePos.neg

deleted theorem Hyperreal.InfinitePos.not_infiniteNeg

deleted theorem Hyperreal.InfinitePos.not_infinitesimal

deleted theorem Hyperreal.InfinitePos.pos

deleted def Hyperreal.InfinitePos

deleted theorem Hyperreal.Infinitesimal.eq_zero

deleted def Hyperreal.Infinitesimal

deleted theorem Hyperreal.IsSt.add

deleted theorem Hyperreal.IsSt.infinitesimal_sub

deleted theorem Hyperreal.IsSt.inv

deleted theorem Hyperreal.IsSt.isSt_st

deleted theorem Hyperreal.IsSt.le

deleted theorem Hyperreal.IsSt.map

deleted theorem Hyperreal.IsSt.map₂

deleted theorem Hyperreal.IsSt.mul

deleted theorem Hyperreal.IsSt.neg

deleted theorem Hyperreal.IsSt.not_infinite

deleted theorem Hyperreal.IsSt.st_eq

deleted theorem Hyperreal.IsSt.sub

deleted theorem Hyperreal.IsSt.unique

deleted def Hyperreal.IsSt

deleted theorem Hyperreal.abs_lt_real_iff_infinitesimal

deleted theorem Hyperreal.eq_of_isSt_real

deleted theorem Hyperreal.exists_st_iff_not_infinite

deleted theorem Hyperreal.exists_st_of_not_infinite

deleted theorem Hyperreal.gt_of_neg_of_infinitesimal

deleted theorem Hyperreal.gt_of_tendsto_zero_of_neg

deleted theorem Hyperreal.infiniteNeg_add_infiniteNeg

deleted theorem Hyperreal.infiniteNeg_add_not_infinite

deleted theorem Hyperreal.infiniteNeg_add_not_infinitePos

deleted theorem Hyperreal.infiniteNeg_def

deleted theorem Hyperreal.infiniteNeg_iff

deleted theorem Hyperreal.infiniteNeg_iff_infinite_and_neg

deleted theorem Hyperreal.infiniteNeg_iff_infinite_of_neg

deleted theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg

deleted theorem Hyperreal.infiniteNeg_mul_infiniteNeg

deleted theorem Hyperreal.infiniteNeg_mul_infinitePos

deleted theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos

deleted theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg

deleted theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos

deleted theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg

deleted theorem Hyperreal.infiniteNeg_neg

deleted theorem Hyperreal.infiniteNeg_of_tendsto_bot

deleted theorem Hyperreal.infinitePos_abs_iff_infinite

deleted theorem Hyperreal.infinitePos_abs_iff_infinite_abs

deleted theorem Hyperreal.infinitePos_add_infinitePos

deleted theorem Hyperreal.infinitePos_add_not_infinite

deleted theorem Hyperreal.infinitePos_add_not_infiniteNeg

deleted theorem Hyperreal.infinitePos_def

deleted theorem Hyperreal.infinitePos_iff

deleted theorem Hyperreal.infinitePos_iff_infinite_and_pos

deleted theorem Hyperreal.infinitePos_iff_infinite_of_nonneg

deleted theorem Hyperreal.infinitePos_iff_infinite_of_pos

deleted theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos

deleted theorem Hyperreal.infinitePos_mul_infiniteNeg

deleted theorem Hyperreal.infinitePos_mul_infinitePos

deleted theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg

deleted theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos

deleted theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg

deleted theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos

deleted theorem Hyperreal.infinitePos_neg

deleted theorem Hyperreal.infinitePos_of_tendsto_top

deleted theorem Hyperreal.infinitePos_omega

deleted theorem Hyperreal.infinite_abs_iff

deleted theorem Hyperreal.infinite_iff

deleted theorem Hyperreal.infinite_iff_abs_lt_abs

deleted theorem Hyperreal.infinite_iff_infinitesimal_inv

deleted theorem Hyperreal.infinite_iff_not_exists_st

deleted theorem Hyperreal.infinite_mul_of_infinite_not_infinitesimal

deleted theorem Hyperreal.infinite_mul_of_not_infinitesimal_infinite

deleted theorem Hyperreal.infinite_neg

deleted theorem Hyperreal.infinite_of_infinitesimal_inv

deleted theorem Hyperreal.infinite_omega

deleted theorem Hyperreal.infinitesimal_def

deleted theorem Hyperreal.infinitesimal_epsilon

deleted theorem Hyperreal.infinitesimal_iff

deleted theorem Hyperreal.infinitesimal_iff_infinite_inv

deleted theorem Hyperreal.infinitesimal_inv_of_infinite

deleted theorem Hyperreal.infinitesimal_neg

deleted theorem Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv

deleted theorem Hyperreal.infinitesimal_of_tendsto_zero

deleted theorem Hyperreal.infinitesimal_pos_iff_infinitePos_inv

deleted theorem Hyperreal.infinitesimal_real_iff

deleted theorem Hyperreal.infinitesimal_sub_st

deleted theorem Hyperreal.infinitesimal_zero

deleted theorem Hyperreal.isSt_iff

deleted theorem Hyperreal.isSt_iff_abs_sub_lt_delta

deleted theorem Hyperreal.isSt_iff_tendsto

deleted theorem Hyperreal.isSt_inj_real

deleted theorem Hyperreal.isSt_ofSeq_iff_tendsto

deleted theorem Hyperreal.isSt_of_tendsto

deleted theorem Hyperreal.isSt_real_iff_eq

deleted theorem Hyperreal.isSt_refl_real

deleted theorem Hyperreal.isSt_sSup

deleted theorem Hyperreal.isSt_st'

deleted theorem Hyperreal.isSt_st

deleted theorem Hyperreal.isSt_st_of_exists_st

deleted theorem Hyperreal.isSt_symm_real

deleted theorem Hyperreal.isSt_trans_real

deleted theorem Hyperreal.lt_neg_of_pos_of_infinitesimal

deleted theorem Hyperreal.lt_of_pos_of_infinitesimal

deleted theorem Hyperreal.lt_of_st_lt

deleted theorem Hyperreal.lt_of_tendsto_zero_of_pos

deleted theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos

deleted theorem Hyperreal.not_infiniteNeg_add_infinitePos

deleted theorem Hyperreal.not_infinitePos_add_infiniteNeg

deleted theorem Hyperreal.not_infinite_add

deleted theorem Hyperreal.not_infinite_iff_exist_lt_gt

deleted theorem Hyperreal.not_infinite_mul

deleted theorem Hyperreal.not_infinite_neg

deleted theorem Hyperreal.not_infinite_of_exists_st

deleted theorem Hyperreal.not_infinite_real

deleted theorem Hyperreal.not_infinite_zero

deleted theorem Hyperreal.not_real_of_infinitesimal_ne_zero

deleted theorem Hyperreal.st_add

deleted theorem Hyperreal.st_eq

deleted theorem Hyperreal.st_eq_sSup

deleted theorem Hyperreal.st_id_real

deleted theorem Hyperreal.st_inv

deleted theorem Hyperreal.st_le_of_le

deleted theorem Hyperreal.st_mul

deleted theorem Hyperreal.st_neg

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

Modified Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

deleted def CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso

deleted def CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso

Deleted Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Deleted Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equifibered.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

deleted theorem CategoryTheory.MorphismProperty.isomorphisms_op

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean

Modified Mathlib/Combinatorics/SimpleGraph/VertexCover.lean

deleted theorem SimpleGraph.vertexCoverNum_le_vertexCoverNum_of_injective

Deleted Mathlib/Computability/Primrec.lean

Modified Mathlib/Computability/Primrec/Basic.lean

deleted theorem Primrec.option_iget

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Fintype/Prod.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.getLastI_eq_getLast?

deleted theorem List.head!_eq_head?

Modified Mathlib/Data/List/Flatten.lean

Modified Mathlib/Data/List/GetD.lean

deleted theorem List.getI_eq_iget_getElem?

Modified Mathlib/Data/Option/Basic.lean

deleted theorem Option.getD_default_eq_iget

deleted theorem Option.iget_mem

deleted theorem Option.iget_of_mem

Modified Mathlib/Data/Option/Defs.lean

deleted theorem Option.iget_some

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Data/SetLike/Basic.lean

Deleted Mathlib/Data/Tree/RBMap.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

Modified Mathlib/Geometry/Manifold/Riemannian/Basic.lean

Deleted Mathlib/Lean/Expr.lean

Deleted Mathlib/Lean/Expr/ReplaceRec.lean

deleted def Lean.Expr.replaceRec

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

deleted theorem TensorProduct.coe_finsuppScalarRight'

deleted theorem TensorProduct.finsuppLeft'_apply

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

deleted theorem Lagrange.interpolate_poly_eq_self

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

Deleted Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

deleted theorem QuadraticForm.complex_equivalent

deleted theorem QuadraticForm.equivalent_sum_squares

Modified Mathlib/Logic/Basic.lean

deleted theorem imp_and_neg_imp_iff

Modified Mathlib/Logic/Encodable/Basic.lean

deleted theorem Encodable.surjective_decode_iget

Modified Mathlib/Logic/Relation.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

Modified Mathlib/NumberTheory/ModularForms/SlashActions.lean

deleted theorem ModularForm.prod_fintype_slash

Modified Mathlib/Order/Antichain.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/Comparable.lean

deleted theorem AntisymmRel.compRel

deleted theorem AntisymmRel.compRel_congr

deleted theorem AntisymmRel.compRel_congr_left

deleted theorem AntisymmRel.compRel_congr_right

deleted theorem CompRel.of_antisymmRel_of_compRel

deleted theorem CompRel.of_compRel_of_antisymmRel

deleted theorem CompRel.of_ge

deleted theorem CompRel.of_gt

deleted theorem CompRel.of_le

deleted theorem CompRel.of_lt

deleted theorem CompRel.of_rel

deleted theorem CompRel.of_rel_symm

deleted theorem CompRel.refl

deleted theorem CompRel.rfl

deleted theorem CompRel.symm

deleted def CompRel

deleted theorem compRel_comm

deleted theorem compRel_of_total

deleted theorem compRel_swap

deleted theorem compRel_swap_apply

deleted def linearOrderOfComprel

deleted theorem not_compRel_iff

deleted theorem not_incompRel_iff

Modified Mathlib/Order/Defs/Unbundled.lean

Modified Mathlib/Order/Notation.lean

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/Order/WellFounded.lean

Modified Mathlib/Probability/Moments/SubGaussian.lean

Modified Mathlib/Probability/Process/HittingTime.lean

Modified Mathlib/Probability/Process/Predictable.lean

deleted theorem MeasureTheory.Predictable.stronglyAdapted

Modified Mathlib/Probability/UniformOn.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply'

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/Finiteness/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

deleted theorem HahnSeries.BddBelow_zero

deleted theorem HahnSeries.forallLTEqZero_supp_BddBelow

deleted theorem HahnSeries.order_ofForallLtEqZero

deleted theorem HahnSeries.suppBddBelow_supp_PWO

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Ideal/Colon.lean

deleted theorem Submodule.mem_colon'

Modified Mathlib/RingTheory/Ideal/IsPrimary.lean

Modified Mathlib/RingTheory/Ideal/Prime.lean

deleted theorem Ideal.bot_prime

Modified Mathlib/RingTheory/Kaehler/TensorProduct.lean

Modified Mathlib/RingTheory/KrullDimension/Regular.lean

deleted theorem ringKrullDim_le_ringKrullDim_add_card

deleted theorem ringKrullDim_le_ringKrullDim_add_spanFinrank

Modified Mathlib/RingTheory/Lasker.lean

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean

Modified Mathlib/RingTheory/Nakayama.lean

Modified Mathlib/RingTheory/OreLocalization/OreSet.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean

Modified Mathlib/RingTheory/Smooth/NoetherianDescent.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

deleted theorem Valuation.IsEquiv.ne_zero

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

deleted theorem ValuativeRel.vle_mul_right

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.mk_emptyCollection

deleted theorem Cardinal.mk_range_eq_lift

deleted theorem Cardinal.nat_lt_aleph0

Modified Mathlib/SetTheory/Cardinal/ENat.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Pigeonhole.lean

Modified Mathlib/SetTheory/Ordinal/CantorNormalForm.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

deleted theorem Ordinal.natCast_opow

Modified Mathlib/SetTheory/Ordinal/Topology.lean

deleted theorem Ordinal.isOpen_iff

deleted theorem Ordinal.isOpen_singleton_iff

deleted theorem Ordinal.isSuccLimit_of_mem_frontier

deleted theorem Ordinal.nhds_eq_pure

Modified Mathlib/SetTheory/ZFC/Ordinal.lean

Modified Mathlib/Tactic.lean

Deleted Mathlib/Tactic/Linter/CommandStart.lean

Modified Mathlib/Tactic/Linter/Whitespace.lean

Modified Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean

Modified Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean

Modified Mathlib/Topology/Algebra/Valued/WithVal.lean

deleted def WithVal.equivWithVal

deleted theorem WithVal.equivWithVal_apply

deleted theorem WithVal.equivWithVal_symm

deleted theorem WithVal.equivWithVal_symm_apply

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/EMetricSpace/Defs.lean

Modified Mathlib/Topology/EMetricSpace/Diam.lean

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

Modified Mathlib/Topology/Instances/NNReal/Lemmas.lean

deleted theorem NNReal.tendsto_of_antitone

deleted theorem Real.tendsto_of_bddAbove_monotone

deleted theorem Real.tendsto_of_bddBelow_antitone

Modified Mathlib/Topology/MetricSpace/Closeds.lean

deleted theorem TopologicalSpace.NonemptyCompacts.isClosed_in_closeds

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Modified Mathlib/Topology/MetricSpace/IsometricSMul.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean

Modified Mathlib/Topology/MetricSpace/PartitionOfUnity.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

Modified Mathlib/Topology/MetricSpace/Snowflaking.lean

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean

Modified Mathlib/Topology/MetricSpace/Thickening.lean

Modified Mathlib/Topology/Order.lean

deleted theorem TopologicalSpace.eq_top_iff_forall_inseparable

deleted theorem TopologicalSpace.ne_top_iff_exists_not_inseparable

deleted theorem inseparable_top

Modified Mathlib/Topology/Order/DenselyOrdered.lean

Modified Mathlib/Topology/Order/MonotoneConvergence.lean

Deleted Mathlib/Util/MemoFix.lean

deleted def injectIntoBaseIO

Modified MathlibTest/Linter/Whitespace.lean