Commit 2024-07-27 08:25 e4a1af96

View on Github →

chore: robustifying for debug.byAsSorry (part 10) (#15164)

Estimated changes

Modified Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

modified theorem Subalgebra.iSupLift_comp_inclusion

modified theorem Subalgebra.iSupLift_inclusion

modified theorem Subalgebra.iSupLift_mk

modified theorem Subalgebra.iSupLift_of_mem

Modified Mathlib/Algebra/Polynomial/Basic.lean

modified theorem Polynomial.X_ne_zero

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Data/DFinsupp/WellFounded.lean

modified theorem DFinsupp.Lex.acc

modified theorem DFinsupp.Lex.acc_of_single

modified theorem DFinsupp.Lex.acc_single

modified theorem DFinsupp.Lex.acc_zero

modified theorem DFinsupp.Lex.wellFounded'

modified theorem DFinsupp.Lex.wellFounded

Modified Mathlib/Data/Set/UnionLift.lean

Modified Mathlib/Order/Interval/Set/Pi.lean

modified theorem Set.pi_univ_Ico_subset

modified theorem Set.pi_univ_Iio_subset

modified theorem Set.pi_univ_Ioc_subset

modified theorem Set.pi_univ_Ioi_subset

modified theorem Set.pi_univ_Ioo_subset

Modified Mathlib/RingTheory/Ideal/Quotient.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

modified theorem IsLocalization.map_units_map_submonoid

Modified Mathlib/RingTheory/Valuation/Integers.lean

modified theorem Valuation.Integers.dvd_iff_le

modified theorem Valuation.Integers.dvd_of_le

modified theorem Valuation.Integers.eq_algebraMap_or_inv_eq_algebraMap

modified theorem Valuation.Integers.isUnit_of_one'

modified theorem Valuation.Integers.isUnit_of_one

modified theorem Valuation.Integers.le_iff_dvd

modified theorem Valuation.Integers.le_of_dvd

modified theorem Valuation.Integers.one_of_isUnit

Modified Mathlib/Topology/Order/Basic.lean

modified theorem Dense.topology_eq_generateFrom

modified theorem Filter.Eventually.exists_Ioo_subset

modified theorem IsOpen.exists_Ioo_subset

modified theorem SecondCountableTopology.of_separableSpace_orderTopology

modified theorem Set.PairwiseDisjoint.countable_of_Ioo

modified theorem countable_image_gt_image_Iio

modified theorem countable_image_gt_image_Ioi

modified theorem countable_image_lt_image_Iio

modified theorem countable_image_lt_image_Ioi

modified theorem countable_of_isolated_left'

modified theorem countable_setOf_covBy_left

modified theorem countable_setOf_covBy_right

modified theorem dense_iff_exists_between

modified theorem dense_of_exists_between

modified theorem exists_Icc_mem_subset_of_mem_nhds

modified theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici

modified theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic

modified theorem exists_Ico_subset_of_mem_nhds'

modified theorem exists_Ico_subset_of_mem_nhds

modified theorem exists_Ioc_subset_of_mem_nhds'

modified theorem exists_Ioc_subset_of_mem_nhds

modified theorem ge_mem_nhds

modified theorem gt_mem_nhds

modified theorem isOpen_gt'

modified theorem isOpen_iff_generate_intervals

modified theorem isOpen_lt'

modified theorem le_mem_nhds

modified theorem lt_mem_nhds

modified theorem mem_nhds_iff_exists_Ioo_subset'

modified theorem mem_nhds_iff_exists_Ioo_subset

modified theorem nhds_basis_Ioo'

modified theorem nhds_basis_Ioo

modified theorem nhds_eq_order

modified theorem nhds_order_unbounded

modified theorem order_separated

modified theorem pi_Iio_mem_nhds

modified theorem tendsto_of_tendsto_of_tendsto_of_le_of_le'

modified theorem tendsto_of_tendsto_of_tendsto_of_le_of_le

modified theorem tendsto_order

modified theorem tendsto_order_unbounded