search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.38k stars 308 forks source link

`auto_param`s for `volume` doing less than they used to #4637

Open hrmacbeth opened 1 year ago

hrmacbeth commented 1 year ago

Per @urkud on #4628,

Lean 3 was able to apply, e.g., instances about measure_theory.measure.prod to the volume on the Cartesian product. Lean 4 can't do this, so we need to duplicate many instances.

See also https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/MeasureTheory.2EMeasure.2ELebesgue.2EBasic.20!4.234552

I believe this issue is not yet fully understood, but I'm recording it here for when someone has time to investigate.

urkud commented 1 year ago

How is it related to auto_params?