gcongr: always running `intro` can be too strong

Stream: mathlib4

[Michael Rothgang]

The following example is minimized from the carleson project. I presume this is a regression from #16747.

import Mathlib

open MeasureTheory Metric
open scoped NNReal ENNReal

theorem minimized {X : Type*} [MetricSpace X] [MeasureSpace X] {x : X} {a : ℝ≥0} {cutoff : X → ℝ≥0}
    (hf : Measurable fun y ↦ (cutoff y : ℝ≥0∞))
    (hf' : ∀ y : ball x 37, a ≤ cutoff y) :
    ∫⁻ (y : X) in ball x 37, a ≤ ∫⁻ (y : X) in ball x 37, ↑(cutoff y) := by
  gcongr with y'
  -- now, the goal has `y' : X`, which is too strong:
  -- I want to take `y'` in the ball, not just in `X`
  sorry

  -- -- in contrast, this works:
  -- apply setLIntegral_mono hf
  -- intro y' hy'
  -- -- closing the sorry
  -- exact ENNReal.coe_le_coe.mpr (hf' ⟨y', hy'⟩)

The automatic running of intro is overzealous here: it introduces a new variable without any side conditions.
I agree that running intro is often desirable. I wonder

• could it be fixed, to recognise that it should introduce y in the ball?
• if not, could running intro be made configurable?

[Michael Rothgang]

CC @Heather Macbeth as the author of the above PR (see the above post)

[Heather Macbeth]

I don't think this is a regression from #16747. Rather, this is just a matter of the choice of gcongr lemma for lintegral: when Floris and I added the tagging in #7681, we apparently chose docs#MeasureTheory.lintegral_mono_fn rather than docs#MeasureTheory.lintegral_mono_ae.

[Heather Macbeth]

That is, we told gcongr to reduce an inequality between Lebesgue integrals to ∀ x, f x ≤ g x rather than to ∀ᵐ (a : α) ∂μ, f a ≤ g a. The latter is more general and it's what would be needed for your use case, but the former is easier to use in the cases where it does work. So I'm not sure what the right choice is!

[Michael Rothgang]

I see, thanks for explaining! Let me think about this.
CC @Floris van Doorn This should be interesting to discuss, next time we meet.

[Floris van Doorn]

Yes, we should make sure we tag the correct lemmas with @[gcongr]. Perhaps we can add an additional gcongr lemma that works for setLIntegral/setIntegral, but is still pointwise and has a higher priority (I don't know if the gcongr tactic supports that).

[Heather Macbeth]

There's no prioritization in gcongr, kind of on principle: having only one lemma which applies in a given situation means that gcongr is opinionated but fast.

(Actually, there is back-door support for prioritization: if there are two lemmas which apply they will be tried in some order which is presumably determined by the tagging order in the library and/or the order of imports. But hopefully this is not currently being exploited anywhere in the library, and maybe someday we will have linters to guard against it.)

[Yaël Dillies]

Heather, you said in #17653 that a tagged lemma of the form f a b ≤ f c d wouldn't apply when trying to prove f a b ≤ f a d. Is that not a form of prioritization as well?

[Heather Macbeth]

Nope, that's the opposite: gcongr looks at the goal and can read off which lemma to use (the 1-input or 2-input version) without having to try both.