MeasureTheory.Measure.Lebesgue.Basic !4#4552

Stream: mathlib4

[Pol'tta / Miyahara Kō]

In Lean 4, the following tc search fails, even if we make volume reducible in MeasureSpaceDef.

variable [Fintype ι]
#synth SigmaFinite (volume : Measure (ι → ℝ))
-- fails
#synth SigmaFinite (Measure.pi fun _ => volume : Measure (ι → ℝ))
-- defeq and succeeds
#synth AddLeftInvariant (volume : Measure (ι → ℝ))
-- fails
#synth AddLeftInvariant (Measure.pi fun _ => (stdOrthonormalBasis ℝ ℝ).toBasis.addHaar : Measure (ι → ℝ))
-- defeq and succeeds

These instances are required in this file.
This file can be built by specifying latter measures now, but this should be fixed clearly.
Does anyone know how to fix this?

[Yury G. Kudryashov]

Which instance does Lean 3 find?

[Pol'tta / Miyahara Kō]

@Yury G. Kudryashov The both. (SigmaFinite & AddLeftInvariant)

[Eric Wieser]

I think Yury is asking what is found, not whether the above succeed

[Pol'tta / Miyahara Kō]

Sorry.
SigmaFinite...MeasureTheory.Measure.pi.sigmaFinite in MeasureTheory.Constructions.Pi
AddLeftInvariant...MeasureTheory.Pi.isAddLeftInvariant_volume in MeasureTheory.Constructions.Pi

[Pol'tta / Miyahara Kō]

These are aligned names.

[Yury G. Kudryashov]

I meant something like

lemma aux : sigma_finite (volume : measure (ι → ℝ)) := by apply_instance
#print aux

[Yury G. Kudryashov]

(in Lean 3)

[Yury G. Kudryashov]

There is more than 1 way to prove this instance.

[Yury G. Kudryashov]

I wonder which one works in Lean 3 and fails in Lean 4.

[Yury G. Kudryashov]

If Lean 3 can see through volume and Lean 4 can't, then we should duplicate each instance about Measure.prod and Measure.pi for MeasureSpaces.