Commit 2024-08-05 08:52 5025874d

View on Github →

chore: move toolchain to v4.11.0-rc1 (#15513)

Estimated changes

Modified Archive/MiuLanguage/DecisionNec.lean

Modified Archive/MiuLanguage/DecisionSuf.lean

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified LongestPole/Main.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/Hom.lean

deleted theorem AlgHom.ext_iff

Modified Mathlib/Algebra/Algebra/NonUnitalHom.lean

deleted theorem NonUnitalAlgHom.ext_iff

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/BigOperators/Group/List.lean

deleted theorem List.length_join

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

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

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

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

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

Modified Mathlib/Algebra/CharP/Defs.lean

Modified Mathlib/Algebra/CubicDiscriminant.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

Modified Mathlib/Algebra/Free.lean

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

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

deleted theorem MulEquiv.ext_iff

Modified Mathlib/Algebra/Group/Units.lean

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Homology/ShortComplex/Basic.lean

Modified Mathlib/Algebra/Lie/Basic.lean

deleted theorem LieHom.ext_iff

deleted theorem LieModuleHom.ext_iff

Modified Mathlib/Algebra/Lie/DirectSum.lean

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

added theorem LieModule.Weight.ext_iff'

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

deleted theorem LinearEquiv.ext_iff

Modified Mathlib/Algebra/Module/Injective.lean

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

deleted theorem LinearMap.ext_ring_iff

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/List.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

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

Modified Mathlib/Algebra/Quaternion.lean

deleted theorem Quaternion.ext_iff

Modified Mathlib/Algebra/Ring/Equiv.lean

Modified Mathlib/Algebra/Ring/Ext.lean

deleted theorem CommRing.ext_iff

deleted theorem CommSemiring.ext_iff

deleted theorem Distrib.ext_iff

deleted theorem NonAssocRing.ext_iff

deleted theorem NonAssocSemiring.ext_iff

deleted theorem NonUnitalCommRing.ext_iff

deleted theorem NonUnitalCommSemiring.ext_iff

deleted theorem NonUnitalNonAssocCommRing.ext_iff

deleted theorem NonUnitalNonAssocCommSemiring.ext_iff

deleted theorem NonUnitalNonAssocRing.ext_iff

deleted theorem NonUnitalNonAssocSemiring.ext_iff

deleted theorem NonUnitalRing.ext_iff

deleted theorem NonUnitalSemiring.ext_iff

deleted theorem Ring.ext_iff

deleted theorem Semiring.ext_iff

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

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

Modified Mathlib/Algebra/Star/StarAlgHom.lean

deleted theorem StarAlgEquiv.ext_iff

Modified Mathlib/Algebra/Star/StarRingHom.lean

deleted theorem StarRingEquiv.ext_iff

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

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

Modified Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/WeakOperatorTopology.lean

deleted theorem ContinuousLinearMapWOT.ext_inner_iff

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

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

Modified Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean

Modified Mathlib/Analysis/NormedSpace/ENorm.lean

deleted theorem ENorm.ext_iff

Modified Mathlib/CategoryTheory/Bicategory/Coherence.lean

Modified Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

Modified Mathlib/CategoryTheory/Category/Basic.lean

Modified Mathlib/CategoryTheory/Category/Bipointed.lean

Modified Mathlib/CategoryTheory/Category/PartialFun.lean

Modified Mathlib/CategoryTheory/Category/Pointed.lean

Modified Mathlib/CategoryTheory/Category/TwoP.lean

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

Modified Mathlib/CategoryTheory/Comma/Basic.lean

Modified Mathlib/CategoryTheory/Comma/Presheaf.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow.lean

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

Modified Mathlib/CategoryTheory/Dialectica/Basic.lean

Modified Mathlib/CategoryTheory/DifferentialObject.lean

Modified Mathlib/CategoryTheory/Endofunctor/Algebra.lean

Modified Mathlib/CategoryTheory/Filtered/Small.lean

Modified Mathlib/CategoryTheory/Functor/Category.lean

modified theorem CategoryTheory.NatTrans.ext'

Modified Mathlib/CategoryTheory/Galois/Prorepresentability.lean

Modified Mathlib/CategoryTheory/GradedObject/Monoidal.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

Modified Mathlib/CategoryTheory/GuitartExact/Basic.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

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

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

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

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

Modified Mathlib/CategoryTheory/Limits/Types.lean

deleted theorem CategoryTheory.Limits.Types.limit_ext_iff

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Localization/Resolution.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

modified theorem CategoryTheory.Comonad.Coalgebra.Hom.ext'

modified theorem CategoryTheory.Monad.Algebra.Hom.ext'

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monad/Coequalizer.lean

Modified Mathlib/CategoryTheory/Monad/Equalizer.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimod.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

modified theorem Comon_.ext

Modified Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

Modified Mathlib/CategoryTheory/Monoidal/Mod_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

Modified Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean

Modified Mathlib/CategoryTheory/PathCategory.lean

Modified Mathlib/CategoryTheory/Quotient.lean

Modified Mathlib/CategoryTheory/Shift/SingleFunctors.lean

modified theorem CategoryTheory.SingleFunctors.hom_ext

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

Modified Mathlib/CategoryTheory/Sites/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Sites/Types.lean

Modified Mathlib/CategoryTheory/Sites/Whiskering.lean

Modified Mathlib/CategoryTheory/Square.lean

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/CategoryTheory/Thin.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Combinatorics/Colex.lean

Modified Mathlib/Combinatorics/Enumerative/Composition.lean

Modified Mathlib/Combinatorics/Enumerative/Partition.lean

Modified Mathlib/Combinatorics/Quiver/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

modified theorem SimpleGraph.comap_id

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

modified theorem SimpleGraph.Walk.IsPath.tail

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

deleted theorem SimpleGraph.Walk.adj_getVert_one

added theorem SimpleGraph.Walk.adj_sndOfNotNil

added theorem SimpleGraph.Walk.cons_getVert

added theorem SimpleGraph.Walk.cons_getVert_succ

added theorem SimpleGraph.Walk.cons_sndOfNotNil

modified theorem SimpleGraph.Walk.cons_tail_eq

deleted def SimpleGraph.Walk.drop

deleted theorem SimpleGraph.Walk.getVert_cons

deleted theorem SimpleGraph.Walk.getVert_cons_one

deleted theorem SimpleGraph.Walk.getVert_cons_succ

deleted theorem SimpleGraph.Walk.getVert_copy

added theorem SimpleGraph.Walk.getVert_one

modified theorem SimpleGraph.Walk.getVert_tail

deleted theorem SimpleGraph.Walk.not_nil_iff_lt_length

added def SimpleGraph.Walk.sndOfNotNil

modified theorem SimpleGraph.Walk.support_tail

deleted theorem SimpleGraph.Walk.support_tail_of_not_nil

modified def SimpleGraph.Walk.tail

deleted theorem SimpleGraph.Walk.tail_cons_eq

deleted theorem SimpleGraph.Walk.tail_cons_nil

added theorem SimpleGraph.Walk.tail_support_eq_support_tail

Modified Mathlib/Computability/Primrec.lean

Modified Mathlib/Control/Traversable/Basic.lean

deleted theorem ApplicativeTransformation.ext_iff

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

Modified Mathlib/Data/Finmap.lean

Modified Mathlib/Data/Finset/Basic.lean

modified theorem Finset.empty_toList

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Fintype/Fin.lean

Modified Mathlib/Data/List/AList.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.Sublist.map

deleted theorem List.attach_eq_nil

deleted theorem List.attach_map_coe'

deleted theorem List.attach_map_val'

deleted theorem List.attach_map_val

deleted theorem List.attach_nil

added theorem List.filter_subset'

deleted theorem List.filter_subset

deleted theorem List.foldl_join

deleted theorem List.foldr_join

deleted theorem List.get?_pmap

deleted theorem List.getElem?_pmap

deleted theorem List.getElem_eq_getElem?

deleted theorem List.getElem_pmap

deleted theorem List.getLast?_append

modified theorem List.getLast_concat'

deleted theorem List.getLast_cons

deleted theorem List.getLast_pmap

deleted theorem List.getLast_reverse

deleted theorem List.get_pmap

deleted theorem List.head?_append

deleted theorem List.head_mem

deleted theorem List.head_replicate

deleted theorem List.length_attach

deleted theorem List.length_pmap

deleted theorem List.map_pmap

deleted theorem List.mem_attach

added theorem List.mem_getLast?_append_of_mem_getLast?

added theorem List.mem_head?_append_of_mem_head?

deleted theorem List.mem_pmap

deleted theorem List.pmap_append'

deleted theorem List.pmap_append

deleted theorem List.pmap_congr

deleted theorem List.pmap_eq_map

deleted theorem List.pmap_eq_map_attach

deleted theorem List.pmap_eq_nil

deleted theorem List.pmap_map

deleted theorem List.reverse_eq_iff

deleted theorem List.sublist_replicate_iff

deleted theorem List.takeWhile_cons_of_neg

deleted theorem List.takeWhile_cons_of_pos

Modified Mathlib/Data/List/Chain.lean

Modified Mathlib/Data/List/Count.lean

deleted theorem List.countP_attach

deleted theorem List.count_attach

deleted theorem List.length_filter_lt_length_iff_exists

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/Destutter.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/EditDistance/Defs.lean

Modified Mathlib/Data/List/Enum.lean

deleted theorem List.enumFrom_append

deleted theorem List.enumFrom_cons'

deleted theorem List.enumFrom_eq_nil

deleted theorem List.enumFrom_map

deleted theorem List.enumFrom_map_snd

deleted theorem List.enumFrom_singleton

deleted theorem List.enum_append

deleted theorem List.enum_cons'

deleted theorem List.enum_eq_nil

deleted theorem List.enum_map

deleted theorem List.enum_map_snd

deleted theorem List.enum_singleton

deleted theorem List.fst_lt_add_of_mem_enumFrom

deleted theorem List.fst_lt_of_mem_enum

deleted theorem List.getElem?_enum

deleted theorem List.getElem?_enumFrom

deleted theorem List.getElem_enum

deleted theorem List.getElem_enumFrom

deleted theorem List.le_fst_of_mem_enumFrom

deleted theorem List.map_fst_add_enumFrom_eq_enumFrom

deleted theorem List.map_fst_add_enum_eq_enumFrom

deleted theorem List.mem_enumFrom

deleted theorem List.snd_mem_of_mem_enum

deleted theorem List.snd_mem_of_mem_enumFrom

Modified Mathlib/Data/List/Forall2.lean

Modified Mathlib/Data/List/GetD.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Intervals.lean

Modified Mathlib/Data/List/Iterate.lean

Modified Mathlib/Data/List/Join.lean

deleted theorem List.join_append

deleted theorem List.join_concat

modified theorem List.join_eq_nil

deleted theorem List.join_join

deleted theorem List.join_reverse

deleted theorem List.reverse_join

Modified Mathlib/Data/List/Lattice.lean

Modified Mathlib/Data/List/NatAntidiagonal.lean

Modified Mathlib/Data/List/Nodup.lean

deleted theorem List.Nodup.erase

deleted theorem List.Nodup.erase_eq_filter

deleted theorem List.Nodup.mem_erase_iff

deleted theorem List.Nodup.not_mem_erase

deleted theorem List.forall_mem_ne

deleted theorem List.nodup_cons

deleted theorem List.nodup_nil

deleted theorem List.nodup_replicate

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Perm.lean

modified theorem List.subperm_cons_self

Modified Mathlib/Data/List/Range.lean

deleted theorem List.enumFrom_eq_zip_range'

deleted theorem List.enum_eq_zip_range

deleted theorem List.nodup_iota

deleted theorem List.nodup_range'

deleted theorem List.nodup_range

deleted theorem List.pairwise_gt_iota

deleted theorem List.pairwise_le_range

deleted theorem List.pairwise_lt_range'

deleted theorem List.pairwise_lt_range

deleted theorem List.range'_one

deleted theorem List.take_range

deleted theorem List.unzip_enumFrom_eq_prod

deleted theorem List.unzip_enum_eq_prod

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/Sort.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/List/Sym.lean

Modified Mathlib/Data/List/TFAE.lean

Modified Mathlib/Data/List/Zip.lean

deleted theorem List.getElem?_zipWith'

deleted theorem List.getElem?_zipWith_eq_some

deleted theorem List.getElem?_zip_eq_some

deleted theorem List.getElem_zip

deleted theorem List.getElem_zipWith

deleted theorem List.lt_length_left_of_zip

deleted theorem List.lt_length_left_of_zipWith

deleted theorem List.lt_length_right_of_zip

deleted theorem List.lt_length_right_of_zipWith

deleted theorem List.map_prod_left_eq_zip

deleted theorem List.map_prod_right_eq_zip

deleted theorem List.mem_zip

deleted theorem List.unzip_eq_map

deleted theorem List.unzip_left

deleted theorem List.unzip_right

deleted theorem List.unzip_zip

deleted theorem List.unzip_zip_left

deleted theorem List.unzip_zip_right

deleted theorem List.zipWith_comm

deleted theorem List.zipWith_comm_of_comm

deleted theorem List.zipWith_distrib_reverse

deleted theorem List.zipWith_same

deleted theorem List.zip_of_prod

deleted theorem List.zip_unzip

Modified Mathlib/Data/Multiset/Basic.lean

modified theorem Multiset.count_replicate

modified theorem Multiset.empty_toList

Modified Mathlib/Data/Multiset/FinsetOps.lean

Modified Mathlib/Data/Multiset/Nodup.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/NNRat/Defs.lean

deleted theorem NNRat.ext_iff

Modified Mathlib/Data/NNReal/Basic.lean

Modified Mathlib/Data/Nat/Defs.lean

deleted theorem Nat.and_forall_succ

deleted theorem Nat.or_exists_succ

Modified Mathlib/Data/Nat/Nth.lean

Modified Mathlib/Data/Option/Basic.lean

deleted theorem Option.get!_none

deleted theorem Option.get!_some

deleted theorem Option.isSome_map

Modified Mathlib/Data/PEquiv.lean

deleted theorem PEquiv.ext_iff

Modified Mathlib/Data/Prod/Basic.lean

Modified Mathlib/Data/Seq/Seq.lean

deleted def Stream'.Seq.ofLazyList

added def Stream'.Seq.ofMLList

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Data/Set/List.lean

Modified Mathlib/Data/Set/Pairwise/Basic.lean

Modified Mathlib/Data/Sigma/Basic.lean

added theorem PSigma.exists'

deleted theorem PSigma.ext_iff

deleted theorem PSigma.subtype_ext_iff

deleted theorem PSigma.«exists»

deleted theorem Sigma.subtype_ext_iff

Modified Mathlib/Data/Sigma/Order.lean

Modified Mathlib/Data/String/Defs.lean

Modified Mathlib/Data/String/Lemmas.lean

Modified Mathlib/Data/Subtype.lean

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/Data/ULift.lean

deleted theorem ULift.ext_iff

Modified Mathlib/Data/Vector/Zip.lean

Modified Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Modified Mathlib/Geometry/Euclidean/Angle/Sphere.lean

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Euclidean/Sphere/Basic.lean

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

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

modified theorem AlgebraicGeometry.SheafedSpace.ext

Modified Mathlib/GroupTheory/Congruence/Basic.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

deleted theorem DistribMulActionHom.ext_iff

deleted theorem DistribMulActionHom.ext_ring_iff

deleted theorem MulSemiringActionHom.ext_iff

Modified Mathlib/GroupTheory/HNNExtension.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/GroupTheory/PushoutI.lean

deleted theorem Monoid.PushoutI.NormalWord.ext_iff

Modified Mathlib/GroupTheory/SemidirectProduct.lean

Modified Mathlib/GroupTheory/Sylow.lean

deleted theorem Sylow.ext_iff

Deleted Mathlib/Init/Data/Nat/GCD.lean

deleted theorem Nat.gcd_def

Modified Mathlib/Lean/Name.lean

modified def allNamesByModule

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

deleted theorem AffineMap.ext_iff

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

deleted theorem ContinuousAffineEquiv.ext_iff

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

deleted theorem Affine.Simplex.ext_iff

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Basic.lean

deleted theorem LinearMap.BilinForm.ext_iff

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/Pi.lean

deleted theorem LinearMap.pi_ext'_iff

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

deleted theorem QuadraticMap.ext_iff

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean

Modified Mathlib/LinearAlgebra/TensorPower.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem exists_eq_right'

deleted theorem exists_or_eq_left'

deleted theorem exists_or_eq_left

deleted theorem exists_or_eq_right'

deleted theorem exists_or_eq_right

deleted theorem exists_prop_congr

deleted theorem exists_prop_of_true

deleted theorem exists_true_left

Modified Mathlib/Logic/Embedding/Basic.lean

deleted theorem Function.Embedding.ext_iff

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

deleted theorem Equiv.ext_iff

Modified Mathlib/Logic/Nontrivial/Basic.lean

Modified Mathlib/Logic/Relation.lean

deleted theorem Acc.TransGen

deleted inductive Relation.TransGen

deleted theorem WellFounded.transGen

deleted theorem acc_transGen_iff

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/MeasureTheory/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

deleted theorem MeasureTheory.AEEqFun.ext_iff

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

deleted theorem MeasureTheory.Lp.ext_iff

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

deleted theorem MeasurableSpace.ext_iff

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

deleted theorem MeasureTheory.Measure.ext_iff

Modified Mathlib/ModelTheory/Basic.lean

deleted theorem FirstOrder.Language.Embedding.ext_iff

deleted theorem FirstOrder.Language.Equiv.ext_iff

deleted theorem FirstOrder.Language.Hom.ext_iff

Modified Mathlib/ModelTheory/ElementaryMaps.lean

deleted theorem FirstOrder.Language.ElementaryEmbedding.ext_iff

Modified Mathlib/ModelTheory/Encoding.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

deleted theorem ArithmeticFunction.ext_iff

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

deleted theorem MulChar.ext_iff

Modified Mathlib/NumberTheory/NumberField/Basic.lean

deleted theorem NumberField.RingOfIntegers.ext_iff

Modified Mathlib/NumberTheory/Pell.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/Order/RelIso/Basic.lean

deleted theorem RelEmbedding.ext_iff

deleted theorem RelHom.ext_iff

deleted theorem RelIso.ext_iff

Modified Mathlib/Order/RelSeries.lean

Modified Mathlib/Probability/ConditionalExpectation.lean

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

deleted theorem PMF.ext_iff

Modified Mathlib/RepresentationTheory/Action/Basic.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

deleted theorem AdicCompletion.AdicCauchySequence.ext_iff

deleted theorem AdicCompletion.ext_iff

Modified Mathlib/RingTheory/Bialgebra/Equiv.lean

deleted theorem BialgEquiv.ext_iff

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

deleted theorem BialgHom.ext_iff

Modified Mathlib/RingTheory/Coalgebra/Equiv.lean

deleted theorem CoalgEquiv.ext_iff

Modified Mathlib/RingTheory/Coalgebra/Hom.lean

deleted theorem CoalgHom.ext_iff

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/IsTensorProduct.lean

Modified Mathlib/RingTheory/MaximalSpectrum.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/RingTheory/PrimeSpectrum.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

deleted theorem AddValuation.ext_iff

deleted theorem Valuation.ext_iff

Modified Mathlib/RingTheory/WittVector/Defs.lean

deleted theorem WittVector.ext_iff

Modified Mathlib/RingTheory/WittVector/Truncated.lean

deleted theorem TruncatedWittVector.ext_iff

Modified Mathlib/SetTheory/ZFC/Basic.lean

deleted theorem Class.ext_iff

deleted theorem ZFSet.ext_iff

Modified Mathlib/Tactic/Abel.lean

Modified Mathlib/Tactic/Attr/Core.lean

Modified Mathlib/Tactic/Linter/Lint.lean

Modified Mathlib/Tactic/Linter/UnusedTactic.lean

Modified Mathlib/Tactic/TFAE.lean

Modified Mathlib/Tactic/Widget/Calc.lean

Modified Mathlib/Tactic/Widget/Conv.lean

Modified Mathlib/Testing/SlimCheck/Functions.lean

modified def SlimCheck.InjectiveFunction.sliceSizes

Modified Mathlib/Testing/SlimCheck/Testable.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

deleted theorem ContinuousAlgHom.ext_iff

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

deleted theorem ContinuousAffineMap.ext_iff

Modified Mathlib/Topology/Algebra/Module/Alternating/Basic.lean

deleted theorem ContinuousAlternatingMap.ext_iff

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

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

deleted theorem ContinuousMultilinearMap.ext_iff

Modified Mathlib/Topology/Basic.lean

Modified Mathlib/Topology/Bornology/Basic.lean

deleted theorem Bornology.ext_iff

Modified Mathlib/Topology/Category/TopCat/OpenNhds.lean

Modified Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean

deleted theorem LocallyConstant.ext_iff

Modified Mathlib/Topology/MetricSpace/Dilation.lean

deleted theorem Dilation.ext_iff

Modified Mathlib/Topology/Metrizable/Uniformity.lean

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified Mathlib/Topology/Sheaves/Sheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/ShrinkingLemma.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Util/AssertNoSorry.lean

Modified Mathlib/Util/LongNames.lean

modified def printNameHashMap

Modified lake-manifest.json

Modified lakefile.lean

Modified lean-toolchain

Modified scripts/check-yaml.lean

Modified scripts/noshake.json

Modified test/DeriveToExpr.lean

Modified test/TCSynth.lean

Modified test/Use.lean

Modified test/Variable.lean

Modified test/eval_elab.lean

Modified test/jacobiSym.lean