Commit 2024-07-27 07:35 319e0a1a

View on Github →

chore: robustifying for debug.byAsSorry (part 8) (#15149) See zulip.

Estimated changes

Modified Mathlib/Algebra/IsPrimePow.lean

Modified Mathlib/Algebra/Module/Submodule/Map.lean

modified def Submodule.comap

modified def Submodule.gciMapComap

modified def Submodule.giMapComap

Modified Mathlib/Algebra/Order/CauSeq/BigOperators.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

Modified Mathlib/CategoryTheory/GuitartExact/Basic.lean

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

modified theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux

Modified Mathlib/CategoryTheory/Limits/Types.lean

modified theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map

Modified Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

modified theorem CategoryTheory.LocalizerMorphism.isEquivalence_imp

Modified Mathlib/CategoryTheory/Localization/Prod.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

modified theorem CategoryTheory.Presieve.Arrows.Compatible.exists_familyOfElements

Modified Mathlib/Combinatorics/Enumerative/Composition.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

modified theorem Rel.edgeDensity_comm

modified theorem Rel.swap_mem_interedges_iff

Modified Mathlib/Data/Real/ConjExponents.lean

modified theorem NNReal.IsConjExponent.conj_eq

modified theorem Real.IsConjExponent.conj_eq

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

Modified Mathlib/Order/Filter/Basic.lean

modified theorem Filter.comap_comm

modified theorem Filter.map_comm

Modified Mathlib/RingTheory/OreLocalization/Ring.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean