Commit 2023-02-18 21:13 6fff7165

View on Github →

chore: tidy various files (#2321)

Estimated changes

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/CategoryTheory/Category/Preorder.lean

modified def CategoryTheory.Equivalence.toOrderIso

added theorem CategoryTheory.homOfLE_comp

added theorem CategoryTheory.homOfLE_leOfHom

added theorem CategoryTheory.homOfLE_refl

deleted theorem CategoryTheory.hom_of_le_comp

deleted theorem CategoryTheory.hom_of_le_le_of_hom

deleted theorem CategoryTheory.hom_of_le_refl

added theorem CategoryTheory.leOfHom_homOfLE

deleted theorem CategoryTheory.le_ofOp_hom

deleted theorem CategoryTheory.le_of_hom_hom_of_le

added theorem CategoryTheory.le_of_op_hom

modified def Monotone.functor

Modified Mathlib/CategoryTheory/Equivalence.lean

added theorem CategoryTheory.Equivalence.essSurj_of_equivalence

deleted theorem CategoryTheory.Equivalence.ess_surj_of_equivalence

Modified Mathlib/CategoryTheory/Pi/Basic.lean

modified def CategoryTheory.Functor.pi'

modified def CategoryTheory.Functor.pi

modified theorem CategoryTheory.Functor.pi_ext

modified def CategoryTheory.NatTrans.pi

modified def CategoryTheory.Pi.comap

modified def CategoryTheory.Pi.comapComp

modified def CategoryTheory.Pi.comapId

modified def CategoryTheory.Pi.sum

Modified Mathlib/Combinatorics/Pigeonhole.lean

Modified Mathlib/Data/Analysis/Filter.lean

Modified Mathlib/Data/Dfinsupp/Lex.lean

Modified Mathlib/GroupTheory/Finiteness.lean

deleted theorem Group.FgIffMonoid.fg

added theorem Group.fg_iff_monoid_fg

Modified Mathlib/GroupTheory/Submonoid/Inverses.lean

added theorem Submonoid.leftInv_le_isUnit

deleted theorem Submonoid.leftInv_le_is_unit

Modified Mathlib/Topology/Order.lean