awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ 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))
have 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)
Tactic: rw [setIntegral_union h_disj' hc (H'.mono_set b_s) (H'.mono_set c_s), this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ 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))
have 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)
Tactic: rw [setIntegral_union h_disj' hc (H'.mono_set b_s) (H'.mono_set c_s), this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ 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))
have 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))
Tactic: rw [setIntegral_union h_disj' hc (H'.mono_set b_s) (H'.mono_set c_s), this, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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 (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ f' x • g (f x))
have 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))
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
have hst : f '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c
Tactic: apply setIntegral_congr_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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 '' s =ᶠ[ae (F := Measure ℝ) volume] f '' c
have hst : f '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
Tactic: rw [← h_union, image_union, image_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
have refine : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' a) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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 '' c
have A : 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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 '' a ∪ (f '' b ∪ f '' c) =ᶠ[ae (F := Measure ℝ) volume] f '' c
have B : 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 _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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 s) fun (x : ℝ) ↦ f' x • g (f x))
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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)
⊢ 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))
have 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))
Tactic: rw [I, J]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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)
⊢ 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))
have hF' : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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))
have apply : ∀ (x : ℝ) (hx : x ∈ c), f' x • g (f x) = |(F' x).det| • g (f x)
Tactic: apply setIntegral_congr_fun hc (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ f' x • g (f x) = |(F' x).det| • g (f x)
have simp : f' x • g (f x) = |f' x| • g (f x)
Tactic: simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
      ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']