case inl
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)

case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c ≠ 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
rcases eq_or_ne c 0 with (hc | hc)
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]]
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c ≠ 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
rw [intervalIntegrable_iff'] at hf ⊢
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]]
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]]
have A : MeasurableEmbedding fun x => x * c⁻¹ :=
  (Homeomorph.mulRight₀ _ (inv_ne_zero hc)).closedEmbedding.measurableEmbedding
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
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]])
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ IntegrableOn (fun x => f (c * x)) [[a / c, b / c]]
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]
case h.e'_5
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) = f

case h.e'_6
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ (fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]
case inr
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
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]])
convert hf using 1
case inl
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (0 * x)) volume (a / 0) (b / 0)
case inl
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (c * x)) volume (a / c) (b / c)
rw [hc]
no goals
case inl
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
hc : c = 0
⊢ IntervalIntegrable (fun x => f (0 * x)) volume (a / 0) (b / 0)
simp
no goals
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ ENNReal.ofReal (Abs.abs c⁻¹) ≠ 0
simpa
case h.e'_5.h
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) x✝ = f x✝
case h.e'_5
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) = f
ext
case h.e'_5.h
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ f (c * (x✝ * c⁻¹)) = f x✝
case h.e'_5.h
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ ((fun x => f (c * x)) ∘ fun x => x * c⁻¹) x✝ = f x✝
simp only [comp_apply]
case h.e'_5.h.e_a
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ c * (x✝ * c⁻¹) = x✝
case h.e'_5.h
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ f (c * (x✝ * c⁻¹)) = f x✝
congr 1
case h.e'_5.h.e_a
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ c * x✝ = x✝ * c
case h.e'_5.h.e_a
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ c * (x✝ * c⁻¹) = x✝
field_simp
no goals
case h.e'_5.h.e_a
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
x✝ : ℝ
⊢ c * x✝ = x✝ * c
ring
case h.e'_6
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]
case h.e'_6
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ (fun x => x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]
rw [preimage_mul_const_uIcc (inv_ne_zero hc)]
no goals
case h.e'_6
ι : Type ?u.6953593
𝕜 : Type ?u.6953596
E : Type u_1
F : Type ?u.6953602
A✝ : Type ?u.6953605
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntegrableOn f [[a, b]]
c : ℝ
hc : c ≠ 0
A : MeasurableEmbedding fun x => x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]
field_simp [hc]