-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem comp_mul_left (hf : IntervalIntegrable f volume a b) (c : ℝ) :
    IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

Proof state:
case h.e'_6
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) = f

Tactic:
ext

Result:
case h.e'_6.h
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) x✝ = f x✝

Proof state:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c ≠ 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

Tactic:
rw [intervalIntegrable_iff'] at hf ⊢

Result:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]] volume

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ ENNReal.ofReal |c⁻¹| ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ IntegrableOn ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) ((fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume

Tactic:
convert hf using 1

Result:
case h.e'_6
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) = f

case h.e'_7
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ (fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]

Proof state:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]] volume

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

Result:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]] volume

Proof state:
case h.e'_6.h
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) x✝ = f x✝

Tactic:
simp only [comp_apply]

Result:
case h.e'_6.h
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ f (c * (x✝ * c⁻¹)) = f x✝

Proof state:
case h.e'_6.h
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ f (c * (x✝ * c⁻¹)) = f x✝

Tactic:
congr 1

Result:
case h.e'_6.h.e_a
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ c * (x✝ * c⁻¹) = x✝

Proof state:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]] volume

Tactic:
rw [← Real.smul_map_volume_mul_right (inv_ne_zero hc), IntegrableOn, Measure.restrict_smul,
  integrable_smul_measure (by simpa : ENNReal.ofReal |c⁻¹| ≠ 0) ENNReal.ofReal_ne_top,
  ← IntegrableOn, MeasurableEmbedding.integrableOn_map_iff A]

Result:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ IntegrableOn ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) ((fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume

Proof state:
case h.e'_7
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]

Tactic:
field_simp [hc]

Result:
no goals

Proof state:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (0 * x)) volume (a / 0) (b / 0)

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

Tactic:
rcases eq_or_ne c 0 with (hc | hc)

Result:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c ≠ 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

Proof state:
case h.e'_6.h.e_a
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ c * (x✝ * c⁻¹) = x✝

Tactic:
field_simp

Result:
no goals

Proof state:
case h.e'_7
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ (fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]

Tactic:
rw [preimage_mul_const_uIcc (inv_ne_zero hc)]

Result:
case h.e'_7
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntegrableOn f [[a, b]] volume
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]

Proof state:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

Tactic:
rw [hc]

Result:
case inl
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (0 * x)) volume (a / 0) (b / 0)