-
-
Save fpvandoorn/05cca028139e98bded9874169a1332d5 to your computer and use it in GitHub Desktop.
output of new linter
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /- The `illegalClassical` linter reports: | |
| FOUND PROPDECIDABLE IN THEOREM STATEMENTS. -/ | |
| -- Mathlib.Algebra.BigOperators.Finprod | |
| Error: ./././Mathlib/Algebra/BigOperators/Finprod.lean:94:1: error: finsum_def'.{u_8, u_7} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/BigOperators/Finprod.lean:100:1: error: finprod_def'.{u_8, u_7} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.DirectLimit | |
| Error: ./././Mathlib/Algebra/DirectLimit.lean:294:1: error: Module.DirectLimit.toModule_totalize_of_le.{u, v, w} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/DirectLimit.lean:306:1: error: Module.DirectLimit.of.zero_exact_aux.{u, v, w} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/DirectLimit.lean:678:1: error: Ring.DirectLimit.of.zero_exact_aux2.{v, w} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/DirectLimit.lean:708:1: error: Ring.DirectLimit.of.zero_exact_aux.{v, w} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.GCDMonoid.Div | |
| Error: ./././Mathlib/Algebra/GCDMonoid/Div.lean:81:1: error: Finset.Polynomial.gcd_div_eq_one.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/GCDMonoid/Div.lean:89:1: error: Finset.Polynomial.gcd_div_id_eq_one.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.Homology.DifferentialObject | |
| Error: ./././Mathlib/Algebra/Homology/DifferentialObject.lean:88:3: error: HomologicalComplex.dgoToHomologicalComplex_obj_d.{u_2, u_1, u_3} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/Homology/DifferentialObject.lean:88:3: error: HomologicalComplex.dgoToHomologicalComplex_map_f.{u_2, u_1, u_3} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.Homology.Homotopy | |
| Error: ./././Mathlib/Algebra/Homology/Homotopy.lean:358:3: error: Homotopy.nullHomotopy'_hom.{u_1, v, u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.Module.DedekindDomain | |
| Error: ./././Mathlib/Algebra/Module/DedekindDomain.lean:39:1: error: Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Algebra/Module/DedekindDomain.lean:67:1: error: Submodule.isInternal_prime_power_torsion.{u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.Module.PID | |
| Error: ./././Mathlib/Algebra/Module/PID.lean:79:1: error: Submodule.isInternal_prime_power_torsion_of_pid.{u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Algebra.MonoidAlgebra.Degree | |
| Error: ./././Mathlib/Algebra/MonoidAlgebra/Degree.lean:258:1: error: AddMonoidAlgebra.supDegree_single.{u_5, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.AlgebraicTopology.TopologicalSimplex | |
| Error: ./././Mathlib/AlgebraicTopology/TopologicalSimplex.lean:59:1: error: SimplexCategory.coe_toTopMap theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.BoxIntegral.Basic | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Basic.lean:109:1: error: BoxIntegral.integralSum_fiberwise.{u_1, u, v, w} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.BoxIntegral.Partition.Basic | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:200:1: error: BoxIntegral.Prepartition.card_filter_mem_Icc_le.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:293:3: error: BoxIntegral.Prepartition.biUnion_boxes.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:347:1: error: BoxIntegral.Prepartition.sum_biUnion_boxes.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:591:3: error: BoxIntegral.Prepartition.filter_boxes.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:630:1: error: BoxIntegral.Prepartition.sum_fiberwise.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:637:3: error: BoxIntegral.Prepartition.disjUnion_boxes.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Basic.lean:660:1: error: BoxIntegral.Prepartition.sum_disj_union_boxes.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.BoxIntegral.Partition.Split | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Split.lean:253:1: error: BoxIntegral.Prepartition.splitMany_insert.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Split.lean:284:1: error: BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean:235:1: error: BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.BoxIntegral.Partition.Tagged | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean:102:3: error: BoxIntegral.TaggedPrepartition.filter_boxes_val.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean:354:1: error: BoxIntegral.TaggedPrepartition.disjUnion_boxes.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.Calculus.ContDiff.Basic | |
| Error: ./././Mathlib/Analysis/Calculus/ContDiff/Basic.lean:1233:1: error: contDiff_update.{u_5, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/Calculus/ContDiff/Basic.lean:1243:1: error: contDiff_single.{u_5, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.Calculus.FDeriv.Basic | |
| Error: ./././Mathlib/Analysis/Calculus/FDeriv/Basic.lean:180:1: error: fderivWithin_def.{u_8, u_7, u_6} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/Calculus/FDeriv/Basic.lean:188:1: error: fderiv_def.{u_8, u_7, u_6} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.Convex.Combination | |
| Error: ./././Mathlib/Analysis/Convex/Combination.lean:53:1: error: Finset.centerMass_pair.{u_5, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/Convex/Combination.lean:60:1: error: Finset.centerMass_insert.{u_5, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/Convex/Combination.lean:114:1: error: Finset.centerMass_ite_eq.{u_5, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/Convex/Combination.lean:502:1: error: convexHull_basis_eq_stdSimplex.{u_5, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/Convex/Combination.lean:591:1: error: AffineIndependent.convexHull_inter'.{u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.Convex.Independent | |
| Error: ./././Mathlib/Analysis/Convex/Independent.lean:175:1: error: convexIndependent_iff_finset.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.Fourier.AddCircle | |
| Error: ./././Mathlib/Analysis/Fourier/AddCircle.lean:443:1: error: coe_fourierBasis theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.InnerProductSpace.Orientation | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/Orientation.lean:178:1: error: Orientation.volumeForm_def.{u_2} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Analysis.InnerProductSpace.l2Space | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:168:1: error: lp.inner_single_left.{u_4, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:178:1: error: lp.inner_single_right.{u_4, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:230:11: error: OrthogonalFamily.linearIsometry_apply_single.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:241:11: error: OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:341:11: error: IsHilbertSum.linearIsometryEquiv_symm_apply_single.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:350:11: error: IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:360:11: error: IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:419:11: error: HilbertBasis.repr_symm_single.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:424:11: error: HilbertBasis.repr_self.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:429:11: error: HilbertBasis.repr_apply_apply.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:436:11: error: HilbertBasis.orthonormal.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:444:11: error: HilbertBasis.hasSum_repr_symm.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:462:11: error: HilbertBasis.hasSum_repr.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:467:11: error: HilbertBasis.dense_span.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:481:11: error: HilbertBasis.hasSum_inner_mul_inner.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:488:11: error: HilbertBasis.summable_inner_mul_inner.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:493:11: error: HilbertBasis.tsum_inner_mul_inner.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:511:1: error: HilbertBasis.coe_toOrthonormalBasis.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:516:11: error: HilbertBasis.hasSum_orthogonalProjection.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:523:1: error: HilbertBasis.finite_spans_dense.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:539:1: error: Orthonormal.linearIsometryEquiv_symm_apply_single_one.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:546:11: error: HilbertBasis.coe_mk.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:559:11: error: HilbertBasis.coe_mkOfOrthogonalEqBot.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:575:1: error: OrthonormalBasis.coe_toHilbertBasis.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:581:1: error: Orthonormal.exists_hilbertBasis_extension.{u_3, u_2} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Analysis/InnerProductSpace/l2Space.lean:594:1: error: exists_hilbertBasis.{u_3, u_2} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.CategoryTheory.Category.PartialFun | |
| Error: ./././Mathlib/CategoryTheory/Category/PartialFun.lean:117:3: error: partialFunToPointed_map.{u_3} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Category/PartialFun.lean:133:3: error: partialFunEquivPointed_counitIso_inv_app_toFun.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Category/PartialFun.lean:133:3: error: partialFunEquivPointed_unitIso_inv_app.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Category/PartialFun.lean:133:3: error: partialFunEquivPointed_functor_map_toFun.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Category/PartialFun.lean:133:3: error: partialFunEquivPointed_unitIso_hom_app.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.CategoryTheory.Limits.Shapes.Biproducts | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:74:11: error: CategoryTheory.Limits.Bicone.mk.{w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:74:1: error: CategoryTheory.Limits.Bicone.rec.{u, w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:78:3: error: CategoryTheory.Limits.Bicone.ι_π.{w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:145:3: error: CategoryTheory.Limits.Bicones.functoriality_map_hom.{w, uC', uC, uD', uD} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:220:3: error: CategoryTheory.Limits.Bicone.ofLimitCone_ι.{w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:228:1: error: CategoryTheory.Limits.Bicone.ι_of_isLimit.{w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:236:3: error: CategoryTheory.Limits.Bicone.ofColimitCocone_π.{w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:245:1: error: CategoryTheory.Limits.Bicone.π_of_isColimit.{w, uC', uC} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:850:1: error: CategoryTheory.Limits.biproduct.isLimitFromSubtype.{w, v, u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean:877:1: error: CategoryTheory.Limits.biproduct.isColimitToSubtype.{w, v, u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.CategoryTheory.Preadditive.HomOrthogonal | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean:74:3: error: CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply.{u_1, v, u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean:116:3: error: CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply.{u_1, v, u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean:129:1: error: CategoryTheory.HomOrthogonal.matrixDecomposition_id.{u_1, v, u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean:145:1: error: CategoryTheory.HomOrthogonal.matrixDecomposition_comp.{u_1, v, u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.CategoryTheory.Preadditive.Mat | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Mat.lean:124:1: error: CategoryTheory.Mat_.id_def.{v₁, u₁} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Mat.lean:130:1: error: CategoryTheory.Mat_.id_apply.{v₁, u₁} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Mat.lean:334:3: error: CategoryTheory.Mat_.isoBiproductEmbedding_inv.{v₁, u₁} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Mat.lean:334:3: error: CategoryTheory.Mat_.isoBiproductEmbedding_hom.{v₁, u₁} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Mat.lean:580:1: error: CategoryTheory.Mat.id_def.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Mat.lean:585:1: error: CategoryTheory.Mat.id_apply.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.CategoryTheory.Preadditive.Schur | |
| Error: ./././Mathlib/CategoryTheory/Preadditive/Schur.lean:212:1: error: CategoryTheory.finrank_hom_simple_simple.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:60:15: error: SzemerediRegularity.chunk.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:70:15: error: SzemerediRegularity.star.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:81:1: error: SzemerediRegularity.biUnion_star_subset_nonuniformWitness.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:88:1: error: SzemerediRegularity.star_subset_chunk.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:180:1: error: SzemerediRegularity.card_chunk.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:188:1: error: SzemerediRegularity.card_eq_of_mem_parts_chunk.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:194:1: error: SzemerediRegularity.m_le_card_of_mem_chunk_parts.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:198:1: error: SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:202:1: error: SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:475:1: error: SzemerediRegularity.edgeDensity_chunk_not_uniform.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:527:1: error: SzemerediRegularity.edgeDensity_chunk_uniform.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean:56:15: error: SzemerediRegularity.increment.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean:65:1: error: SzemerediRegularity.card_increment.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean:80:1: error: SzemerediRegularity.increment_isEquipartition.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean:123:1: error: SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean:140:1: error: SzemerediRegularity.energy_increment.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean:75:1: error: szemeredi_regularity.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean:48:1: error: SimpleGraph.farFromTriangleFree_iff.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean:53:1: error: SimpleGraph.farFromTriangleFree.le_card_sub_card.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean:60:1: error: SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty'.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean:84:1: error: SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Computability.TuringMachine | |
| Error: ./././Mathlib/Computability/TuringMachine.lean:2544:1: error: Turing.TM2to1.trStmts₁_run.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Control.Fix | |
| Error: ./././Mathlib/Control/Fix.lean:74:11: error: Part.fix_def.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Finite.Card | |
| Error: ./././Mathlib/Data/Finite/Card.lean:49:1: error: Nat.card_eq.{u_4} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Finset.Functor | |
| Error: ./././Mathlib/Data/Finset/Functor.lean:208:1: error: Finset.map_comp_coe.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finset/Functor.lean:213:1: error: Finset.map_traverse.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Finsupp.Interval | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:79:1: error: Finsupp.rangeIcc_support.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:103:1: error: Finsupp.Icc_eq.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:107:1: error: Finsupp.card_Icc.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:112:1: error: Finsupp.card_Ico.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:117:1: error: Finsupp.card_Ioc.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:122:1: error: Finsupp.card_Ioo.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Finsupp/Interval.lean:132:1: error: Finsupp.card_uIcc.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Nat.Lattice | |
| Error: ./././Mathlib/Data/Nat/Lattice.lean:33:1: error: Nat.sInf_def theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/Nat/Lattice.lean:37:1: error: Nat.sSup_def theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Nat.PartENat | |
| Error: ./././Mathlib/Data/Nat/PartENat.lean:710:1: error: PartENat.toWithTop_add theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.PFunctor.Univariate.M | |
| Error: ./././Mathlib/Data/PFunctor/Univariate/M.lean:628:1: error: PFunctor.M.ext.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Data/PFunctor/Univariate/M.lean:663:1: error: PFunctor.M.nth_of_bisim.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Real.Archimedean | |
| Error: ./././Mathlib/Data/Real/Archimedean.lean:112:1: error: Real.sSup_def theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Data.Set.BoolIndicator | |
| Error: ./././Mathlib/Data/Set/BoolIndicator.lean:47:1: error: Set.preimage_boolIndicator_eq_union.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.FieldTheory.Finite.Polynomial | |
| Error: ./././Mathlib/FieldTheory/Finite/Polynomial.lean:204:1: error: MvPolynomial.rank_R.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/Finite/Polynomial.lean:231:1: error: MvPolynomial.finrank_R.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.FieldTheory.RatFunc | |
| Error: ./././Mathlib/FieldTheory/RatFunc.lean:1122:1: error: RatFunc.numDenom_div.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/RatFunc.lean:1148:1: error: RatFunc.num_div.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/RatFunc.lean:1173:1: error: RatFunc.num_div_dvd'.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/RatFunc.lean:1184:1: error: RatFunc.denom_div.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.FieldTheory.Separable | |
| Error: ./././Mathlib/FieldTheory/Separable.lean:101:1: error: Polynomial.separable_gcd_left.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/Separable.lean:106:1: error: Polynomial.separable_gcd_right.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/Separable.lean:188:1: error: Polynomial.multiplicity_le_one_of_separable.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/Separable.lean:302:1: error: Polynomial.count_roots_le_one.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.FieldTheory.SeparableDegree | |
| Error: ./././Mathlib/FieldTheory/SeparableDegree.lean:333:1: error: Polynomial.natSepDegree_eq_of_splits.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/FieldTheory/SeparableDegree.lean:342:1: error: Polynomial.natSepDegree_eq_of_isAlgClosed.{u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Geometry.Manifold.PartitionOfUnity | |
| Error: ./././Mathlib/Geometry/Manifold/PartitionOfUnity.lean:517:1: error: SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod.{uι, uE, uH, uM} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Geometry/Manifold/PartitionOfUnity.lean:524:1: error: SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq.{uι, uE, uH, uM} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.GroupTheory.Exponent | |
| Error: ./././Mathlib/GroupTheory/Exponent.lean:486:3: error: AddMonoid.exponent_eq_iSup_addOrderOf'.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Exponent.lean:487:1: error: Monoid.exponent_eq_iSup_orderOf'.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.GroupTheory.FreeAbelianGroupFinsupp | |
| Error: ./././Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean:193:1: error: FreeAbelianGroup.support_add.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.GroupTheory.Nilpotent | |
| Error: ./././Mathlib/GroupTheory/Nilpotent.lean:385:1: error: least_ascending_central_series_length_eq_nilpotencyClass.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Nilpotent.lean:398:1: error: least_descending_central_series_length_eq_nilpotencyClass.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Nilpotent.lean:416:1: error: lowerCentralSeries_length_eq_nilpotencyClass.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.GroupTheory.SchurZassenhaus | |
| Error: ./././Mathlib/GroupTheory/SchurZassenhaus.lean:249:1: error: Subgroup.SchurZassenhausInduction.step7.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/SchurZassenhaus.lean:276:1: error: Subgroup.exists_right_complement'_of_coprime_of_fintype.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/SchurZassenhaus.lean:307:1: error: Subgroup.exists_left_complement'_of_coprime_of_fintype.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.GroupTheory.Sylow | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:498:1: error: QuotientGroup.card_preimage_mk.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:543:1: error: Sylow.card_quotient_normalizer_modEq_card_quotient.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:553:1: error: Sylow.card_normalizer_modEq_card.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:564:1: error: Sylow.prime_dvd_card_quotient_normalizer.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:581:1: error: Sylow.prime_pow_dvd_card_normalizer.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:590:1: error: Sylow.exists_subgroup_card_pow_succ.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:631:1: error: Sylow.exists_subgroup_card_pow_prime_le.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:651:1: error: Sylow.exists_subgroup_card_pow_prime.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:690:1: error: Sylow.pow_dvd_card_of_pow_dvd_card.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:697:1: error: Sylow.dvd_card_of_dvd_card.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:705:1: error: Sylow.card_coprime_index.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/GroupTheory/Sylow.lean:720:1: error: Sylow.card_eq_multiplicity.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.LinearAlgebra.Determinant | |
| Error: ./././Mathlib/LinearAlgebra/Determinant.lean:174:1: error: LinearMap.det_def.{u_8, u_7} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/LinearAlgebra/Determinant.lean:184:1: error: LinearMap.coe_det.{u_5, u_2} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.LinearAlgebra.Trace | |
| Error: ./././Mathlib/LinearAlgebra/Trace.lean:88:1: error: LinearMap.trace_eq_matrix_trace_of_finset.{u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Logic.Basic | |
| Error: ./././Mathlib/Logic/Basic.lean:1292:1: error: beq_eq_decide.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Decomposition.Lebesgue | |
| Error: ./././Mathlib/MeasureTheory/Decomposition/Lebesgue.lean:71:1: error: MeasureTheory.Measure.singularPart_def.{u_3} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Decomposition/Lebesgue.lean:78:1: error: MeasureTheory.Measure.rnDeriv_def.{u_3} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic | |
| Error: ./././Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean:87:1: error: MeasureTheory.condexp_def.{u_6, u_5} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean:113:1: error: MeasureTheory.condexp_of_sigmaFinite.{u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Function.SimpleFunc | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:228:1: error: MeasureTheory.SimpleFunc.coe_piecewise.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:233:1: error: MeasureTheory.SimpleFunc.piecewise_apply.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:264:1: error: MeasureTheory.SimpleFunc.range_indicator.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:320:1: error: MeasureTheory.SimpleFunc.map_preimage.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:327:1: error: MeasureTheory.SimpleFunc.map_preimage_singleton.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:826:1: error: MeasureTheory.SimpleFunc.approx_apply.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFunc.lean:1155:1: error: MeasureTheory.SimpleFunc.support_eq.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Function.SimpleFuncDense | |
| Error: ./././Mathlib/MeasureTheory/Function/SimpleFuncDense.lean:87:1: error: MeasureTheory.SimpleFunc.nearestPtInd_succ.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Integral.Bochner | |
| Error: ./././Mathlib/MeasureTheory/Integral/Bochner.lean:790:1: error: MeasureTheory.integral_def.{u_7, u_6} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Integral.SetToL1 | |
| Error: ./././Mathlib/MeasureTheory/Integral/SetToL1.lean:307:1: error: MeasureTheory.SimpleFunc.setToSimpleFunc_eq_sum_filter.{u_4, u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.MeasurableSpace.Defs | |
| Error: ./././Mathlib/MeasureTheory/MeasurableSpace/Defs.lean:231:1: error: MeasurableSet.ite'.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Measure.MeasureSpace | |
| Error: ./././Mathlib/MeasureTheory/Measure/MeasureSpace.lean:646:1: error: MeasureTheory.measure_if.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Measure/MeasureSpace.lean:1170:1: error: MeasureTheory.Measure.map_def.{u_9, u_8} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Measure.MeasureSpaceDef | |
| Error: ./././Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean:615:1: error: MeasureTheory.toMeasurable_def.{u_6} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.MeasureTheory.Measure.VectorMeasure | |
| Error: ./././Mathlib/MeasureTheory/Measure/VectorMeasure.lean:409:3: error: MeasureTheory.Measure.toSignedMeasure_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Measure/VectorMeasure.lean:468:3: error: MeasureTheory.Measure.toENNRealVectorMeasure_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/MeasureTheory/Measure/VectorMeasure.lean:1257:3: error: MeasureTheory.VectorMeasure.trim_apply.{u_4, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.KummerDedekind | |
| Error: ./././Mathlib/NumberTheory/KummerDedekind.lean:251:15: error: KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/KummerDedekind.lean:277:1: error: KummerDedekind.multiplicity_factors_map_eq_multiplicity.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/KummerDedekind.lean:289:1: error: KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.LegendreSymbol.MulCharacter | |
| Error: ./././Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean:106:3: error: MulChar.trivial_apply.{u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.NumberField.CanonicalEmbedding | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:283:1: error: NumberField.mixedEmbedding.fundamentalDomain_stdBasis.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:290:1: error: NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:341:1: error: NumberField.mixedEmbedding.det_matrixToStdBasis.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:356:1: error: NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:551:1: error: NumberField.mixedEmbedding.instIsAddHaarMeasureProdForAllSubtypeInfinitePlaceIsRealRealForAllIsComplexComplexInstAddGroupAddGroupInstAddGroupRealToAddGroupToNormedAddGroupInstNormedAddCommGroupComplexInstTopologicalSpaceProdTopologicalSpaceToTopologicalSpaceToUniformSpacePseudoMetricSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToMeasurableSpaceMeasureSpacePiFintypePropDecidableFintypeMeasureSpaceMeasureSpaceOfInnerProductSpaceComplexToRealInnerProductSpaceInstIsROrCComplexInstFiniteDimensionalRealComplexInstDivisionRingRealAddCommGroupInstModuleToSemiringToDivisionSemiringToModuleMeasurableSpaceBorelSpaceVolume.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:553:1: error: NumberField.mixedEmbedding.instNoAtomsProdForAllSubtypeInfinitePlaceIsRealRealForAllIsComplexComplexToMeasurableSpaceMeasureSpacePiFintypePropDecidableFintypeMeasureSpaceMeasureSpaceOfInnerProductSpaceInstNormedAddCommGroupComplexComplexToRealInnerProductSpaceInstIsROrCComplexInstFiniteDimensionalRealComplexInstDivisionRingRealAddCommGroupInstModuleToSemiringToDivisionSemiringToModuleMeasurableSpaceBorelSpaceVolume.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:573:1: error: NumberField.mixedEmbedding.convexBodyLT_volume.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:686:1: error: NumberField.mixedEmbedding.convexBodyLT'_volume.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:789:1: error: NumberField.mixedEmbedding.norm_le_convexBodySumFun.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:818:1: error: NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:873:1: error: NumberField.mixedEmbedding.convexBodySum_volume.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:945:1: error: NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:976:1: error: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:990:1: error: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt'.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:1005:1: error: NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:1012:1: error: NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt'.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:1064:1: error: NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean:1101:1: error: NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.NumberField.Discriminant | |
| Error: ./././Mathlib/NumberTheory/NumberField/Discriminant.lean:71:1: error: NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.NumberField.Embeddings | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:450:1: error: NumberField.InfinitePlace.card_filter_mk_eq.{u_2} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:579:1: error: NumberField.InfinitePlace.card_real_embeddings.{u_2} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:583:1: error: NumberField.InfinitePlace.card_complex_embeddings.{u_2} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:864:1: error: NumberField.InfinitePlace.card_stabilizer.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:929:1: error: NumberField.InfinitePlace.card_isUnramified.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:951:1: error: NumberField.InfinitePlace.card_isUnramified_compl.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Embeddings.lean:972:1: error: NumberField.InfinitePlace.card_eq_card_isUnramifiedIn.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.NumberField.Units | |
| Error: ./././Mathlib/NumberTheory/NumberField/Units.lean:204:1: error: NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Units.lean:240:1: error: NumberField.Units.dirichletUnitTheorem.logEmbedding_component_le.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Units.lean:246:1: error: NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/NumberField/Units.lean:278:1: error: NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.NumberTheory.RamificationInertia | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:74:1: error: Ideal.ramificationIdx_eq_find.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:145:1: error: Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:155:1: error: Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:695:1: error: Ideal.Factors.ne_bot.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:699:1: error: Ideal.Factors.isPrime.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:704:1: error: Ideal.Factors.ramificationIdx_ne_zero.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:710:1: error: Ideal.Factors.fact_ramificationIdx_neZero.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:719:1: error: Ideal.Factors.isScalarTower.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:726:1: error: Ideal.Factors.finrank_pow_ramificationIdx.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:734:1: error: Ideal.Factors.finiteDimensional_quotient.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:743:1: error: Ideal.Factors.inertiaDeg_ne_zero.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:748:1: error: Ideal.Factors.finiteDimensional_quotient_pow.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:760:15: error: Ideal.Factors.piQuotientEquiv.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:775:1: error: Ideal.Factors.piQuotientEquiv_mk.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:780:1: error: Ideal.Factors.piQuotientEquiv_map.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:790:15: error: Ideal.Factors.piQuotientLinearEquiv.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/NumberTheory/RamificationInertia.lean:812:1: error: Ideal.sum_ramification_inertia.{u_2, u_1, u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Order.CompleteLatticeIntervals | |
| Error: ./././Mathlib/Order/CompleteLatticeIntervals.lean:49:1: error: subset_sSup_def.{u_2} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Order/CompleteLatticeIntervals.lean:89:1: error: subset_sInf_def.{u_2} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Order.LiminfLimsup | |
| Error: ./././Mathlib/Order/LiminfLimsup.lean:1399:1: error: Filter.HasBasis.liminf_eq_ite.{u_5, u_4, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Order/LiminfLimsup.lean:1444:1: error: Filter.HasBasis.limsup_eq_ite.{u_5, u_4, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Probability.Distributions.Uniform | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:207:1: error: MeasureTheory.pdf.uniformPDF_ite.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:242:1: error: PMF.uniformOfFinset_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:271:1: error: PMF.toOuterMeasure_uniformOfFinset_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:290:1: error: PMF.toMeasure_uniformOfFinset_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:327:1: error: PMF.toOuterMeasure_uniformOfFintype_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:333:1: error: PMF.toMeasure_uniformOfFintype_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:368:1: error: PMF.ofMultiset_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:373:1: error: PMF.support_ofMultiset.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:377:1: error: PMF.mem_support_ofMultiset_iff.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:391:1: error: PMF.toOuterMeasure_ofMultiset_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/Distributions/Uniform.lean:400:1: error: PMF.toMeasure_ofMultiset_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Probability.ProbabilityMassFunction.Constructions | |
| Error: ./././Mathlib/Probability/ProbabilityMassFunction/Constructions.lean:51:1: error: PMF.map_apply.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/ProbabilityMassFunction/Constructions.lean:124:1: error: PMF.seq_apply.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Probability.ProbabilityMassFunction.Monad | |
| Error: ./././Mathlib/Probability/ProbabilityMassFunction/Monad.lean:45:1: error: PMF.pure_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/ProbabilityMassFunction/Monad.lean:73:1: error: PMF.toOuterMeasure_pure_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Probability/ProbabilityMassFunction/Monad.lean:86:1: error: PMF.toMeasure_pure_apply.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Probability.Process.Filtration | |
| Error: ./././Mathlib/Probability/Process/Filtration.lean:164:1: error: MeasureTheory.Filtration.sInf_def.{u_3, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RepresentationTheory.Character | |
| Error: ./././Mathlib/RepresentationTheory/Character.lean:117:1: error: FdRep.char_orthonormal.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RepresentationTheory.FdRep | |
| Error: ./././Mathlib/RepresentationTheory/FdRep.lean:129:1: error: FdRep.finrank_hom_simple_simple.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.DedekindDomain.AdicValuation | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/AdicValuation.lean:89:1: error: IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.DedekindDomain.Different | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Different.lean:88:1: error: Submodule.traceDual_top'.{u_3, u_2, u_1, u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.DedekindDomain.Factorization | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Factorization.lean:57:1: error: Associates.finite_factors.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Factorization.lean:88:1: error: Ideal.finite_mulSupport_coe.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Factorization.lean:98:1: error: Ideal.finite_mulSupport_inv.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Factorization.lean:107:1: error: Ideal.finprod_not_dvd.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Factorization.lean:138:1: error: Ideal.finprod_count.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Factorization.lean:170:1: error: Ideal.finprod_heightOneSpectrum_factorization_coe.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.DedekindDomain.Ideal | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:915:1: error: prod_normalizedFactors_eq_self.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:919:1: error: count_le_of_ideal_ge.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:926:1: error: sup_eq_prod_inf_factors.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:955:1: error: irreducible_pow_sup.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:961:1: error: irreducible_pow_sup_of_le.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:969:1: error: irreducible_pow_sup_of_ge.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:1248:1: error: Ideal.count_normalizedFactors_eq.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:1349:15: error: IsDedekindDomain.quotientEquivPiFactors.{u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/DedekindDomain/Ideal.lean:1365:1: error: IsDedekindDomain.quotientEquivPiFactors_mk.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.Fintype | |
| Error: ./././Mathlib/RingTheory/Fintype.lean:17:1: error: card_units_lt.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.HahnSeries.Addition | |
| Error: ./././Mathlib/RingTheory/HahnSeries/Addition.lean:90:3: error: HahnSeries.single.addMonoidHom_apply_coeff.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.HahnSeries.Basic | |
| Error: ./././Mathlib/RingTheory/HahnSeries/Basic.lean:179:1: error: HahnSeries.single_coeff.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.HahnSeries.Multiplication | |
| Error: ./././Mathlib/RingTheory/HahnSeries/Multiplication.lean:49:1: error: HahnSeries.one_coeff.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/HahnSeries/Multiplication.lean:605:3: error: HahnSeries.embDomainAlgHom_apply_coeff.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.HahnSeries.PowerSeries | |
| Error: ./././Mathlib/RingTheory/HahnSeries/PowerSeries.lean:220:3: error: HahnSeries.ofPowerSeriesAlg_apply_coeff.{u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.HahnSeries.Summable | |
| Error: ./././Mathlib/RingTheory/HahnSeries/Summable.lean:78:1: error: HahnSeries.addVal_apply.{u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/HahnSeries/Summable.lean:438:1: error: HahnSeries.SummableFamily.embDomain_apply.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.IntegralClosure | |
| Error: ./././Mathlib/RingTheory/IntegralClosure.lean:175:1: error: Submodule.span_range_natDegree_eq_adjoin.{u_6, u_5} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.LocalProperties | |
| Error: ./././Mathlib/RingTheory/LocalProperties.lean:439:1: error: IsLocalization.smul_mem_finsetIntegerMultiple_span.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/LocalProperties.lean:602:1: error: IsLocalization.exists_smul_mem_of_mem_adjoin.{u} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/LocalProperties.lean:628:1: error: IsLocalization.lift_mem_adjoin_finsetIntegerMultiple.{u} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.Localization.FractionRing | |
| Error: ./././Mathlib/RingTheory/Localization/FractionRing.lean:111:1: error: IsFractionRing.inv_def.{u_7, u_6} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.OreLocalization.Basic | |
| Error: ./././Mathlib/RingTheory/OreLocalization/Basic.lean:905:11: error: OreLocalization.inv_def.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.Perfection | |
| Error: ./././Mathlib/RingTheory/Perfection.lean:533:1: error: PreTilt.coeff_nat_find_add_ne_zero.{u₁, u₂} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.RingTheory.RootsOfUnity.Basic | |
| Error: ./././Mathlib/RingTheory/RootsOfUnity/Basic.lean:881:1: error: IsPrimitiveRoot.card_nthRoots.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/RootsOfUnity/Basic.lean:974:1: error: IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'.{u_4} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/RingTheory/RootsOfUnity/Basic.lean:1003:1: error: IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots.{u_4} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.Algebra.InfiniteSum.Defs | |
| Error: ./././Mathlib/Topology/Algebra/InfiniteSum/Defs.lean:69:1: error: tsum_def.{u_5, u_4} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.Category.Profinite.CofilteredLimit | |
| Error: ./././Mathlib/Topology/Category/Profinite/CofilteredLimit.lean:128:1: error: Profinite.exists_locallyConstant_finite_aux.{u_1, u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.ContinuousFunction.FunctionalCalculus | |
| Error: ./././Mathlib/Topology/ContinuousFunction/FunctionalCalculus.lean:274:1: error: cfc_def.{u_4, u_3} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.Instances.ENNReal | |
| Error: ./././Mathlib/Topology/Instances/ENNReal.lean:1048:1: error: ENNReal.tsum_eq_add_tsum_ite.{u_2} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/Instances/ENNReal.lean:1257:1: error: NNReal.tsum_eq_add_tsum_ite.{u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.LocallyConstant.Basic | |
| Error: ./././Mathlib/Topology/LocallyConstant/Basic.lean:563:3: error: LocallyConstant.indicator_apply_eq_if.{u_5, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/LocallyConstant/Basic.lean:564:1: error: LocallyConstant.mulIndicator_apply_eq_if.{u_5, u_1} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.MetricSpace.PiNat | |
| Error: ./././Mathlib/Topology/MetricSpace/PiNat.lean:67:1: error: PiNat.firstDiff_def.{u_2} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.PartitionOfUnity | |
| Error: ./././Mathlib/Topology/PartitionOfUnity.lean:363:1: error: BumpCovering.coe_single.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/PartitionOfUnity.lean:481:1: error: BumpCovering.toPOUFun_eq_mul_prod.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/PartitionOfUnity.lean:507:1: error: BumpCovering.exists_finset_toPOUFun_eventuallyEq.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/PartitionOfUnity.lean:553:1: error: BumpCovering.toPartitionOfUnity_eq_mul_prod.{u, v} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/PartitionOfUnity.lean:559:1: error: BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq.{u, v} theorem statement contains `Classical.propDecidable`. | |
| -- Mathlib.Topology.VectorBundle.Basic | |
| Error: ./././Mathlib/Topology/VectorBundle/Basic.lean:119:1: error: Pretrivialization.coe_linearMapAt.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/VectorBundle/Basic.lean:130:1: error: Pretrivialization.linearMapAt_apply.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/VectorBundle/Basic.lean:234:1: error: Trivialization.coe_linearMapAt.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: ./././Mathlib/Topology/VectorBundle/Basic.lean:244:1: error: Trivialization.linearMapAt_apply.{u_4, u_3, u_2, u_1} theorem statement contains `Classical.propDecidable`. | |
| Error: The process '/usr/bin/env' failed with exit code 1 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment