awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c

Tactic:
union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)

Premises used: Iff.mpr, MeasureTheory.union_ae_eq_right_of_ae_eq_empty, MeasureTheory.ae_eq_empty
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
refine : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' a) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c

Tactic:
refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)

Premises used: Iff.mpr, MeasureTheory.union_ae_eq_right_of_ae_eq_empty, MeasureTheory.ae_eq_empty
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' a) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(a_count.image _).measure_zero _

Premises used: Set.Countable.measure_zero, Set.Countable.image
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' a) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (a_count.image _).measure_zero _

Premises used: Set.Countable.measure_zero, Set.Countable.image
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c

Tactic:
have A : (f '' a ∪ (f '' b ∪ f '' c) : Set ℝ) =ᵐ[volume] (f '' b ∪ f '' c : Set ℝ) := by
      refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
      exact (a_count.image _).measure_zero _
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
A : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c
⊢ f '' b ∪ f '' c =ᶠ[ae (F := Measure ℝ) volume] f '' c

Tactic:
have B : (f '' b ∪ f '' c : Set ℝ) =ᵐ[volume] f '' c :=
      union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr (fb_count.measure_zero _))
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
A : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c
B : f '' b ∪ f '' c =ᶠ[ae (F := Measure ℝ) volume] f '' c
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c

Tactic:
A.trans B

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
A : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' b ∪ f '' c
B : f '' b ∪ f '' c =ᶠ[ae (F := Measure ℝ) volume] f '' c
⊢ f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c

Tactic:
exact A.trans B

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x

Tactic:
have J : ∫⁻ x in f '' s, u x = ∫⁻ x in f '' c, u x := by
    apply setLIntegral_congr
    rw [← h_union, image_union, image_union]
    have A : (f '' a ∪ (f '' b ∪ f '' c) : Set ℝ) =ᵐ[volume] (f '' b ∪ f '' c : Set ℝ) := by
      refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
      exact (a_count.image _).measure_zero _
    have B : (f '' b ∪ f '' c : Set ℝ) =ᵐ[volume] f '' c :=
      union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr (fb_count.measure_zero _))
    exact A.trans B
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
rw : ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x)

Tactic:
rw [I, J]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
rw : c ⊆ a ∪ (b ∪ c)
⊢ c ⊆ s

Tactic:
rw [← h_union]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ c ⊆ a ∪ (b ∪ c)

Tactic:
subset_union_right.trans subset_union_right

Premises used: Set.subset_union_right, HasSubset.Subset.trans
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ c ⊆ a ∪ (b ∪ c)

Tactic:
exact subset_union_right.trans subset_union_right

Premises used: Set.subset_union_right, HasSubset.Subset.trans
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
⊢ c ⊆ s

Tactic:
have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
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:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
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), ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)

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

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
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 : ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal |f' x| * u (f x)
⊢ ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal |(F' x).det| * u (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:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
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₁ : ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal (f' x) * u (f x)
⊢ ENNReal.ofReal (f' x) * u (f x) = ENNReal.ofReal |f' x| * u (f x)

Tactic:
rw [abs_of_nonneg (deriv_c x hx)]

Premises used: abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hf' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
⊢ ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)

Tactic:
have : ∫⁻ x in c, ENNReal.ofReal (f' x) * u (f x)
      = ∫⁻ x in c, ENNReal.ofReal (|(F' x).det|) * u (f x) := by
    apply setLIntegral_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:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hf' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
this : ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
rw : ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hf' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
this : ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)

Tactic:
lintegral_image_eq_lintegral_abs_det_fderiv_mul _ hc hf' inj_c _

Premises used: MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf'_1 : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn f s
u : ℝ → ℝ≥0∞
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
I : ∫⁻ (x : ℝ) in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x)
J : ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in f '' c, u x
c_s : c ⊆ s
F' : ℝ → ℝ →L[ℝ] ℝ := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
hf' : ∀ (x : ℝ) (hx : x ∈ c), HasFDerivWithinAt f (F' x) c x
this : ∫⁻ (x : ℝ) in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)
⊢ ∫⁻ (x : ℝ) in f '' c, u x = ∫⁻ (x : ℝ) in c, ENNReal.ofReal |(F' x).det| * u (f x)

Tactic:
exact lintegral_image_eq_lintegral_abs_det_fderiv_mul _ hc hf' inj_c _

Premises used: MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : MonotoneOn 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_monotoneOn hs hf' hf 1).symm

Premises used: MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn, 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 : MonotoneOn f s
g : ℝ → F
rcases :
  ∀ (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),
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume ↔
      IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) s volume

Tactic:
rcases exists_decomposition_of_monotoneOn_hasDerivWithinAt hs hf hf' with
    ⟨a, b, c, h_union, ha, hb, hc, h_disj, h_disj', a_count, fb_count, deriv_b, deriv_c, inj_c⟩

Premises used: MeasureTheory.exists_decomposition_of_monotoneOn_hasDerivWithinAt
-- 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
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
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) a volume

Tactic:
have A : IntegrableOn (fun x ↦ f' x • g (f x)) a :=
      IntegrableOn.of_measure_zero (a_count.measure_zero volume)
-- 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
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 : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) a volume
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ 0) b volume

Tactic:
simp
-- 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
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 : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) a volume
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ 0) b volume

Tactic:
have : IntegrableOn (fun x ↦ (0 : F)) b := by simp