!4#3170

Stream: mathlib4

[MonadMaverick]

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∞ ▶

[MonadMaverick]

OuterMeasure.lean This file builds without error

[Kevin Buzzard]

?m.7236733 is quite impressive!