!4#3674 MeasureTheory.Measure.OuterMeasure

Stream: mathlib4

[MonadMaverick]

PR reopened: 3170 -> 3674

[MonadMaverick]

MonadMaverick said:

Mathlib.MeasureTheory.Measure.OuterMeasure almost fixed.

But importing Mathlib.Analysis.SpecificLimits.Basic causes error in synthesizing instances

It seems that importing Mathlib.Topology.Algebra.Algebra introduces too many possibilities

For example, around line 840 in theorem smul_ofFunction:

▶ 837:5-837:42: information:
[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ?m.7236733 ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ?m.7236733 ▶

[Meta.synthInstance] 💥 SMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ?m.7236733 ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ?m.7236733 ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 SMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 SMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶

[Meta.synthInstance] 💥 HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶


▶ 837:70-837:75: information:
[Meta.synthInstance] ✅ HSMul ℝ≥0∞ (Set α → ℝ≥0∞) (Set α → ℝ≥0∞) ▶


▶ 837:81-837:95: information:
[Meta.synthInstance] ✅ Set α → SMul ℝ≥0∞ ℝ≥0∞ ▶

[Meta.synthInstance] ✅ Mul ℝ≥0∞ ▶

[Meta.synthInstance] ✅ MulZeroClass ℝ≥0∞ ▶

[Meta.synthInstance] ✅ MulZeroClass ℝ≥0∞ ▶


▶ 837:5-837:42: error:
typeclass instance problem is stuck, it is often due to metavariables
  HSMul ℝ≥0∞ (OuterMeasure α) (OuterMeasure α)

without Mathlib.Topology.Algebra.Algebra

▶ 837:5-837:42: information:
[Meta.synthInstance] ✅ HSMul ℝ≥0∞ (MeasureTheory.OuterMeasure α) (MeasureTheory.OuterMeasure α) ▶


▶ 837:70-837:75: information:
[Meta.synthInstance] ✅ HSMul ℝ≥0∞ (Set α → ℝ≥0∞) (Set α → ℝ≥0∞) ▶


▶ 837:81-837:95: information:
[Meta.synthInstance] ✅ Set α → SMul ℝ≥0∞ ℝ≥0∞ ▶

[Meta.synthInstance] ✅ Mul ℝ≥0∞ ▶

[Meta.synthInstance] ✅ MulZeroClass ℝ≥0∞ ▶

[Meta.synthInstance] ✅ MulZeroClass ℝ≥0∞ ▶

[Scott Morrison]

@MonadMaverick, you might try merging eta_cleanup and seeing if that helps.

[MonadMaverick]

Are you referring to the branch reenableeta?
I have tried using the toolchain gebner/lean4:reenableeta230411, but I am still getting the same results.

[Alex J. Best]

I guess scott means https://github.com/leanprover-community/mathlib4/pull/3668 so merging master should be enough

[MonadMaverick]

Alex J. Best said:

I guess scott means https://github.com/leanprover-community/mathlib4/pull/3668 so merging master should be enough

Thank you.
I'll give it a go

[MonadMaverick]

Tried with latest master.
No luck

[Scott Morrison]

I'm confused, the PR is failing with

./././Mathlib.lean:1:0: error: import Mathlib.MeasureTheory.Measure.tmp failed, environment already contains 'hasSum_geometric_two'' from Mathlib.Analysis.SpecificLimits.Basic

Could you bring this PR into a state where I can see the issue discussed here, and then ping me?

[MonadMaverick]

@Scott Morrison

I've pushed the changes for reproducing the errors.

The following is a description of what's going on:

• import Mathlib.Analysis.SpecificLimits.Basic causes the error
  • there are 5 imports in SpecificLimits.Basic
  • import Mathlib.Topology.Algebra.Algebra causes the error
• OuterMeasure uses 1 lemma from SpecificLimits.Basic
  • which is:
    • ofFunction in OuterMeasure uses
    • ENNReal.exists_pos_sum_of_countable in SpecificLimits.Basic
• tmp.lean was created to isolated the lemma ENNReal.exists_pos_sum_of_countable and it compiles
  • ENNReal.exists_pos_sum_of_countable does not depend on Topology.Algebra.Algebra
  • tmp.lean is a just a stripped copy of SpecificLimits.Basic that only provides ENNReal.exists_pos_sum_of_countable for OuterMeasure to use
• OuterMeasure.lean is almost fixed
  • for the first import
    • import Mathlib.Analysis.SpecificLimits.Basic causes the error
    • import Mathlib.MeasureTheory.Measure.tmp compiles

[MonadMaverick]

And git revert HEAD toggles the 2 scenarios

[Scott Morrison]

Sorry, I still don't see it. The build is currently failing with Error: ./././Mathlib/MeasureTheory/Measure/OuterMeasure.lean:433:26: error: typeclass instance problem is stuck, it is often due to metavariables which is very far from smul_ofFunction.

Maybe you could clarify what "the error" is referring to in your message above? Sorry if I'm being dense.

[Scott Morrison]

Further there's no file Mathlib.MeasureTheory.Measure.tmp in your PR.

[Scott Morrison]

Okay, in any case, I've pushed a candidate fix to the errors in this PR.

[Scott Morrison]

Lean is failing to find IsScalarTower ℝ≥0∞ ℝ≥0∞ ℝ≥0∞, even though IsScalarTower.right is an instance. I've included in comments the trace of typeclass search crashing, to help debugging later.

I've added some local instance statements to provide this missing instance.

[Pol'tta / Miyahara Kō]

It works well to change the priority of IsScalarTower.of_ring_hom.

[Eric Wieser]

There is a PR that needs forward-porting that should help with that missing instance

[Ruben Van de Velde]

!4#3778?

[Pol'tta / Miyahara Kō]

Unfortunately, that PR didn't help this file.