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
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume a) fun (x : ℝ) ↦ f' x • g (f x)) 0

Tactic:
have : ∫ x in a, f' x • g (f x) = 0 :=
      setIntegral_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
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
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume a) fun (x : ℝ) ↦ f' x • g (f x)) 0
rw :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (b ∪ c)) fun (x : ℝ) ↦ f' x • g (f 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 s) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))

Tactic:
rw [← h_union, setIntegral_union h_disj (hb.union hc) (H'.mono_set a_s) (H'.mono_set bc_s),
      this, zero_add]

Premises used: MeasureTheory.setIntegral_union, zero_add, MeasureTheory.IntegrableOn.mono_set, MeasurableSet.union
-- 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
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume a) fun (x : ℝ) ↦ f' x • g (f x)) 0
x : ℝ
hx : x ∈ b
⊢ f' x • g (f x) = 0

Tactic:
simp [deriv_b 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
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume a) fun (x : ℝ) ↦ f' x • g (f x)) 0
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume b) fun (x : ℝ) ↦ f' x • g (f x)) 0

Tactic:
have : ∫ x in b, f' x • g (f x) = 0 :=
      setIntegral_eq_zero_of_forall_eq_zero (fun x hx ↦ by simp [deriv_b 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
this_1 :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume a) fun (x : ℝ) ↦ f' x • g (f x)) 0
this :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume b) fun (x : ℝ) ↦ f' x • g (f x)) 0
rw :
  HAdd.hAdd (α := F) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume b) fun (x : ℝ) ↦ f' x • g (f x))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x)) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x)
rw₁ :
  HAdd.hAdd (α := F) 0
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x)) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x)
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (b ∪ c)) fun (x : ℝ) ↦ f' x • g (f x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume c) fun (x : ℝ) ↦ f' x • g (f x))

Tactic:
rw [setIntegral_union h_disj' hc (H'.mono_set b_s) (H'.mono_set c_s), this, zero_add]

Premises used: MeasureTheory.setIntegral_union, zero_add, MeasureTheory.IntegrableOn.mono_set
-- 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
⊢ 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))

Tactic:
have I : ∫ x in s, f' x • g (f x) = ∫ x in c, f' x • g (f x) := by
    have : ∫ x in a, f' x • g (f x) = 0 :=
      setIntegral_measure_zero _ (a_count.measure_zero volume)
    rw [← h_union, setIntegral_union h_disj (hb.union hc) (H'.mono_set a_s) (H'.mono_set bc_s),
      this, zero_add]
    have : ∫ x in b, f' x • g (f x) = 0 :=
      setIntegral_eq_zero_of_forall_eq_zero (fun x hx ↦ by simp [deriv_b x hx])
    rw [setIntegral_union h_disj' hc (H'.mono_set b_s) (H'.mono_set c_s), this, zero_add]
-- 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))
hst : f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c
⊢ 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)

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
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))
hst : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
⊢ f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c

Tactic:
rw [← h_union, image_union, image_union]

Premises used: Set.image_union
-- 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))
⊢ 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:
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))
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:
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))
⊢ 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:
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))
⊢ 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:
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))
⊢ 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:
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))
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:
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))
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:
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))
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:
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))
⊢ 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)

Tactic:
have J : ∫ x in f '' s, g x = ∫ x in f '' c, g x := by
    apply setIntegral_congr_set
    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