Commit 2024-07-25 10:38 ca397b72

View on Github →

chore: robustifying for debug.byAsSorry (part 3) (#15120) cf #14993 and #15119

Estimated changes

Modified Mathlib/Algebra/Associated/Basic.lean

Modified Mathlib/Algebra/Field/Basic.lean

Modified Mathlib/Algebra/Field/Opposite.lean

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

modified def Submonoid.gciMapComap

Modified Mathlib/Algebra/Order/Group/OrderIso.lean

Modified Mathlib/Algebra/Order/Hom/Monoid.lean

modified theorem monotone_iff_map_nonneg

modified theorem strictMono_iff_map_pos

Modified Mathlib/CategoryTheory/Category/GaloisConnection.lean

Modified Mathlib/CategoryTheory/ComposableArrows.lean

modified def CategoryTheory.ComposableArrows.homMkSucc

Modified Mathlib/CategoryTheory/Core.lean

Modified Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

modified theorem CategoryTheory.IsHomLift.codomain_eq

modified theorem CategoryTheory.IsHomLift.domain_eq

Modified Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean

modified def CategoryTheory.CommSq.leftAdjointLiftStructEquiv

modified theorem CategoryTheory.CommSq.left_adjoint

modified theorem CategoryTheory.CommSq.right_adjoint

Modified Mathlib/Control/LawfulFix.lean

modified theorem Part.fix_eq

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Deprecated/Group.lean

Modified Mathlib/Order/Irreducible.lean