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
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)
this : f '' Icc a b \ f '' Ioo a b ⊆ {f a, f b}
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (f '' Icc a b \ f '' Ioo a b) : ℝ≥0∞) (0 : ℝ≥0∞)
have hst : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {f a, f b} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply measure_mono_null this
-- 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.{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 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)
Tactic: have A : ∫ u in Icc (f b) (f a), g u = ∫ u in f '' (Ioo a b), g u := by
    apply setIntegral_congr_set
    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)
-- 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)
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 (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 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))
Tactic: rw [A, integral_Icc_eq_integral_Ioo,
    integral_image_eq_integral_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]
-- 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)
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))
⊢ 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 hf'₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x
Tactic: rw [A, integral_Icc_eq_integral_Ioo,
    integral_image_eq_integral_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]
-- 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)
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
⊢ 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 hf₁ : AntitoneOn f (Ioo a b)
Tactic: rw [A, integral_Icc_eq_integral_Ioo,
    integral_image_eq_integral_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]
-- 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
⊢ 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
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)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ioo a b) volume
have hst : Icc (f b) (f a) =ᶠ[ae (F := Measure ℝ) volume] f '' Ioo a b
Tactic: apply integrableOn_congr_set_ae
-- 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)
⊢ 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
have A : 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)
-- 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)
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)) (Icc a b)
      volume ↔
    IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Icc (f b) (f a)) volume
have 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
Tactic: rw [A, integrableOn_Icc_iff_integrableOn_Ioo,
    integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]
-- 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)
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
⊢ 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
have hf'₁ : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioo a b) x
Tactic: rw [A, integrableOn_Icc_iff_integrableOn_Ioo,
    integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]
-- 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)
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
⊢ 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
have hf₁ : AntitoneOn f (Ioo a b)
Tactic: rw [A, integrableOn_Icc_iff_integrableOn_Ioo,
    integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn measurableSet_Ioo (f' := f')]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ (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))
have 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))
Tactic: rw [hf.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul volume hs
    hg hf_int hf']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ (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))
have 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))
Tactic: rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs
      f hg hf_int hf']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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 : ℝ), x ∈ f '' s → 0 ≤ g x
have 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
Tactic: filter_upwards [hg] with x hx using fun _ ↦ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x
have h₁ : ∀ (a : ℝ), 0 a ≤ g a → a ∈ f '' s → 0 ≤ g a
Tactic: filter_upwards [hg] with x hx using fun _ ↦ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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 : ℝ), Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x
have 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
Tactic: filter_upwards [hg] with x hx using fun _ ↦ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ ∀ᵐ (x : ℝ), Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) x → 0 ≤ g x
have h₁ : ∀ (a : ℝ), 0 a ≤ g a → Membership.mem (γ := Set ℝ) ((⇑f : (a : ℝ) → ℝ) '' s) a → 0 ≤ g a
Tactic: filter_upwards [hg] with x hx using fun _ ↦ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.JacobianOneDim (goal)
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
⊢ (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))
have 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))
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
⊢ MeasureTheory.Integrable (↑(mk f hf) : α → ε) μ ↔ MeasureTheory.Integrable f μ
have h : (↑(mk f hf) : α → ε) =ᶠ[ae μ] f
Tactic: apply integrable_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α →ₘ[μ] ε
⊢ MeasureTheory.Integrable (↑f : α → ε) μ ↔ f.Integrable
have rw : (mk (↑f : α → ε) sorry).Integrable ↔ f.Integrable
Tactic: rw [← integrable_mk f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
ε : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α →ₘ[μ] ε
rw : (mk (↑f : α → ε) ⋯).Integrable ↔ f.Integrable
⊢ MeasureTheory.Integrable (↑f : α → ε) μ ↔ f.Integrable
have rw₁ : f.Integrable ↔ f.Integrable
Tactic: rw [← integrable_mk f.aestronglyMeasurable, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ f.Integrable ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
have rw : MeasureTheory.Integrable (↑f : α → β) μ ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
Tactic: rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α →ₘ[μ] β
rw : MeasureTheory.Integrable (↑f : α → β) μ ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
⊢ f.Integrable ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
have rw₁ : MemLp (↑f : α → β) 1 μ ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
Tactic: rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
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
⊢ f.Integrable ↔ Membership.mem (γ := AddSubgroup (α →ₘ[μ] β)) (Lp β 1 μ) f
have rw₂ : MemLp (↑f : α → β) 1 μ ↔ MemLp (↑f : α → β) 1 μ
Tactic: rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : α →ₘ[μ] β
⊢ f.Integrable → g.Integrable → (f + g).Integrable
have 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
Tactic: refine induction_on₂ f g fun f hf g hg hfi hgi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
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
⊢ (mk f hf + mk g hg).Integrable
have simp : ∀ (hfi : MeasureTheory.Integrable f μ) (hgi : MeasureTheory.Integrable g μ), MeasureTheory.Integrable (f + g) μ
Tactic: simp only [integrable_mk, mk_add_mk] at hfi hgi ⊢
Cleared hypotheses: hfi, hgi
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ Integrable (↑(↑f : α →ₘ[μ] β) : α → β) μ
have rw : MemLp (↑(↑f : α →ₘ[μ] β) : α → β) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ edist f g = ∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ
have simp : (if Eq (α := ℝ≥0∞) 1 ∞ then eLpNormEssSup ((↑(↑f : α →ₘ[μ] β) : α → β) - (↑(↑g : α →ₘ[μ] β) : α → β)) μ
  else ∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) a - (↑(↑g : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ) =
  ∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ
Tactic: simp only [Lp.edist_def, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm, Pi.sub_apply,
    toReal_one, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ dist f g = (∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ).toReal
have simp_rw : (edist f g).toReal = (∫⁻ (a : α), edist ((↑(↑f : α →ₘ[μ] β) : α → β) a) ((↑(↑g : α →ₘ[μ] β) : α → β) a) ∂μ).toReal
Tactic: simp_rw [dist_edist, edist_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ ‖f - g‖ = (∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ).toReal
have rw : (∫⁻ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] β) : α → β) a‖ₑ ∂μ).toReal =
  (∫⁻ (x : α), ‖(↑(↑f : α →ₘ[μ] β) : α → β) x - (↑(↑g : α →ₘ[μ] β) : α → β) x‖ₑ ∂μ).toReal
Tactic: rw [norm_def]