how to do variable substitute？

Stream: new members

[Junqi Liu]

example (a : ℝ) (_ : 0 < a) : ∫ (z : ℝ) in (0)..1, 1 / (1 - a * z) = ∫ (z : ℝ) in (0)..a, (1 / a) * 1 / (1 - z) := by
  sorry

how to do variable substitute $z = a * z$

[Mitchell Lee]

Look at the statement and proof of docs#MeasureTheory.integral_comp_mul_left_Ioi, and try to prove a version of that theorem for integrals over bounded intervals.