-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_mul_right (hc : c ≠ 0) :
    (∫ x in a..b, f (x * c)) = c⁻¹ • ∫ x in a * c..b * c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) =
    c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x ∂ENNReal.ofReal |c| • Measure.map (fun x => x * c) volume

Tactic:
simp_rw [integral_smul_measure, intervalIntegral, A.setIntegral_map,
  ENNReal.toReal_ofReal (abs_nonneg c)]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      |c| •
        (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
have A : MeasurableEmbedding fun x => x * c :=
  (Homeomorph.mulRight₀ c hc).isClosedEmbedding.measurableEmbedding

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x

Proof state:
case inl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
h : c < 0
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      |c| •
        (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)

Tactic:
simp [h, mul_div_cancel_right₀, hc, abs_of_neg,
  Measure.restrict_congr_set (α := ℝ) (μ := volume) Ico_ae_eq_Ioc]

Result:
no goals

Proof state:
case inr
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
h : 0 < c
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      |c| •
        (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)

Tactic:
simp [h, mul_div_cancel_right₀, hc, abs_of_pos]

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      |c| •
        (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)

Tactic:
rcases hc.lt_or_lt with h | h

Result:
case inl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
h : c < 0
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      |c| •
        (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)

case inr
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
h : 0 < c
⊢ ∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume =
    c⁻¹ •
      |c| •
        (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume -
          ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x

Tactic:
conv_rhs => rw [← Real.smul_map_volume_mul_right hc]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) =
    c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x ∂ENNReal.ofReal |c| • Measure.map (fun x => x * c) volume