Commit 2026-10-10 09:42 f6768845

View on Github →

chore: delete deprecated declarations to March 2026 (#44240)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/Category/AlgCat/Basic.lean

deleted theorem AlgCat.forget_map

Modified Mathlib/Algebra/Category/CommAlgCat/Basic.lean

deleted theorem CommAlgCat.forget_map

Modified Mathlib/Algebra/Category/CommBialgCat.lean

deleted theorem CommBialgCat.forget_map

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

deleted theorem ModuleCat.forget_map

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

deleted theorem FreeMonoid.toList_cons

deleted theorem FreeMonoid.toList_nil

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

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

deleted theorem Subgroup.mul_comm_of_mem_isMulCommutative

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Cardinal.lean

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

deleted theorem Rat.div_lt_div_iff_mul_lt_mul

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Star/Subalgebra.lean

Modified Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Homology/HomotopyInvariance.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

deleted theorem IsSelfAdjoint.spectrum_nonempty

deleted theorem NNReal.spectrum_nonempty

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Range.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

deleted theorem CFC.spectrum_nonempty

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

Modified Mathlib/Analysis/Complex/Harmonic/Analytic.lean

Modified Mathlib/Analysis/Convex/Cone/InnerDual.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

deleted theorem EuclideanSpace.dist_single_same

deleted theorem EuclideanSpace.edist_single_same

deleted theorem EuclideanSpace.nndist_single_same

deleted theorem EuclideanSpace.nnnorm_single

deleted theorem EuclideanSpace.norm_single

deleted theorem EuclideanSpace.ofLp_single

deleted theorem EuclideanSpace.single_apply

deleted theorem EuclideanSpace.single_eq_zero_iff

deleted theorem EuclideanSpace.toLp_single

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Matrix/Hermitian.lean

deleted theorem Matrix.isHermitian_iff_isSymmetric

Modified Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

deleted theorem ContinuousAffineMap.toConstProdContinuousLinearMap_fst

deleted theorem ContinuousAffineMap.toConstProdContinuousLinearMap_snd

Modified Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

deleted theorem PiLp.dist_toLp_single_same

deleted theorem PiLp.edist_toLp_single_same

deleted theorem PiLp.nndist_toLp_single_same

deleted theorem PiLp.nnnorm_toLp_single

deleted theorem PiLp.norm_toLp_single

Modified Mathlib/Analysis/Normed/Module/Dual.lean

deleted theorem NormedSpace.eq_iff_forall_dual_eq

deleted theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero

deleted theorem NormedSpace.eq_zero_of_forall_dual_eq_zero

Modified Mathlib/Analysis/Normed/Operator/Compact/Basic.lean

Modified Mathlib/Analysis/Normed/Operator/Compact/FiniteDimension.lean

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

deleted def WithAbs.equivWithAbs

deleted theorem WithAbs.equivWithAbs_equiv_symm_apply

deleted theorem WithAbs.equivWithAbs_symm

deleted theorem WithAbs.equivWithAbs_symm_equiv_symm_apply

deleted theorem WithAbs.equiv_equivWithAbs_symm_apply

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

Modified Mathlib/Analysis/SpecialFunctions/Integrability/PosLog.lean

Modified Mathlib/Analysis/SpecialFunctions/Stirling.lean

deleted theorem Stirling.log_stirlingSeq_sdiff_le_geo_sum

deleted theorem Stirling.log_stirlingSeq_sub_log_stirlingSeq_succ

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/Basic/Logic/Basic.lean

Modified Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Types/Colimits.lean

deleted theorem CategoryTheory.Limits.Types.Colimit.w_apply

deleted theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply

deleted theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply

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

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Mon.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

Modified Mathlib/CategoryTheory/Sites/CartesianMonoidal.lean

Modified Mathlib/CategoryTheory/Sites/ConstantSheaf.lean

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

deleted theorem CategoryTheory.Sheaf.cond

Modified Mathlib/CategoryTheory/Subobject/Classifier/Defs.lean

Modified Mathlib/CategoryTheory/Types/Basic.lean

deleted theorem CategoryTheory.FunctorToTypes.comp

deleted theorem CategoryTheory.FunctorToTypes.map_comp_apply

deleted theorem CategoryTheory.FunctorToTypes.map_id_apply

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted def SimpleGraph.IsSubgraph

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/LineGraph.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean

deleted theorem SimpleGraph.Walk.support_eq_cons

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean

deleted theorem SimpleGraph.Walk.support_eq_concat

Modified Mathlib/Computability/Reduce.lean

Modified Mathlib/Computability/TuringMachine/Computable.lean

Modified Mathlib/Condensed/Basic.lean

deleted theorem CondensedSet.hom_naturality_apply

Modified Mathlib/Condensed/Discrete/LocallyConstant.lean

Modified Mathlib/Condensed/Light/Basic.lean

deleted theorem LightCondSet.hom_naturality_apply

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

Modified Mathlib/Data/Finset/Lattice/Fold.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Int/Init.lean

Modified Mathlib/Data/Nat/Bits.lean

deleted def Nat.boddDiv2

deleted theorem Nat.boddDiv2_eq

Modified Mathlib/Data/Nat/Digits/Lemmas.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

deleted theorem Nat.factorizationEquiv_inv_apply

Modified Mathlib/Data/Nat/Factorization/Defs.lean

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/Data/Nat/PadicValNat.lean

Modified Mathlib/Data/Nat/Size.lean

Modified Mathlib/Data/PFunctor/Multivariate/W.lean

Modified Mathlib/Data/Set/Basic.lean

deleted theorem Set.not_top_subset

Modified Mathlib/Data/Set/Function.lean

Modified Mathlib/Data/Sym/Sym2.lean

deleted def Sym2.fromRelOrderEmbedding

Modified Mathlib/Dynamics/OmegaLimit.lean

Modified Mathlib/Geometry/Convex/Cone/Basic.lean

deleted theorem Convex.mem_toCone'

deleted theorem Convex.mem_toCone

deleted theorem Convex.subset_toCone

deleted def Convex.toCone

deleted theorem Convex.toCone_eq_sInf

deleted theorem Convex.toCone_isLeast

deleted theorem ConvexCone.IsGenerating.mono

deleted theorem ConvexCone.IsGenerating.of_top_le_span

deleted theorem ConvexCone.IsGenerating.span_eq_top

deleted theorem ConvexCone.IsGenerating.top_le_span

deleted def ConvexCone.IsGenerating

deleted theorem ConvexCone.isGenerating_bot

deleted theorem ConvexCone.isGenerating_bot_iff

deleted theorem ConvexCone.isGenerating_top

deleted theorem convexHull_toCone_eq_sInf

deleted theorem convexHull_toCone_isLeast

Modified Mathlib/Geometry/Convex/Cone/Dual.lean

Modified Mathlib/Geometry/Convex/Cone/Pointed.lean

Modified Mathlib/GroupTheory/Coxeter/Length.lean

deleted theorem CoxeterSystem.length_mul_ge_length_sub_length'

deleted theorem CoxeterSystem.length_mul_ge_length_sub_length

deleted theorem CoxeterSystem.length_mul_ge_max

Modified Mathlib/GroupTheory/Coxeter/Matrix.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Modified Mathlib/GroupTheory/Subgroup/Centralizer.lean

Modified Mathlib/GroupTheory/Subgroup/Saturated.lean

Modified Mathlib/GroupTheory/Submonoid/Centralizer.lean

Modified Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

Modified Mathlib/Lean/MessageData/Trace.lean

deleted def Lean.MessageData.stripTraceResultPrefix

deleted def Lean.MessageData.traceResultOf

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

deleted def LinearMap.BilinForm.IsOrtho

deleted theorem LinearMap.BilinForm.isOrtho_def

deleted theorem LinearMap.BilinForm.isOrtho_smul_left

deleted theorem LinearMap.BilinForm.isOrtho_smul_right

deleted theorem LinearMap.BilinForm.isOrtho_zero_left

deleted theorem LinearMap.BilinForm.isOrtho_zero_right

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

deleted def LinearMap.IsOrtho

deleted theorem LinearMap.isOrtho_def

deleted theorem LinearMap.isOrtho_flip

deleted theorem LinearMap.isOrtho_zero_left

deleted theorem LinearMap.isOrtho_zero_right

deleted theorem LinearMap.ortho_smul_left

deleted theorem LinearMap.ortho_smul_right

Modified Mathlib/Logic/Encodable/Basic.lean

Modified Mathlib/Logic/Equiv/Fin/Rotate.lean

deleted theorem finRotate_succ_apply

deleted theorem finRotate_succ_symm_apply

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/Pairwise.lean

Modified Mathlib/Logic/Relation.lean

deleted theorem Relation.reflTransGen_idem

deleted theorem Relation.reflexive_reflGen

deleted theorem Relation.reflexive_reflTransGen

deleted theorem Relation.transGen_idem

Modified Mathlib/MeasureTheory/Function/JacobianOneDim.lean

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

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/SumMeasure.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

deleted theorem MeasureTheory.Measure.forall_measure_inter_spanningSets_eq_zero

Modified Mathlib/NumberTheory/Height/Basic.lean

Modified Mathlib/NumberTheory/Modular.lean

deleted theorem ModularGroup.c_eq_zero

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

Modified Mathlib/NumberTheory/Primorial.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/Cofinal.lean

Modified Mathlib/Order/Defs/Unbundled.lean

deleted def Reflexive

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/CountableInter.lean

Modified Mathlib/Order/GaloisConnection/Defs.lean

Modified Mathlib/Order/GameAdd.lean

deleted theorem Prod.GameAdd.induction

deleted theorem Sym2.GameAdd.induction

Modified Mathlib/Order/Hom/WithTopBot.lean

Modified Mathlib/Order/IsNormal.lean

Modified Mathlib/Order/MinMax.lean

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem Order.not_isSuccLimit_succ_of_not_isMax

deleted theorem Order.not_isSuccPrelimit_succ_of_not_isMax

Modified Mathlib/Order/SuccPred/Relation.lean

Modified Mathlib/Probability/Distributions/Cauchy.lean

Modified Mathlib/Probability/Distributions/Geometric.lean

deleted def ProbabilityTheory.geometricPMF

deleted def ProbabilityTheory.geometricPMFReal

deleted theorem ProbabilityTheory.geometricPMFRealSum

deleted theorem ProbabilityTheory.geometricPMFReal_nonneg

deleted theorem ProbabilityTheory.geometricPMFReal_pos

deleted theorem ProbabilityTheory.measurable_geometricPMFReal

deleted theorem ProbabilityTheory.stronglyMeasurable_geometricPMFReal

Modified Mathlib/Probability/Distributions/Poisson/Basic.lean

deleted theorem ProbabilityTheory.measurable_poissonPMFReal

deleted def ProbabilityTheory.poissonPMF

deleted def ProbabilityTheory.poissonPMFReal

deleted theorem ProbabilityTheory.poissonPMFReal_nonneg

deleted theorem ProbabilityTheory.poissonPMFReal_ofReal_eq_poissonPMF

deleted theorem ProbabilityTheory.poissonPMFReal_pos

deleted theorem ProbabilityTheory.stronglyMeasurable_poissonPMFReal

Modified Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean

deleted theorem ProbabilityTheory.binomial_tendsto_poissonPMFReal_atTop

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted theorem Ideal.inf_eq_mul_of_isCoprime

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/Perfection.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

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

deleted def ValuativeRel.ValueGroupWithZero.valueGroupWithZero_equiv_valueGroup₀

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted theorem Cardinal.aleph0_lt_iff_aleph_one_le

deleted theorem Cardinal.aleph1_le_mk

deleted theorem Cardinal.aleph1_le_mk_iff

deleted theorem Cardinal.aleph_add_one

deleted theorem Cardinal.aleph_one_le_lift

deleted theorem Cardinal.aleph_succ

deleted theorem Cardinal.countable_iff_lt_aleph_one

deleted theorem Cardinal.lift_lt_aleph_one

deleted theorem Cardinal.preAleph_add_one

deleted theorem Cardinal.preAleph_succ

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.nat_succ

Modified Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

deleted theorem Ordinal.aleph0_le_cof

deleted theorem Ordinal.blsub_lt_ord

deleted theorem Ordinal.blsub_lt_ord_lift

deleted theorem Ordinal.bsup_lt_ord

deleted theorem Ordinal.bsup_lt_ord_lift

deleted theorem Ordinal.cof_blsub_le

deleted theorem Ordinal.cof_blsub_le_lift

deleted theorem Ordinal.cof_bsup_le

deleted theorem Ordinal.cof_bsup_le_lift

deleted theorem Ordinal.cof_eq'

deleted theorem Ordinal.cof_eq_sInf_lsub

deleted theorem Ordinal.cof_iSup_le

deleted theorem Ordinal.cof_iSup_le_lift

deleted theorem Ordinal.cof_lsub_def_nonempty

deleted theorem Ordinal.cof_lsub_le

deleted theorem Ordinal.cof_lsub_le_lift

deleted theorem Ordinal.exists_blsub_cof

deleted theorem Ordinal.exists_lsub_cof

deleted theorem Ordinal.iSup_lt_lift

deleted theorem Ordinal.iSup_lt_ord_lift

deleted theorem Ordinal.le_cof_iff_blsub

deleted theorem Ordinal.le_cof_iff_lsub

deleted theorem Ordinal.lsub_lt_ord

deleted theorem Ordinal.lsub_lt_ord_lift

Modified Mathlib/SetTheory/Cardinal/Order.lean

deleted theorem Cardinal.add_one_le_succ

deleted theorem Cardinal.succ_def

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

deleted theorem Cardinal.blsub_lt_ord_lift_of_isRegular

deleted theorem Cardinal.blsub_lt_ord_of_isRegular

deleted theorem Cardinal.bsup_lt_ord_lift_of_isRegular

deleted theorem Cardinal.bsup_lt_ord_of_isRegular

deleted theorem Cardinal.iSup_lt_lift_of_isRegular

deleted theorem Cardinal.iSup_lt_of_isRegular

deleted theorem Cardinal.iSup_lt_ord_lift_of_isRegular

deleted theorem Cardinal.iSup_lt_ord_of_isRegular

deleted theorem Cardinal.isRegular_aleph_succ

deleted theorem Cardinal.isRegular_preAleph_succ

deleted theorem Cardinal.lsub_lt_ord_lift_of_isRegular

deleted theorem Cardinal.lsub_lt_ord_of_isRegular

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted theorem Cardinal.card_typein_toType_lt

deleted theorem Ordinal.lt_one_iff_zero

Modified Mathlib/SetTheory/Ordinal/Family.lean

deleted theorem Ordinal.IsNormal.blsub_eq

deleted theorem Ordinal.IsNormal.bsup_eq

deleted def Ordinal.blsub

deleted theorem Ordinal.blsub_comp

deleted theorem Ordinal.blsub_congr

deleted theorem Ordinal.blsub_const

deleted theorem Ordinal.blsub_eq_blsub

deleted theorem Ordinal.blsub_eq_lsub'

deleted theorem Ordinal.blsub_eq_lsub

deleted theorem Ordinal.blsub_eq_of_brange_eq

deleted theorem Ordinal.blsub_eq_zero_iff

deleted theorem Ordinal.blsub_id

deleted theorem Ordinal.blsub_le

deleted theorem Ordinal.blsub_le_bsup_succ

deleted theorem Ordinal.blsub_le_iff

deleted theorem Ordinal.blsub_le_of_brange_subset

deleted theorem Ordinal.blsub_one

deleted theorem Ordinal.blsub_pos

deleted theorem Ordinal.blsub_succ_of_mono

deleted theorem Ordinal.blsub_type

deleted theorem Ordinal.blsub_zero

deleted theorem Ordinal.bsup_comp

deleted theorem Ordinal.bsup_eq_blsub

deleted theorem Ordinal.bsup_eq_blsub_iff_lt_bsup

deleted theorem Ordinal.bsup_eq_blsub_iff_succ

deleted theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit

deleted theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub

deleted theorem Ordinal.bsup_id_add_one

deleted theorem Ordinal.bsup_id_limit

deleted theorem Ordinal.bsup_id_succ

deleted theorem Ordinal.bsup_le_blsub

deleted theorem Ordinal.bsup_succ_eq_blsub

deleted theorem Ordinal.bsup_succ_le_blsub

deleted theorem Ordinal.iSup_eq_lsub

deleted theorem Ordinal.iSup_eq_lsub_iff

deleted theorem Ordinal.iSup_eq_lsub_iff_lt_iSup

deleted theorem Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub

deleted theorem Ordinal.iSup_eq_of_range_eq

deleted theorem Ordinal.iSup_le_lsub

deleted theorem Ordinal.iSup_typein_limit

deleted theorem Ordinal.iSup_typein_succ

deleted theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq

deleted theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq

deleted def Ordinal.lsub

deleted theorem Ordinal.lsub_const

deleted theorem Ordinal.lsub_empty

deleted theorem Ordinal.lsub_eq_blsub'

deleted theorem Ordinal.lsub_eq_blsub

deleted theorem Ordinal.lsub_eq_lsub

deleted theorem Ordinal.lsub_eq_of_range_eq

deleted theorem Ordinal.lsub_eq_zero_iff

deleted theorem Ordinal.lsub_le

deleted theorem Ordinal.lsub_le_iff

deleted theorem Ordinal.lsub_le_of_range_subset

deleted theorem Ordinal.lsub_le_succ_iSup

deleted theorem Ordinal.lsub_notMem_range

deleted theorem Ordinal.lsub_pos

deleted theorem Ordinal.lsub_sum

deleted theorem Ordinal.lsub_typein

deleted theorem Ordinal.lsub_unique

deleted theorem Ordinal.lt_blsub

deleted theorem Ordinal.lt_blsub_iff

deleted theorem Ordinal.lt_lsub

deleted theorem Ordinal.lt_lsub_iff

deleted theorem Ordinal.nonempty_compl_range

deleted theorem Ordinal.succ_iSup_eq_lsub_iff

deleted theorem Ordinal.succ_iSup_le_lsub_iff

Modified Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

Modified Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

deleted theorem Ordinal.IsFundamentalSequence.blsub_eq

deleted theorem Ordinal.IsFundamentalSequence.id_of_le_cof

deleted theorem Ordinal.IsFundamentalSequence.of_isNormal

deleted theorem Ordinal.IsFundamentalSequence.ord_cof

deleted theorem Ordinal.IsFundamentalSequence.trans

deleted def Ordinal.IsFundamentalSequence

deleted theorem Ordinal.exists_fundamental_sequence

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean

deleted theorem Ordinal.accPt_subtype

Modified Mathlib/SetTheory/Ordinal/Univ.lean

deleted theorem Ordinal.liftPrincipalSeg_top'

deleted theorem Ordinal.univ_id

Modified Mathlib/SetTheory/ZFC/Basic.lean

deleted theorem ZFSet.le_def

deleted theorem ZFSet.lt_def

Modified Mathlib/SetTheory/ZFC/PSet.lean

deleted theorem PSet.le_def

deleted theorem PSet.lt_def

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean

Modified Mathlib/Topology/Algebra/ValuativeRel/ValuativeTopology.lean

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

Modified Mathlib/Topology/Bases.lean

deleted theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

deleted theorem BoundedContinuousFunction.coe_nsmulRec

Modified Mathlib/Topology/DiscreteSubset.lean

Modified Mathlib/Topology/Instances/Discrete.lean

Modified Mathlib/Topology/LocallyFinsupp.lean

Modified Mathlib/Topology/Maps/Basic.lean

Modified Mathlib/Topology/Sheaves/Presheaf.lean

Modified Mathlib/Topology/Subpath.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean