awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
this : f '' Icc a b \ f '' Ioo a b ⊆ {f a, f b}
⊢ Set.Finite (α := ℝ) {f a, f b}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
this : f '' Icc a b \ f '' Ioo a b ⊆ {f a, f b}
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {f a, f b} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply Finite.measure_zero (by simp)

Premises used: Set.Finite.measure_zero
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)

Tactic:
have A : ∫ u in Icc (f a) (f b), g u = ∫ u in f '' (Ioo a b), g u := by
    apply setIntegral_congr_set
    rw [← hf.image_Icc_of_monotoneOn hab M]
    refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩
    have : f '' (Icc a b) \ f '' Ioo a b ⊆ {f a, f b} := by grind
    apply measure_mono_null this
    apply Finite.measure_zero (by simp)
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)
hf'₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x
hf₁ : MonotoneOn f (Ioo a b)
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)

Tactic:
rw [A, integral_Icc_eq_integral_Ioo,
    integral_image_eq_integral_deriv_smul_of_monotoneOn measurableSet_Ioo]

Premises used: MeasureTheory.integral_Icc_eq_integral_Ioo, measurableSet_Ioo, MeasureTheory.integral_image_eq_integral_deriv_smul_of_monotoneOn
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

Tactic:
fun z hz ↦ (hff' z hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

Tactic:
exact fun z hz ↦ (hff' z hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)
⊢ MonotoneOn f (Ioo a b)

Tactic:
M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f a) (f b))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)
⊢ MonotoneOn f (Ioo a b)

Tactic:
exact M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
hst : Icc (f a) (f b) =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume

Tactic:
apply integrableOn_congr_set_ae

Premises used: MeasureTheory.integrableOn_congr_set_ae
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume

Tactic:
have A : IntegrableOn g (Icc (f a) (f b)) ↔ IntegrableOn g (f '' (Ioo a b)) := by
    apply integrableOn_congr_set_ae
    rw [← hf.image_Icc_of_monotoneOn hab M]
    refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩
    have : f '' (Icc a b) \ f '' Ioo a b ⊆ {f a, f b} := by grind
    apply measure_mono_null this
    apply Finite.measure_zero (by simp)
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
hf'₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x
hf₁ : MonotoneOn f (Ioo a b)
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) (Icc a b)
      volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume

Tactic:
rw [A, integrableOn_Icc_iff_integrableOn_Ioo,
    integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn measurableSet_Ioo]

Premises used: MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn, measurableSet_Ioo, integrableOn_Icc_iff_integrableOn_Ioo
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

Tactic:
fun z hz ↦ (hff' z hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

Tactic:
exact fun z hz ↦ (hff' z hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ MonotoneOn f (Ioo a b)

Tactic:
M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
M : MonotoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f a) (f b)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ MonotoneOn f (Ioo a b)

Tactic:
exact M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
⊢ ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x

Tactic:
have hg' (x) (hx : x ∈ s) : HasDerivWithinAt e (-f' x) s x := (hf' x hx).neg
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
rw : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in e '' s, (u ∘ n) x
⊢ ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)

Tactic:
rw [← lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn hs hg' hf.neg (u ∘ n)]

Premises used: AntitoneOn.neg, MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn, Function.comp
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in e '' s, (u ∘ n) x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)

Tactic:
have A : ∫⁻ x in e '' s, u (n x) = ∫⁻ x in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x) := by
    rw [← lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn hs hg' hf.neg (u ∘ n)]; rfl
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
⊢ ∫⁻ (x : ℝ) in n '' e '' s, u x = ∫⁻ (x : ℝ) in e '' s, ENNReal.ofReal |(-1)| * u (n x)

Tactic:
have B : ∫⁻ x in n '' e '' s, u x = ∫⁻ x in e '' s, ENNReal.ofReal (|-1|) * u (n x) :=
    lintegral_image_eq_lintegral_abs_deriv_mul (hs.image_of_monotoneOn hf.neg)
      (fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n '' e '' s, u x = ∫⁻ (x : ℝ) in e '' s, ENNReal.ofReal |(-1)| * u (n x)
⊢ ∫⁻ (x : ℝ) in n '' e '' s, u x = ∫⁻ (x : ℝ) in e '' s, u (n x)

Tactic:
simp only [abs_neg, abs_one, ENNReal.ofReal_one, one_mul] at B

Premises used: abs_neg, ENNReal.ofReal_one, abs_one, one_mul
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n '' e '' s, u x = ∫⁻ (x : ℝ) in e '' s, u (n x)
⊢ ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)

Tactic:
rw [A, ← image_comp] at B

Premises used: Set.image_comp
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
⊢ ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)

Tactic:
B
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
h : ∀ (x : ℝ) (hx : x ∈ s), f x = (n ∘ e) x
h₁ : ∀ (x : ℝ), u (f x) = (u ∘ n) (e x)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)

Tactic:
convert! B using 4 with x hx x
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
x : ℝ
hx : x ∈ s
⊢ f x = (n ∘ e) x

Tactic:
simp [n, e]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
x : ℝ
⊢ u (f x) = (u ∘ n) (e x)

Tactic:
simp [n, e]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
⊢ ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) = (volume : (a : Set ℝ) → ℝ≥0∞) (f '' s)

Tactic:
simpa using (lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn hs hf' hf 1).symm

Premises used: MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn, OfNat.ofNat, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
⊢ ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x

Tactic:
have hg' (x) (hx : x ∈ s) : HasDerivWithinAt e (-f' x) s x := (hf' x hx).neg
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
rw :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (g ∘ n) (e '' s) volume
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume

Tactic:
rw [← integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]

Premises used: AntitoneOn.neg, MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn, Function.comp
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (g ∘ n) (e '' s) volume

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume

Tactic:
have A : IntegrableOn (fun x ↦ g (n x)) (e '' s)
      ↔ IntegrableOn (fun x ↦ (-f' x) • (g ∘ n) (e x)) s := by
    rw [← integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]; rfl
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ HSMul.hSMul (α := ℝ) |(-1)| (g (n x))) (e '' s) volume

Tactic:
have B : IntegrableOn g (n '' e '' s) ↔ IntegrableOn (fun x ↦ (|-1| : ℝ) • g (n x)) (e '' s) :=
    integrableOn_image_iff_integrableOn_abs_deriv_smul (hs.image_of_monotoneOn hf.neg)
      (fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
B :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ HSMul.hSMul (α := ℝ) |(-1)| (g (n x))) (e '' s) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume

Tactic:
simp only [abs_neg, abs_one, one_smul] at B

Premises used: abs_neg, one_smul, abs_one
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
B :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n ∘ e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume

Tactic:
rw [A, ← image_comp] at B

Premises used: Set.image_comp