Rewrite in Set Integral with hypothesis

Stream: mathlib4

[Enrico Borba]

Unsure if this is a mathlib question, because I'm not sure if there is some integral_* lemma that could help out here.

How can I rewrite a term inside an set integral with the hypothesis that the variable of integration is a member of the set being integrated over? Specifically I'm trying to do

import Mathlib.MeasureTheory.Integral.IntervalIntegral

example : ∫ (θ : ℝ) in Set.Icc 0 π, ENNReal.toReal (ENNReal.ofReal θ.sin) ∂ℙ = 2 := by
  conv => lhs; arg 2; intro θ; rw [ENNReal.toReal_ofReal ?pos]

But I don't think conv is the right move here as it isn't aware of the context θ is under.

[Enrico Borba]

Ended up solving it with docs#MeasureTheory.set_integral_congr and docs#Set.EqOn:

-- This can probably have a weaker condition, that f s is almost everywhere non-negative.
lemma set_integral_toReal_ofReal [MeasureSpace α] {s : Set α} {f : α → ℝ} (hs : MeasurableSet s) (hf : ∀ x ∈ s, f x ≥ 0) :
  ∫ (x : α) in s, ENNReal.toReal (ENNReal.ofReal (f x)) = ∫ (x : α) in s, f x := by

  have comp_eq : (fun x => ENNReal.toReal (ENNReal.ofReal (f x))) = (ENNReal.toReal ∘ ENNReal.ofReal ∘ f) := by rfl
  simp_rw [comp_eq]

  have eq_on : Set.EqOn (ENNReal.toReal ∘ ENNReal.ofReal ∘ f) f s := by
    intro x hx
    simp only [Function.comp_apply, ENNReal.toReal_ofReal_eq_iff]
    exact hf x hx

  rw [MeasureTheory.set_integral_congr hs eq_on]

Edited because I didn't actually resolve the goals in the original message...

[David Loeffler]

The problem is that set_integral is defined by restricting the measure, not the domain of integration. You can either use set_integral_congr + EqOn as you did, or you can rewrite with MeasureTheory.integral_subtype to get an integral where the integration variable lives in the subtype ↑s, so you can rewrite using x.property.

[Enrico Borba]

Oh that's a nice idea. I had not seen docs#MeasureTheory.integral_subtype before