awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ |(f' x).det|) (μ.restrict s)

Tactic:
continuous_abs.measurable.comp_aemeasurable ?_

Premises used: abs, Continuous.measurable, Measurable.comp_aemeasurable, continuous_abs
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
refine : AEMeasurable (β := ℝ) (fun (x : E) ↦ (f' x).det) (μ.restrict s)
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ |(f' x).det|) (μ.restrict s)

Tactic:
refine continuous_abs.measurable.comp_aemeasurable ?_

Premises used: Continuous.measurable, Measurable.comp_aemeasurable, continuous_abs
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ (f' x).det) (μ.restrict s)

Tactic:
ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_

Premises used: ContinuousLinearMap.continuous_det, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
refine : AEMeasurable f' (μ.restrict s)
⊢ AEMeasurable (β := ℝ) (fun (x : E) ↦ (f' x).det) (μ.restrict s)

Tactic:
refine ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_

Premises used: ContinuousLinearMap.continuous_det, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
aemeasurable_fderivWithin μ hs hf'

Premises used: MeasureTheory.aemeasurable_fderivWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
exact aemeasurable_fderivWithin μ hs hf'

Premises used: MeasureTheory.aemeasurable_fderivWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
apply : AEMeasurable (β := ℝ) (fun (x : E) ↦ |(f' x).det|) (μ.restrict s)
⊢ AEMeasurable (β := ℝ≥0) (fun (x : E) ↦ |(f' x).det|.toNNReal) (μ.restrict s)

Tactic:
apply measurable_real_toNNReal.comp_aemeasurable

Premises used: measurable_real_toNNReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ MeasurableSet (f '' s)

Tactic:
haveI : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
  hs.image_of_continuousOn_injOn (DifferentiableOn.continuousOn this) hf

Premises used: DifferentiableOn.continuousOn, MeasurableSet.image_of_continuousOn_injOn, HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
rcases : ∀ (t : Set E) (ts : t ⊆ s) (ht : MeasurableSet t) (t_eq_s : t =ᶠ[ae μ] s), NullMeasurableSet (f '' s) μ
⊢ NullMeasurableSet (f '' s) μ

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ s = t ∪ s \ t

Tactic:
simp [union_eq_self_of_subset_left ts]

Premises used: Set.union_eq_self_of_subset_left
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ s = t ∪ s \ t

Tactic:
have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
rw : f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t
⊢ f '' s =ᶠ[ae μ] f '' t

Tactic:
rw [this, image_union]

Premises used: Set.image_union
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
⊢ f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t

Tactic:
union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)

Premises used: Iff.mpr, MeasureTheory.ae_eq_empty, MeasureTheory.union_ae_eq_left_of_ae_eq_empty
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
refine : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s \ t)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t

Tactic:
refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)

Premises used: Iff.mpr, MeasureTheory.ae_eq_empty, MeasureTheory.union_ae_eq_left_of_ae_eq_empty
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
apply : ∀ (x : E) (hx : x ∈ s \ t), DifferentiableWithinAt ℝ f (s \ t) x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s \ t)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _
      (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2

Premises used: MeasureTheory.ae_eq_set, And.right, Iff.mp, MeasureTheory.addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
x : E
hx : x ∈ s \ t
⊢ DifferentiableWithinAt ℝ f (s \ t) x

Tactic:
(hf' x hx.1).differentiableWithinAt.mono diff_subset

Premises used: Set.diff_subset, DifferentiableWithinAt.mono, And.left, HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
x : E
hx : x ∈ s \ t
⊢ DifferentiableWithinAt ℝ f (s \ t) x

Tactic:
exact (hf' x hx.1).differentiableWithinAt.mono diff_subset

Premises used: Set.diff_subset, DifferentiableWithinAt.mono, And.left, HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ f '' s =ᶠ[ae μ] f '' t

Tactic:
have A : f '' s =ᵐ[μ] f '' t := by
    have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]
    rw [this, image_union]
    refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)
    apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _
      (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2
    exact (hf' x hx.1).differentiableWithinAt.mono diff_subset
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : f '' s =ᶠ[ae μ] f '' t
apply : NullMeasurableSet (f '' t) μ
⊢ NullMeasurableSet (f '' s) μ

Tactic:
apply NullMeasurableSet.congr _ A.symm

Premises used: MeasureTheory.NullMeasurableSet.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : f '' s =ᶠ[ae μ] f '' t
h : MeasurableSet (f '' t)
⊢ NullMeasurableSet (f '' t) μ

Tactic:
apply MeasurableSet.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : f '' s =ᶠ[ae μ] f '' t
apply : ∀ x ∈ t, HasFDerivWithinAt f (f' x) t x
⊢ MeasurableSet (f '' t)

Tactic:
apply measurable_image_of_fderivWithin ht _ (hf.mono ts) (f' := f')

Premises used: MeasureTheory.measurable_image_of_fderivWithin, Set.InjOn.mono
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : f '' s =ᶠ[ae μ] f '' t
x : E
hx : x ∈ t
⊢ HasFDerivWithinAt f (f' x) t x

Tactic:
(hf' x (ts hx)).mono ts

Premises used: HasFDerivWithinAt.mono
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : f '' s =ᶠ[ae μ] f '' t
x : E
hx : x ∈ t
⊢ HasFDerivWithinAt f (f' x) t x

Tactic:
exact (hf' x (ts hx)).mono ts

Premises used: HasFDerivWithinAt.mono
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ MeasurableEmbedding (s.restrict (π := fun (a : E) ↦ E) f)

Tactic:
haveI : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
  this.continuousOn.measurableEmbedding hs hf

Premises used: DifferentiableOn.continuousOn, ContinuousOn.measurableEmbedding, HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
⊢ ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)

Tactic:
simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]

Premises used: lt_add_iff_pos_right, ENNReal.ofReal, ENNReal.coe_lt_coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
⊢ ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)

Tactic:
have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
rcases :
  ∀ (δ : ℝ≥0)
    (h :
      ∀ (s : Set E) (f : E → E),
        ApproximatesLinearOn f A s δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (δpos : 0 < δ),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
                HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δpos⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, MeasureTheory.addHaar_image_le_mul_of_det_lt, self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
⊢ ∃ (δ' : ℝ), 0 < δ' ∧ ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)

Tactic:
continuousAt_iff.1 ?_ ε εpos

Premises used: Iff.mp, Metric.continuousAt_iff, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
refine : ContinuousAt ContinuousLinearMap.det A
⊢ ∃ (δ' : ℝ), 0 < δ' ∧ ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)

Tactic:
refine continuousAt_iff.1 ?_ ε εpos

Premises used: Iff.mp, Metric.continuousAt_iff, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
⊢ ContinuousAt ContinuousLinearMap.det A

Tactic:
ContinuousLinearMap.continuous_det.continuousAt

Premises used: ContinuousLinearMap.continuous_det, Continuous.continuousAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
⊢ ContinuousAt ContinuousLinearMap.det A

Tactic:
exact ContinuousLinearMap.continuous_det.continuousAt

Premises used: ContinuousLinearMap.continuous_det, Continuous.continuousAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
obtain :
  ∀ (δ' : ℝ) (δ'pos : 0 < δ') (hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
                HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
obtain ⟨δ', δ'pos, hδ'⟩ : ∃ (δ' : ℝ), 0 < δ' ∧ ∀ B, dist B A < δ' → dist B.det A.det < ↑ε := by
      refine continuousAt_iff.1 ?_ ε εpos
      exact ContinuousLinearMap.continuous_det.continuousAt