awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
u : ℝ → ℝ≥0∞
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A : ∫⁻ (x : ℝ) in e '' s, u (n x) = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
B : ∫⁻ (x : ℝ) in n ∘ e '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * (u ∘ n) (e x)
h : ∀ (x : ℝ) (hx : x ∈ s), f x = (n ∘ e) x
⊢ ∫⁻ (x : ℝ) in f '' s, u x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (-f' x) * u (f x)
have h₁ : ∀ (x : ℝ), u (f x) = (u ∘ n) (e x)
Tactic: convert! B using 4 with x hx x
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
⊢ 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
have hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
Tactic: have hg' (x) (hx : x ∈ s) : HasDerivWithinAt e (-f' x) s x := (hf' x hx).neg
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
have rw : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (g ∘ n) (e '' s) volume
Tactic: rw [← integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ 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
have A : IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
Tactic: have A : IntegrableOn (fun x ↦ g (n x)) (e '' s)
      ↔ IntegrableOn (fun x ↦ (-f' x) • (g ∘ n) (e x)) s := by
    rw [← integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]; rfl
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • g (f x)) s volume
have B : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ HSMul.hSMul (α := ℝ) |(-1)| (g (n x))) (e '' s) volume
Tactic: have B : IntegrableOn g (n '' e '' s) ↔ IntegrableOn (fun x ↦ (|-1| : ℝ) • g (n x)) (e '' s) :=
    integrableOn_image_iff_integrableOn_abs_deriv_smul (hs.image_of_monotoneOn hf.neg)
      (fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
B :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ HSMul.hSMul (α := ℝ) |(-1)| (g (n x))) (e '' s) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • g (f x)) s volume
have B₁ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume
Tactic: simp only [abs_neg, abs_one, one_smul] at B
Cleared hypotheses: B
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
B :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n '' e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • g (f x)) s volume
have B₁ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n ∘ e '' s) volume ↔
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
Tactic: rw [A, ← image_comp] at B
Cleared hypotheses: 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
B :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n ∘ e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e 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
have h : ∀ (x : ℝ) (hx : x ∈ s), f x = (n ∘ e) x
Tactic: convert! B using 3 with x hx x
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ g (n x)) (e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
B :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (n ∘ e '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x)) s volume
h : ∀ (x : ℝ) (hx : x ∈ s), f x = (n ∘ e) x
⊢ 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
have h₁ : ∀ (x : ℝ), -f' x • g (f x) = -f' x • (g ∘ n) (e x)
Tactic: convert! B using 3 with x hx x
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
⊢ 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 hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
Tactic: have hg' (x) (hx : x ∈ s) : HasDerivWithinAt e (-f' x) s x := (hf' x hx).neg
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
have rw : Eq.{u_1 + 1} (α := F)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ (g ∘ n) x)
Tactic: rw [← integral_image_eq_integral_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s 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 A : Eq.{u_1 + 1} (α := F)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
Tactic: have A : ∫ x in e '' s, g (n x) = ∫ x in s, (-f' x) • (g ∘ n) (e x) := by
    rw [← integral_image_eq_integral_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]; rfl
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e 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 B : Eq.{u_1 + 1} (α := F)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n '' e '' s)) fun (x : ℝ) ↦ g x)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦
    HSMul.hSMul (α := ℝ) |(-1)| (g (n x)))
Tactic: have B : ∫ x in n '' e '' s, g x = ∫ x in e '' s, (|-1| : ℝ) • g (n x) :=
    integral_image_eq_integral_abs_deriv_smul (hs.image_of_monotoneOn hf.neg)
      (fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
B :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n '' e '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦
      HSMul.hSMul (α := ℝ) |(-1)| (g (n 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 B₁ : Eq.{u_1 + 1} (α := F)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n '' e '' s)) fun (x : ℝ) ↦ g x)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
Tactic: simp only [abs_neg, abs_one, one_smul] at B
Cleared hypotheses: B
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
B :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n '' e '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n 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 B₁ : Eq.{u_1 + 1} (α := F)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n ∘ e '' s)) fun (x : ℝ) ↦ g x)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
Tactic: rw [A, ← image_comp] at B
Cleared hypotheses: 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
B :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n ∘ e '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e 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 h : f '' s = n ∘ e '' s
Tactic: convert! B using 3 with x hx x
-- 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 : AntitoneOn f s
g : ℝ → F
n : ℝ → ℝ := fun (x : ℝ) ↦ -x
e : ℝ → ℝ := n ∘ f
hg' : ∀ (x : ℝ) (hx : x ∈ s), HasDerivWithinAt e (-f' x) s x
A :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (e '' s)) fun (x : ℝ) ↦ g (n x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
B :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (n ∘ e '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ -f' x • (g ∘ n) (e x))
h : f '' s = n ∘ e '' 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 h₁ : ∀ (x : ℝ), -f' x • g (f x) = -f' x • (g ∘ n) (e x)
Tactic: convert! B using 3 with x hx x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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, f' x ≤ 0
hab : a ≤ b
⊢ AntitoneOn f (Icc a b)
have hf'₁ : DifferentiableOn ℝ f (interior (Icc a b))
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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, f' x ≤ 0
hab : a ≤ b
hf'₁ : DifferentiableOn ℝ f (interior (Icc a b))
⊢ AntitoneOn f (Icc a b)
have hf'_nonpos : ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
Tactic: apply antitoneOn_of_deriv_nonpos (convex_Icc a b) hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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, f' x ≤ 0
hab : a ≤ b
⊢ DifferentiableOn ℝ f (interior (Icc a b))
have hf'₁ : DifferentiableOn ℝ f (Ioo a b)
Tactic: rw [interior_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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, f' x ≤ 0
hab : a ≤ b
⊢ ∀ x ∈ interior (Icc a b), deriv f x ≤ 0
have hf'_nonpos : ∀ x ∈ Ioo a b, deriv f x ≤ 0
Tactic: rw [interior_Icc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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, f' x ≤ 0
hab : a ≤ b
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc a b)) fun (x : ℝ) ↦ f' x • g (f x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f b) (f a))) fun (u : ℝ) ↦ g u)
have M : AntitoneOn f (Icc a b)
Tactic: have M : AntitoneOn f (Icc a b) := by
    apply antitoneOn_of_deriv_nonpos (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc (f b) (f a))) fun (u : ℝ) ↦ g u)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' Ioo a b)) fun (u : ℝ) ↦ g u)
have hst : Icc (f b) (f a) =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
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
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, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ Icc (f b) (f a) =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
have hst : f '' Icc a b =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
Tactic: rw [← hf.image_Icc_of_antitoneOn hab M]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ f '' Icc a b =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
have hst : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' Icc a b \ f '' Ioo a b) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (hypothesis)
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, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' Icc a b \ f '' Ioo a b) : ℝ≥0∞) (0 : ℝ≥0∞)
have this : 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