Commit 2024-07-28 23:33 04e23488

View on Github →

chore: robustifying for debug.byAsSorry (part 13) (#15197)

Estimated changes

Modified Mathlib/Algebra/Homology/CommSq.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

modified theorem CategoryTheory.GradedObject.hasMap_of_iso

Modified Mathlib/CategoryTheory/Limits/EpiMono.lean

modified theorem CategoryTheory.epi_iff_inl_eq_inr

modified theorem CategoryTheory.epi_iff_isIso_inl

modified theorem CategoryTheory.epi_iff_isIso_inr

modified theorem CategoryTheory.mono_iff_fst_eq_snd

modified theorem CategoryTheory.mono_iff_isIso_fst

modified theorem CategoryTheory.mono_iff_isIso_snd

Modified Mathlib/CategoryTheory/Quotient/Linear.lean

modified def CategoryTheory.Quotient.Linear.module'

modified def CategoryTheory.Quotient.Linear.module

modified def CategoryTheory.Quotient.Linear.smul

modified theorem CategoryTheory.Quotient.Linear.smul_eq

modified def CategoryTheory.Quotient.linear

Modified Mathlib/CategoryTheory/Quotient/Preadditive.lean

modified def CategoryTheory.Quotient.Preadditive.add

modified def CategoryTheory.Quotient.Preadditive.neg

modified theorem CategoryTheory.Quotient.functor_additive

modified def CategoryTheory.Quotient.preadditive

Modified Mathlib/Combinatorics/Young/YoungDiagram.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

modified theorem Cardinal.mk_embedding_eq_arrow_of_le

modified theorem Cardinal.mk_embedding_eq_arrow_of_lift_le

modified theorem Cardinal.mk_equiv_eq_arrow_of_eq

modified theorem Cardinal.mk_equiv_eq_arrow_of_lift_eq

modified theorem Cardinal.mk_equiv_of_eq

modified theorem Cardinal.mk_equiv_of_lift_eq

modified theorem Cardinal.mk_surjective_eq_arrow_of_le

modified theorem Cardinal.mk_surjective_eq_arrow_of_lift_le

Modified Mathlib/SetTheory/Surreal/Multiplication.lean

modified theorem Surreal.Multiplication.P1_of_ih

modified theorem Surreal.Multiplication.ih1

modified theorem Surreal.Multiplication.ih1_swap

modified theorem Surreal.Multiplication.ih4

modified theorem Surreal.Multiplication.ih₁₂

modified theorem Surreal.Multiplication.ih₂₁

modified theorem Surreal.Multiplication.mulOption_lt

modified theorem Surreal.Multiplication.mulOption_lt_of_lt

modified theorem Surreal.Multiplication.numeric_mul_option

modified theorem Surreal.Multiplication.numeric_of_ih

modified theorem Surreal.Multiplication.numeric_option_mul

modified theorem Surreal.Multiplication.numeric_option_mul_option

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

modified theorem Subgroup.isOpen_mono

modified theorem Subgroup.isOpen_of_mem_nhds

modified theorem Subgroup.isOpen_of_one_mem_interior

modified theorem Subgroup.isOpen_of_openSubgroup

Modified Mathlib/Topology/Algebra/UniformField.lean