Commit 2024-07-26 02:02 19a1471c

View on Github →

chore: robustifying for debug.byAsSorry (part 5) (#15126)

Estimated changes

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

modified theorem CauSeq.Completion.inv_mk

Modified Mathlib/CategoryTheory/Filtered/Basic.lean

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

modified theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hom_ext

modified theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hom_ext

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

modified theorem CategoryTheory.hasFiniteCoproducts_of_has_binary_and_initial

modified theorem CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal

Modified Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

modified def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit

modified def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

Modified Mathlib/Computability/Reduce.lean

Modified Mathlib/Data/Set/Finite.lean

Modified Mathlib/GroupTheory/Subgroup/Center.lean

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

modified theorem IsRelPrime.add_mul_left_left

Modified Mathlib/Tactic/NormNum/OfScientific.lean