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

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

Tactic:
rw [intervalIntegrable_iff'] at hf ⊢

Result:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : a ≤ b
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]] volume

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] (Measure.map (fun x => x + c) volume)
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]] volume

Tactic:
convert (MeasurableEmbedding.integrableOn_map_iff A).mp hf using 1

Result:
case h.e'_7
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] (Measure.map (fun x => x + c) volume)
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ [[a - c, b - c]] = (fun x => x + c) ⁻¹' [[a, b]]

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : a ≤ b
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]] volume

Tactic:
have A : MeasurableEmbedding fun x => x + c :=
  (Homeomorph.addRight c).isClosedEmbedding.measurableEmbedding

Result:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]] volume

Proof state:
case h.e'_7
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] (Measure.map (fun x => x + c) volume)
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ [[a - c, b - c]] = (fun x => x + c) ⁻¹' [[a, b]]

Tactic:
rw [preimage_add_const_uIcc]

Result:
no goals

Proof state:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]] volume

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Result:
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntegrableOn f [[a, b]] (Measure.map (fun x => x + c) volume)
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]] volume

Proof state:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
this :
  ∀ {a b : ℝ}, IntervalIntegrable f volume a b → a ≤ b → IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
h : ¬a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)

Tactic:
exact IntervalIntegrable.symm (this hf.symm (le_of_not_le h))

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 (x + c)) volume (a - c) (b - c)

Tactic:
wlog h : a ≤ b generalizing a b

Result:
case inr
E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
this :
  ∀ {a b : ℝ}, IntervalIntegrable f volume a b → a ≤ b → IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
h : ¬a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)

E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b✝ c a b : ℝ
hf : IntervalIntegrable f volume a b
h : a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)