awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
hF : F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
A :
  Measure.map F
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
⊢ F = s.restrict (π := fun (a : E) ↦ E) f
have h : ∀ (x : (↑s : Type u_1)), F x = s.restrict (π := fun (a : E) ↦ E) f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
hF : F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
A :
  Measure.map F
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
⊢ Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have this : F = s.restrict (π := fun (a : E) ↦ E) f
Tactic: have : F = s.restrict f := by
    ext x
    exact uf x.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
hF : F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
A :
  Measure.map F
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
this : F = s.restrict (π := fun (a : E) ↦ E) f
⊢ Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have rwa : ∀
  (A :
    Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
        (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
          (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
      μ.restrict (f '' s))
  (this : F = s.restrict (π := fun (a : E) ↦ E) f),
  Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
Tactic: rwa [this] at A
Cleared hypotheses: A, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → ℝ≥0∞
⊢ ∫⁻ (x : E) in f '' s, g x ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
have rw : ∫⁻ (a : (↑s : Type u_1)),
    g
      (s.restrict (π := fun (a : E) ↦ E) f
        a) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
Tactic: rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).lintegral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → ℝ≥0∞
⊢ ∫⁻ (a : (↑s : Type u_1)),
      g
        (s.restrict (π := fun (a : E) ↦ E) f
          a) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
have simp : ∫⁻ (a : (↑s : Type u_1)),
    (g ∘ f)
      (↑a :
        E) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
Tactic: simp only [Set.restrict_apply, ← Function.comp_apply (f := g)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → ℝ≥0∞
⊢ ∫⁻ (a : (↑s : Type u_1)),
      (g ∘ f)
        (↑a :
          E) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
have rw : ∫⁻ (a : E) in s, HMul.hMul (α := E → ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (g ∘ f) a ∂μ =
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs,
    setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → ℝ≥0∞
rw :
  ∫⁻ (a : E) in s, HMul.hMul (α := E → ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (g ∘ f) a ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
⊢ ∫⁻ (a : (↑s : Type u_1)),
      (g ∘ f)
        (↑a :
          E) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
have rw₁ : ∀ᵐ (x : E) ∂μ.restrict s, ENNReal.ofReal |(f' x).det| < ∞
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs,
    setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → ℝ≥0∞
rw :
  ∫⁻ (a : E) in s, HMul.hMul (α := E → ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (g ∘ f) a ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
rw₁ : ∀ᵐ (x : E) ∂μ.restrict s, ENNReal.ofReal |(f' x).det| < ∞
⊢ ∫⁻ (a : (↑s : Type u_1)),
      (g ∘ f)
        (↑a :
          E) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
have rw₂ : AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (μ.restrict s)
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs,
    setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ IntegrableOn g (f '' s) μ ↔ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
have rw : @Integrable _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s)) (g ∘ s.restrict (π := fun (a : E) ↦ E) f)
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) ↔
  IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
Tactic: rw [IntegrableOn, ← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).integrable_map_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ @Integrable _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s)) (g ∘ s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
have simp : @Integrable _ _ _ (↑s : Type u_1) (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
    ((g ∘ f) ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s))
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞))) ↔
  IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
Tactic: simp only [Set.restrict_eq, ← Function.comp_assoc, ENNReal.ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ @Integrable _ _ _ (↑s : Type u_1) (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      ((g ∘ f) ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞))) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
have rw : Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
  IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs,
    restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
rw :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
⊢ @Integrable _ _ _ (↑s : Type u_1) (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      ((g ∘ f) ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞))) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
have hf₁ : AEMeasurable (β := ℝ≥0) (fun (x : E) ↦ |(f' x).det|.toNNReal) (μ.restrict s)
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs,
    restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
have simp_rw : Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) (μ.restrict s)
Tactic: simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
simp_rw :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) (μ.restrict s)
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
have simp_rw₁ : Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • (g ∘ f) x) (μ.restrict s) ↔
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) (μ.restrict s)
Tactic: simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in f '' s, g x ∂μ) (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ)
have rw : Eq.{u_2 + 1} (α := F)
  (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|))
    fun (x : (↑s : Type u_1)) ↦ g (s.restrict (π := fun (a : E) ↦ E) f x))
  (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ)
Tactic: rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).integral_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|))
      fun (x : (↑s : Type u_1)) ↦ g (s.restrict (π := fun (a : E) ↦ E) f x))
    (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ)
have simp : Eq.{u_2 + 1} (α := F)
  (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞)))
    fun (x : (↑s : Type u_1)) ↦ (g ∘ f) (↑x : E))
  (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)
Tactic: simp only [Set.restrict_apply, ← Function.comp_apply (f := g), ENNReal.ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞)))
      fun (x : (↑s : Type u_1)) ↦ (g ∘ f) (↑x : E))
    (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)
have rw : Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, |(f' x).det|.toNNReal • (g ∘ f) x ∂μ)
  (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)
Tactic: rw [← (MeasurableEmbedding.subtype_coe hs).integral_map, map_comap_subtype_coe hs,
    setIntegral_withDensity_eq_setIntegral_smul₀
      (aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf') _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, |(f' x).det|.toNNReal • (g ∘ f) x ∂μ)
    (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)
have e_f : ∀ (x : E), |(f' x).det|.toNNReal • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
x : E
⊢ |(f' x).det|.toNNReal • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
have e_f : (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
Tactic: rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
x : E
e_f : (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
⊢ |(f' x).det|.toNNReal • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
have e_f₁ : |(f' x).det| • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
Tactic: rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in f.target, g x ∂μ) (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)
have this : (↑f : E → E) '' f.source = f.target
Tactic: have : f '' f.source = f.target := PartialEquiv.image_source_eq_target f.toPartialEquiv
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
this : (↑f : E → E) '' f.source = f.target
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in f.target, g x ∂μ) (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)
have rw : Eq.{u_2 + 1} (α := F) (∫ (x : E) in (↑f : E → E) '' f.source, g x ∂μ)
  (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
this : (↑f : E → E) '' f.source = f.target
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in (↑f : E → E) '' f.source, g x ∂μ)
    (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)
have apply : ∀ x ∈ f.source, HasFDerivWithinAt (↑f : E → E) (f' x) f.source x
Tactic: apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurableSet _ f.injOn