Commit 2023-10-17 09:07 fe9572d2

View on Github →

chore: remove many Type _ before the colon (#7718) We have turned to Type* instead of Type _, but many of them remained in mathlib because the straight replacement did not work. In general, having Type _ before the colon is a code smell, though, as it hides which types should be in the same universe and which shouldn't, and is not very robust. This PR replaces most of the remaining Type _ before the colon (except those in category theory) by Type* or Type u. This has uncovered a few bugs (where declarations were not as polymorphic as they should be). I had to increase heartbeats at two places when replacing Type _ by Type*, but I think it's worth it as it's really more robust.

Estimated changes

modified def AlgHom.Simps.apply
modified theorem iterate_map_mul
modified theorem Finset.image₂_def
modified structure Levenshtein.Cost
modified theorem Multiset.map_hcongr
modified theorem Multiset.bind_hcongr
modified theorem Option.bind_eq_bind
modified theorem Option.map₂_def
modified def MvPFunctor.objAppend1
modified def MvQPF.corecF
modified theorem MvQPF.corecF_eq
modified theorem MvQPF.Fix.ind_rec
modified theorem MvQPF.Fix.rec_unique
modified def MvQPF.recF
modified theorem MvQPF.recF_eq'
modified theorem MvQPF.recF_eq
modified theorem MvQPF.recF_eq_of_wEquiv
modified theorem Equivalence.quot_mk_eq_iff
modified theorem Set.image2_def
modified def TypeVec.Curry
modified def TypeVec.RelLast
modified theorem TypeVec.appendFun_comp_id
modified theorem PerfectRing.ofSurjective
modified theorem PerfectRing.toPerfectField
modified theorem QuotientGroup.mk_prod
modified theorem ConjClasses.mk_bijOn
modified def ConjClasses.noncenter
modified theorem linearIndependent_le_basis
modified theorem Equiv.piCongrLeft_sum_inl
modified theorem Equiv.piCongrLeft_sum_inr
modified theorem cast_inj
modified theorem DistLat.coe_of
modified def DistLat.of
modified theorem Filter.seq_eq_filter_seq
modified theorem PMF.monad_map_eq_map
modified theorem PMF.monad_seq_eq_seq
modified theorem Algebra.adjoin_int
modified theorem Algebra.adjoin_nat
modified theorem isDedekindRing_iff
modified theorem isNilpotent_sum
modified theorem Cardinal.add_mk_eq_max'
modified theorem Cardinal.add_mk_eq_max
modified theorem Cardinal.mul_mk_eq_max
modified structure IsometryEquiv