awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
pos :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))

Tactic:
rw [I, J]
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
⊢ ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x

Tactic:
have hF' (x : ℝ) (hx : x ∈ c) : HasFDerivWithinAt f (F' x) c x :=
    (hf' x (c_s hx)).hasFDerivWithinAt.mono c_s
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
apply : ∀ (x : ℝ) (hx : x ∈ c), f' x • g (f x) = |(F' x).det| • g (f x)
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))

Tactic:
apply setIntegral_congr_fun hc (fun x hx ↦ ?_)

Premises used: MeasureTheory.setIntegral_congr_fun
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
simp : f' x • g (f x) = |f' x| • g (f x)
⊢ f' x • g (f x) = |(F' x).det| • g (f x)

Tactic:
simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
      ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']

Premises used: ContinuousLinearMap.coe_coe, ContinuousLinearMap.one_apply, LinearMap.det_ring, smul_eq_mul, ContinuousLinearMap.smulRight_apply, one_mul
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
x : ℝ
hx : x ∈ c
rw rw₁ : f' x • g (f x) = f' x • g (f x)
⊢ f' x • g (f x) = |f' x| • g (f x)

Tactic:
rw [abs_of_nonneg (deriv_c x hx)]

Premises used: abs_of_nonneg
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))

Tactic:
have : ∫ x in c, f' x • g (f x) = ∫ x in c, |(F' x).det| • g (f x) := by
    apply setIntegral_congr_fun hc (fun x hx ↦ ?_)
    simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
      ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']
    rw [abs_of_nonneg (deriv_c x hx)]
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))
pos :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))

Tactic:
rw [this]
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))

Tactic:
integral_image_eq_integral_abs_det_fderiv_smul _ hc hF' inj_c _

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul
-- 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 : MonotoneOn f s
g : ℝ → F
H : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
H' : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
a b c : Set ℝ
h_union : a ∪ (b ∪ c) = s
ha : MeasurableSet a
hb : MeasurableSet b
hc : MeasurableSet c
h_disj : Disjoint a (b ∪ c)
h_disj' : Disjoint b c
a_count : a.Countable
fb_count : (f '' b).Countable
deriv_b : ∀ x ∈ b, f' x = 0
deriv_c : ∀ x ∈ c, 0 ≤ f' x
inj_c : InjOn f c
a_s : a ⊆ s
bc_s : b ∪ c ⊆ s
b_s : b ⊆ s
c_s : c ⊆ s
I :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
J :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hF' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' c)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ |(F' x).det| • g (f x))

Tactic:
exact integral_image_eq_integral_abs_det_fderiv_smul _ hc hF' inj_c _

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul
-- 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
hf'₁ : DifferentiableOn ℝ f (interior (Icc a b))
hf'_nonneg : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Icc a b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Icc a b) hf

Premises used: monotoneOn_of_deriv_nonneg, convex_Icc
-- 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
hf'₁ : DifferentiableOn ℝ f (Ioo a b)
⊢ DifferentiableOn ℝ f (interior (Icc a b))

Tactic:
rw [interior_Icc]

Premises used: interior_Icc
-- 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
⊢ DifferentiableOn ℝ f (Ioo a b)

Tactic:
fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- 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
⊢ DifferentiableOn ℝ f (Ioo a b)

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

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.differentiableWithinAt
-- 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
hf'_nonneg : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
⊢ ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x

Tactic:
rw [interior_Icc]

Premises used: interior_Icc
-- 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
z : ℝ
hz : z ∈ Ioo a b
⊢ 0 ≤ deriv f z

Tactic:
simpa [(hff' z hz).deriv] using hf' z hz

Premises used: HasDerivAt.deriv
-- 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
⊢ MonotoneOn f (Icc a b)

Tactic:
have M : MonotoneOn f (Icc a b) := by
    apply monotoneOn_of_deriv_nonneg (convex_Icc a b) hf
    · rw [interior_Icc]
      exact fun z hz ↦ (hff' z hz).differentiableAt.differentiableWithinAt
    · rw [interior_Icc]
      intro z hz
      simpa [(hff' z hz).deriv] using hf' z hz
-- 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
⊢ 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:
apply setIntegral_congr_set

Premises used: MeasureTheory.setIntegral_congr_set
-- 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 : f '' Icc a b =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
⊢ Icc (f a) (f b) =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b

Tactic:
rw [← hf.image_Icc_of_monotoneOn hab M]

Premises used: ContinuousOn.image_Icc_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)
⊢ f '' Ioo a b \ f '' Icc a b = ∅

Tactic:
grind
-- 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 (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' Ioo a b \ f '' Icc a b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]
-- 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 : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' Icc a b \ f '' Ioo a b) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f '' Icc a b =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b

Tactic:
refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩

Premises used: Iff.mpr, MeasureTheory.ae_eq_set, And.intro
-- 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)
⊢ f '' Icc a b \ f '' Ioo a b ⊆ {f a, f b}

Tactic:
grind
-- 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)
⊢ f '' Icc a b \ f '' Ioo a b ⊆ {f a, f b}

Tactic:
have : f '' (Icc a b) \ f '' Ioo a b ⊆ {f a, f b} := by grind
-- 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}
hst : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {f a, f b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' Icc a b \ f '' Ioo a b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_mono_null this

Premises used: MeasureTheory.measure_mono_null