awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
inr :
  IntegrableOn.{0, u_3} (α := ℝ) (ε := ε) (mα := Real.measurableSpace)
    ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) ((fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (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]

Premises used: MeasurableEmbedding.integrableOn_map_iff, MeasureTheory.Measure.restrict_smul, Real.smul_map_volume_mul_right, MeasureTheory.IntegrableOn, MeasureTheory.integrable_smul_measure, inv_ne_zero, ENNReal.ofReal_ne_top
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
⊢ IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume

Tactic:
hf
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
h₁ : ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) = f
h₂ : (fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]
⊢ IntegrableOn.{0, u_3} (α := ℝ) (ε := ε) (mα := Real.measurableSpace)
    ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) ((fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume

Tactic:
convert! hf using 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
h₁ : ∀ (x : ℝ), ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) x = f x
⊢ ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) = f

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
x : ℝ
h₁ : f (c * (x * c⁻¹)) = f x
⊢ ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) x = f x

Tactic:
simp only [comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
x : ℝ
h₁ : c * (x * c⁻¹) = x
⊢ f (c * (x * c⁻¹)) = f x

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
x : ℝ
⊢ c * (x * c⁻¹) = x

Tactic:
field
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
h₁ : [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]
⊢ (fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]

Tactic:
rw [preimage_mul_const_uIcc (inv_ne_zero hc)]

Premises used: Set.preimage_mul_const_uIcc, inv_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
⊢ [[a / c / c⁻¹, b / c / c⁻¹]] = [[a, b]]

Tactic:
field_simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c ≠ 0
h_1 : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
h : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
⊢ ‖f (c * (c⁻¹ * min (a / c / c⁻¹) (b / c / c⁻¹)))‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c ≠ 0
h_1 : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
h : IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
⊢ IntervalIntegrable f volume a b

Tactic:
simpa [hc] using h.comp_mul_left (c := c⁻¹) h' (by simp)

Premises used: IntervalIntegrable.comp_mul_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
f : ℝ → E
c : ℝ
hc : c ≠ 0
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c) ↔ IntervalIntegrable f volume a b

Tactic:
exact ⟨fun h ↦ by simpa [hc] using h.comp_mul_left (c := c⁻¹) h' (by simp),
    (comp_mul_left · h h')⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x * c)) volume (a / c) (b / c)

Tactic:
simpa only [mul_comm] using comp_mul_left hf h h'

Premises used: IntervalIntegrable.comp_mul_left, mul_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
rw [min_sub_sub_right, sub_add, sub_self, sub_zero]

Premises used: sub_add, sub_self, sub_zero, min_sub_sub_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
have h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ⊤ := by
    rw [min_sub_sub_right, sub_add, sub_self, sub_zero]
    exact h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞)
        (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞) (hab : a ≤ b),
        IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c))
    (hab : ¬a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
wlog :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)

Tactic:
wlog hab : a ≤ b generalizing a b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
apply : ‖f (min b a)‖ₑ ≠ ∞
apply₁ : ‖f (min (b - c) (a - c) + c)‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)

Tactic:
apply IntervalIntegrable.symm (this hf.symm ?_ ?_ (le_of_not_ge hab))

Premises used: le_of_not_ge, IntervalIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
rw : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min b a)‖ₑ ≠ ∞

Tactic:
rw [min_comm]

Premises used: min_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
rw : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
⊢ ‖f (min (b - c) (a - c) + c)‖ₑ ≠ ∞

Tactic:
rw [min_comm]

Premises used: min_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
h'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ} (hf : IntervalIntegrable f volume a b) (h : ‖f (min a b)‖ₑ ≠ ∞) (h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞)
    (hab : a ≤ b), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
exact h'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume

Tactic:
rw [intervalIntegrable_iff' h] at hf

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
rw [intervalIntegrable_iff' h] at hf

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h₁ : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
rw [intervalIntegrable_iff' h] at hf

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h₁ : ‖f (min a b)‖ₑ ≠ ∞
h'₁ : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
⊢ a ≤ b

Tactic:
rw [intervalIntegrable_iff' h] at hf

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
rw : IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (x + c)) [[a - c, b - c]] volume
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume (a - c) (b - c)

Tactic:
rw [intervalIntegrable_iff' h'] at ⊢

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c

Tactic:
have A : MeasurableEmbedding fun x => x + c :=
    (Homeomorph.addRight c).isClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
⊢ IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Premises used: MeasureTheory.map_add_right_eq_self, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
⊢ ‖f (min a b)‖ₑ ≠ ∞

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Premises used: MeasureTheory.map_add_right_eq_self, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h₁ : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Premises used: MeasureTheory.map_add_right_eq_self, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h₁ : ‖f (min a b)‖ₑ ≠ ∞
h'₁ : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
⊢ a ≤ b

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Premises used: MeasureTheory.map_add_right_eq_self, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
hf₁ : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h₁ : ‖f (min a b)‖ₑ ≠ ∞
h'₁ : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab₁ : a ≤ b
⊢ MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c

Tactic:
rw [← map_add_right_eq_self volume c] at hf

Premises used: MeasureTheory.map_add_right_eq_self, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
⊢ IntegrableOn (α := ℝ) (mα := Real.measurableSpace) (f ∘ fun (x : ℝ) ↦ x + c) ((fun (x : ℝ) ↦ x + c) ⁻¹' [[a, b]])
    volume

Tactic:
(MeasurableEmbedding.integrableOn_map_iff A).mp hf

Premises used: MeasurableEmbedding.integrableOn_map_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
h₁ : [[a - c, b - c]] = (fun (x : ℝ) ↦ x + c) ⁻¹' [[a, b]]
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (x + c)) [[a - c, b - c]] volume

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

Premises used: MeasurableEmbedding.integrableOn_map_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a_1 b_1 : ℝ
inst_2 : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] (Measure.map (fun (x : ℝ) ↦ x + c) volume)
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + c
h₁ h₂ : [[a - c, b - c]] = [[a - c, b - c]]
⊢ [[a - c, b - c]] = (fun (x : ℝ) ↦ x + c) ⁻¹' [[a, b]]

Tactic:
rw [preimage_add_const_uIcc]

Premises used: Set.preimage_add_const_uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume a b
⊢ IntervalIntegrable f volume (a + c) (b + c)

Tactic:
simpa using hf.comp_add_right (-c)

Premises used: IntervalIntegrable.comp_add_right, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable f volume (a + c) (b + c)
rwa rwa₁ rwa₂ rwa₃ : ‖f (min a b + c)‖ₑ ≠ ∞
⊢ ‖f (min (a + c) (b + c))‖ₑ ≠ ∞

Tactic:
rwa [min_add_add_right]

Premises used: min_add_add_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable f volume (a + c) (b + c)
⊢ ‖f (min (a + c) (b + c))‖ₑ ≠ ∞

Tactic:
have : ‖f (min (a + c) (b + c))‖ₑ ≠ ⊤ := by rwa [min_add_add_right]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
c : ℝ
h : ‖f (min a b + c)‖ₑ ≠ ∞
hf : IntervalIntegrable f volume (a + c) (b + c)
this : ‖f (min (a + c) (b + c))‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (x + c)) volume a b

Tactic:
simpa using hf.comp_add_right c

Premises used: IntervalIntegrable.comp_add_right