awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  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)
rw :
  Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (t : ℝ) ↦ f' t • g (f t))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦
        -f' x • g (f x))
hf'₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x
hf₁ : AntitoneOn f (Ioo 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)

Tactic:
rw [A, integral_Icc_eq_integral_Ioo,
    integral_image_eq_integral_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]

Premises used: MeasureTheory.integral_Icc_eq_integral_Ioo, MeasureTheory.integral_image_eq_integral_deriv_smul_of_antitoneOn, measurableSet_Ioo
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  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)
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (t : ℝ) ↦ f' t • g (f t))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦
        -f' x • g (f x))

Tactic:
simp [integral_neg]

Premises used: MeasureTheory.integral_neg
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  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)
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

Tactic:
fun z hz ↦ (hff' z hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  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)
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

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

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  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)
⊢ AntitoneOn f (Ioo a b)

Tactic:
M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, AntitoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  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)
⊢ AntitoneOn f (Ioo a b)

Tactic:
exact M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, AntitoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
hst : Icc (f b) (f a) =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume

Tactic:
apply integrableOn_congr_set_ae

Premises used: MeasureTheory.integrableOn_congr_set_ae
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume

Tactic:
have A : IntegrableOn g (Icc (f b) (f a)) ↔ IntegrableOn g (f '' (Ioo a b)) := by
    apply integrableOn_congr_set_ae
    rw [← hf.image_Icc_of_antitoneOn hab M]
    refine ae_eq_set.2 ⟨?_, by simp [show f '' Ioo a b \ f '' Icc a b = ∅ by grind]⟩
    have : f '' (Icc a b) \ f '' Ioo a b ⊆ {f a, f b} := by grind
    apply measure_mono_null this
    apply Finite.measure_zero (by simp)
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
rw :
  IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) (Ioo a b)
      volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • g (f x)) (Ioo a b)
      volume
hf'₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x
hf₁ : AntitoneOn f (Ioo a b)
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) (Icc a b)
      volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume

Tactic:
rw [A, integrableOn_Icc_iff_integrableOn_Ioo,
    integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]

Premises used: MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn, measurableSet_Ioo, integrableOn_Icc_iff_integrableOn_Ioo
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • g (f x)) (Ioo a b)
      volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' x • g (f x)) (Ioo a b)
      volume

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

Tactic:
fun z hz ↦ (hff' z hz).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x

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

Premises used: HasDerivAt.hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ AntitoneOn f (Ioo a b)

Tactic:
M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, AntitoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
M : AntitoneOn f (Icc a b)
A :
  IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
⊢ AntitoneOn f (Ioo a b)

Tactic:
exact M.mono Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, AntitoneOn.mono
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |det (toSpanSingleton ℝ (f' x))| * g (f x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ |f' x| * g (f x))
⊢ (Measure.comap f (withDensity volume fun (x : ℝ) ↦ ENNReal.ofReal (g x)) : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ |f' x| * g (f x))

Tactic:
rw [hf.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul volume hs
    hg hf_int hf']

Premises used: MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |det (toSpanSingleton ℝ (f' x))| * g (f x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ |f' x| * g (f x))

Tactic:
simp only [det_toSpanSingleton]

Premises used: ContinuousLinearMap.det_toSpanSingleton
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g ((⇑f : (a : ℝ) → ℝ) '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f : (a : ℝ) → ℝ) (f' x) s x
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |det (toSpanSingleton ℝ (f' x))| * g ((f : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |f' x| * g ((f : (a : ℝ) → ℝ) x))
⊢ (Measure.map (α := ℝ) (⇑f.symm : (a : ℝ) → ℝ) (withDensity volume fun (x : ℝ) ↦ ENNReal.ofReal (g x)) :
        (a : Set ℝ) → ℝ≥0∞)
      s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |f' x| * g ((f : (a : ℝ) → ℝ) x))

Tactic:
rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs
      f hg hf_int hf']

Premises used: MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g ((⇑f : (a : ℝ) → ℝ) '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f : (a : ℝ) → ℝ) (f' x) s x
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |det (toSpanSingleton ℝ (f' x))| * g ((f : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |f' x| * g ((f : (a : ℝ) → ℝ) x))

Tactic:
simp only [det_toSpanSingleton]

Premises used: ContinuousLinearMap.det_toSpanSingleton
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae (F := Measure ℝ) volume] g
hg_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
x : ℝ
hx : 0 x ≤ g x
⊢ x ∈ f '' s → 0 ≤ g x

Tactic:
fun _ ↦ hx
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae (F := Measure ℝ) volume] g
hg_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ g x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ f '' s → 0 ≤ g x) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (hx : 0 x ≤ g x), x ∈ f '' s → 0 ≤ g x
⊢ ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x

Tactic:
filter_upwards [hg] with x hx using fun _ ↦ hx
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f : (a : ℝ) → ℝ) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae (F := Measure ℝ) volume] g
hg_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
x : ℝ
hx : 0 x ≤ g x
⊢ Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x

Tactic:
fun _ ↦ hx
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f : (a : ℝ) → ℝ) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae (F := Measure ℝ) volume] g
hg_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ g x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (hx : 0 x ≤ g x), Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x
⊢ ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x

