Commit 2023-02-13 09:31 0a70c6a6

View on Github →

chore: tidy various files (#2251)

Estimated changes

Modified Mathlib/Algebra/Order/Nonneg/Field.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

added theorem CategoryTheory.Functor.map_comp_hEq'

deleted theorem CategoryTheory.Functor.map_comp_heq'

added theorem CategoryTheory.Functor.postcomp_map_hEq'

deleted theorem CategoryTheory.Functor.postcomp_map_heq'

modified theorem CategoryTheory.congrArg_cast_hom_left

modified theorem CategoryTheory.eqToHom_op

modified theorem CategoryTheory.eqToHom_unop

modified theorem CategoryTheory.inv_eqToHom

Modified Mathlib/Combinatorics/Colex.lean

deleted theorem Colex.colex_lt_of_sSubset

added theorem Colex.colex_lt_of_ssubset

Modified Mathlib/Combinatorics/Quiver/SingleObj.lean

modified theorem Quiver.SingleObj.pathToList_listToPath

modified def Quiver.SingleObj.toPrefunctor

Modified Mathlib/Combinatorics/Young/YoungDiagram.lean

deleted theorem YoungDiagram.cells_sSubset_iff

added theorem YoungDiagram.cells_ssubset_iff

Modified Mathlib/Data/Finset/LocallyFinite.lean

deleted theorem Finset.Icc_sSubset_Icc_left

deleted theorem Finset.Icc_sSubset_Icc_right

added theorem Finset.Icc_ssubset_Icc_left

added theorem Finset.Icc_ssubset_Icc_right

Modified Mathlib/Data/List/Basic.lean

modified theorem List.getLast?_cons_cons

modified theorem List.getLast?_singleton

Modified Mathlib/Data/Set/Finite.lean

deleted theorem Set.Finite.sSubset_toFinset

added theorem Set.Finite.ssubset_toFinset

deleted theorem Set.Finite.supᵢ_binfi_of_antitone

deleted theorem Set.Finite.supᵢ_binfi_of_monotone

added theorem Set.Finite.supᵢ_binfᵢ_of_antitone

added theorem Set.Finite.supᵢ_binfᵢ_of_monotone

deleted theorem Set.Finite.toFinset_sSubset

added theorem Set.Finite.toFinset_ssubset

Modified Mathlib/Deprecated/Subgroup.lean

Modified Mathlib/Deprecated/Submonoid.lean

added theorem Additive.isAddSubmonoid_iff

deleted theorem Additive.is_add_submonoid_iff

deleted theorem IsSubmonoid.Inter

added theorem IsSubmonoid.interᵢ

deleted theorem Monoid.closure.IsSubmonoid

added theorem Monoid.closure.isSubmonoid

added theorem Range.isSubmonoid

deleted theorem Range.is_submonoid

added theorem Submonoid.isSubmonoid

deleted theorem Submonoid.is_submonoid

deleted theorem Univ.IsSubmonoid

added theorem Univ.isSubmonoid

added theorem isSubmonoid_unionᵢ_of_directed

deleted theorem is_submonoid_Union_of_directed

added theorem powers.isSubmonoid

deleted theorem powers.is_submonoid

Modified Mathlib/GroupTheory/Abelianization.lean

modified def Abelianization.lift

modified def MulEquiv.abelianizationCongr

added theorem rank_closureCommutatorRepresentatives_le

deleted theorem rank_closure_commutator_representations_le

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem Submonoid.coe_equivMapOfInjective_apply

deleted theorem Submonoid.coe_equiv_map_of_injective_apply

modified def Submonoid.subtype

added theorem Submonoid.topEquiv_toMonoidHom

deleted theorem Submonoid.top_equiv_toMonoidHom

modified def SubmonoidClass.Subtype

Modified Mathlib/Order/Copy.lean

modified def BoundedOrder.copy

modified def CompleteDistribLattice.copy

modified def CompleteLattice.copy

modified def ConditionallyCompleteLattice.copy

modified def DistribLattice.copy

modified def Lattice.copy

Modified Mathlib/Order/Ideal.lean

deleted theorem Order.Ideal.coe_sSubset_coe

added theorem Order.Ideal.coe_ssubset_coe

Modified Mathlib/RingTheory/Subring/Basic.lean

modified theorem AddSubgroup.int_mul_mem

added theorem Subring.coe_intCast

deleted theorem Subring.coe_int_cast

added theorem Subring.coe_natCast

deleted theorem Subring.coe_nat_cast

Modified Mathlib/Tactic/FieldSimp.lean

Modified Mathlib/Topology/Sets/Closeds.lean

Modified Mathlib/Topology/Sets/Opens.lean