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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
addHaar_image_le_lintegral_abs_det_fderiv_aux2 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) ≤ ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
apply
        addHaar_image_le_lintegral_abs_det_fderiv_aux2 μ (hs.inter (u_meas n)) _ fun x hx =>
          (hf' x hx.1).mono inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_aux2, And.left, HasFDerivWithinAt.mono, MeasurableSet.inter
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (u n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : μ (u n) < ∞ :=
        lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, ne_of_lt, Set.inter_subset_right
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, ne_of_lt, Set.inter_subset_right
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
rw : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
| ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
rw [A]
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
conv_rhs :
  ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
⊢ ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
conv_rhs => rw [A]
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
hm : ∀ (i : ℕ), MeasurableSet (s ∩ u i)
hd : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ u n)
⊢ ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
rw [lintegral_iUnion]

Premises used: MeasureTheory.lintegral_iUnion
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
⊢ MeasurableSet (s ∩ u n)

Tactic:
hs.inter (u_meas n)

Premises used: MeasurableSet.inter
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
⊢ MeasurableSet (s ∩ u n)

Tactic:
exact hs.inter (u_meas n)

Premises used: MeasurableSet.inter
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ u n)

Tactic:
pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

Premises used: pairwise_disjoint_mono, disjoint_disjointed, Set.inter_subset_right
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ u n)

Tactic:
exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

Premises used: pairwise_disjoint_mono, disjoint_disjointed, Set.inter_subset_right
-- 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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
μ₂ :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)))
    (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ)
μ₃ : ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
calc
    μ (f '' s) ≤ ∑' n, μ (f '' (s ∩ u n)) := by
      conv_lhs => rw [A, image_iUnion]
      exact measure_iUnion_le _
    _ ≤ ∑' n, ∫⁻ x in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply
        addHaar_image_le_lintegral_abs_det_fderiv_aux2 μ (hs.inter (u_meas n)) _ fun x hx =>
          (hf' x hx.1).mono inter_subset_left
      have : μ (u n) < ∞ :=
        lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)
      exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)
    _ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ := by
      conv_rhs => rw [A]
      rw [lintegral_iUnion]
      · intro n; exact hs.inter (u_meas n)
      · exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

Premises used: Set.image, DFunLike.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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
⊢ ∃ (δ' : ℝ), 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
⊢ 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
⊢ 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
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 δ →
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                  (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑δ'' : ℝ)
apply : dist B A < δ'
⊢ dist B.det A.det ≤ (↑ε : ℝ)

Tactic:
apply (hδ' B _).le

Premises used: LT.lt.le
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑δ'' : ℝ)
rw : ‖B - A‖ < δ'
⊢ dist B A < δ'

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑δ'' : ℝ)
⊢ ‖B - A‖ < δ'

Tactic:
hB.trans_lt (half_lt_self δ'pos)

Premises used: half_lt_self, LE.le.trans_lt
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑δ'' : ℝ)
⊢ ‖B - A‖ < δ'

Tactic:
exact hB.trans_lt (half_lt_self δ'pos)

Premises used: half_lt_self, LE.le.trans_lt
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
⊢ ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)

Tactic:
have I'' : ∀ B : E →L[ℝ] E, ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε := by
      intro B hB
      rw [← Real.dist_eq]
      apply (hδ' B _).le
      rw [dist_eq_norm]
      exact hB.trans_lt (half_lt_self δ'pos)
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
inl :
  ∀ (hA : A.det = 0),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                  (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
inr :
  ∀ (hA : A.det ≠ 0),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                  (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))

Tactic:
rcases eq_or_ne A.det 0 with (hA | hA)

Premises used: ContinuousLinearMap.det, eq_or_ne, OfNat.ofNat
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det = 0
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))

Tactic:
⟨δ'', half_pos δ'pos, I'', ?_⟩

Premises used: half_pos, And.intro, Exists.intro
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det = 0
inl :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g A t δ'' →
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
          (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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 δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))

Tactic:
refine ⟨δ'', half_pos δ'pos, I'', ?_⟩
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det = 0
⊢ ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g A t δ'' →
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
          (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))

Tactic:
simp only [hA, forall_const, zero_mul, ENNReal.ofReal_zero, imp_true_iff,
        zero_le, abs_zero]

Premises used: zero_le, MulZeroClass.zero_mul, imp_true_iff, abs_zero, ENNReal.ofReal_zero, forall_const