Tactic:
filter_upwards [hg] with x hx using fun _ ↦ hx
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f : (a : ℝ) → ℝ) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae (F := Measure ℝ) volume] g
hg_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |det (toSpanSingleton ℝ (f' x))| * g ((f : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |f' x| * g ((f : (a : ℝ) → ℝ) x))
⊢ (Measure.map (α := ℝ) (⇑f.symm : (a : ℝ) → ℝ) (withDensity volume fun (x : ℝ) ↦ ENNReal.ofReal (g x)) :
        (a : Set ℝ) → ℝ≥0∞)
      s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |f' x| * g ((f : (a : ℝ) → ℝ) x))

Tactic:
rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs
      f (by filter_upwards [hg] with x hx using fun _ ↦ hx) hg_int.integrableOn
      (fun x _ => (hf' x).hasDerivWithinAt)]

Premises used: HasDerivAt.hasDerivWithinAt, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f : (a : ℝ) → ℝ) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae (F := Measure ℝ) volume] g
hg_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |det (toSpanSingleton ℝ (f' x))| * g ((f : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦
        |f' x| * g ((f : (a : ℝ) → ℝ) x))

Tactic:
simp only [det_toSpanSingleton]

Premises used: ContinuousLinearMap.det_toSpanSingleton
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : (↑(mk f hf) : α → ε) =ᶠ[ae μ] f
⊢ MeasureTheory.Integrable (↑(mk f hf) : α → ε) μ ↔ MeasureTheory.Integrable f μ

Tactic:
apply integrable_congr

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
⊢ (↑(mk f hf) : α → ε) =ᶠ[ae μ] f

Tactic:
coeFn_mk f hf

Premises used: MeasureTheory.AEEqFun.coeFn_mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
⊢ (↑(mk f hf) : α → ε) =ᶠ[ae μ] f

Tactic:
exact coeFn_mk f hf

Premises used: MeasureTheory.AEEqFun.coeFn_mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α →ₘ[μ] ε
rw : (mk (↑f : α → ε) ⋯).Integrable ↔ f.Integrable
rw₁ rw₂ : f.Integrable ↔ f.Integrable
⊢ MeasureTheory.Integrable (↑f : α → ε) μ ↔ f.Integrable

Tactic:
rw [← integrable_mk f.aestronglyMeasurable, mk_coeFn]

Premises used: MeasureTheory.AEEqFun.integrable_mk, MeasureTheory.AEEqFun.mk_coeFn, MeasureTheory.AEEqFun.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
ε' : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
⊢ Integrable.{u_1, u_4} (α := α) (ε := ε') (m := m) (μ := μ) 0

Tactic:
(MeasureTheory.integrable_zero α ε' μ).congr (coeFn_mk _ _).symm

Premises used: MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.integrable_zero, MeasureTheory.Integrable.congr, MeasureTheory.AEEqFun.Integrable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ f.Integrable → (-f).Integrable

Tactic:
induction_on f fun _f hfm hfi => (integrable_mk _).2 ((integrable_mk hfm).1 hfi).neg

Premises used: MeasureTheory.AEEqFun.induction_on
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α →ₘ[μ] β
rw : MeasureTheory.Integrable (↑f : α → β) μ ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
rw₁ : MemLp (↑f : α → β) 1 μ ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
rw₂ rw₃ : MemLp (↑f : α → β) 1 μ ↔ MemLp (↑f : α → β) 1 μ
⊢ f.Integrable ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f

Tactic:
rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]

Premises used: MeasureTheory.AEEqFun.integrable_coeFn, MeasureTheory.Lp.mem_Lp_iff_memLp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α →ₘ[μ] β
⊢ f.Integrable → g.Integrable → (f + g).Integrable

Tactic:
induction_on₂ f g fun f hf g hg hfi hgi => ?_

Premises used: MeasureTheory.AEEqFun.induction_on₂
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α →ₘ[μ] β
refine :
  ∀ (f : α → β) (hf : AEStronglyMeasurable f μ) (g : α → β) (hg : AEStronglyMeasurable g μ) (hfi : (mk f hf).Integrable)
    (hgi : (mk g hg).Integrable), (mk f hf + mk g hg).Integrable
⊢ f.Integrable → g.Integrable → (f + g).Integrable

Tactic:
refine induction_on₂ f g fun f hf g hg hfi hgi => ?_
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f_1 g_1 : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : (mk f hf).Integrable
hgi : (mk g hg).Integrable
simp : ∀ (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.Integrable g μ), MeasureTheory.Integrable (f + g) μ
⊢ (mk f hf + mk g hg).Integrable

Tactic:
simp only [integrable_mk, mk_add_mk] at hfi hgi ⊢

Premises used: MeasureTheory.AEEqFun.integrable_mk, MeasureTheory.AEEqFun.mk_add_mk
-- Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f_1 g_1 : α →ₘ[μ] β
f : α → β
hf : AEStronglyMeasurable f μ
g : α → β
hg : AEStronglyMeasurable g μ
hfi : MeasureTheory.Integrable f μ
hgi : MeasureTheory.Integrable g μ
⊢ MeasureTheory.Integrable (f + g) μ

Tactic:
hfi.add hgi

Premises used: MeasureTheory.Integrable.add