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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K :
  f '' (s ∩ closedBall x r) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
this :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞) ≤
    ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞) ≤
  ENNReal.ofReal (r ^ finrank ℝ E) *
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
Tactic: rw [add_comm]
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K :
  f '' (s ∩ closedBall x r) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
this :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
⊢ ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have simp : ENNReal.ofReal (r ^ finrank ℝ E) *
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
  (↑m : ℝ≥0∞) *
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
Tactic: simp only [addHaar_closedBall' μ _ r0]
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K :
  f '' (s ∩ closedBall x r) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
this :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have μ₁ : (μ : (a : Set E) → ℝ≥0∞)
    ({f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
      ℝ≥0∞)
Tactic: calc
      μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=
        measure_mono K
      _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by
        simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]
      _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by
        rw [add_comm]; gcongr
      _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K :
  f '' (s ∩ closedBall x r) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
this :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
μ₁ :
  (μ : (a : Set E) → ℝ≥0∞)
      ({f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have μ₂ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
      ℝ≥0∞) ≤
  ENNReal.ofReal (r ^ finrank ℝ E) *
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
Tactic: calc
      μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=
        measure_mono K
      _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by
        simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]
      _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by
        rw [add_comm]; gcongr
      _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K :
  f '' (s ∩ closedBall x r) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
this :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
μ₁ :
  (μ : (a : Set E) → ℝ≥0∞)
      ({f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞)
μ₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞) ≤
    ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have μ₃ : ENNReal.ofReal (r ^ finrank ℝ E) *
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: calc
      μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=
        measure_mono K
      _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by
        simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]
      _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by
        rw [add_comm]; gcongr
      _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have I : ∀ (x : E) (r : ℝ),
  x ∈ s →
    0 ≤ r →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
Tactic: have I : ∀ x r, x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ m * μ (closedBall x r) := by
    intro x r xs r0
    have K : f '' (s ∩ closedBall x r) ⊆ A '' closedBall 0 r + closedBall (f x) (ε * r) := by
      rintro y ⟨z, ⟨zs, zr⟩, rfl⟩
      rw [mem_closedBall_iff_norm] at zr
      apply Set.mem_add.2 ⟨A (z - x), _, f z - f x - A (z - x) + f x, _, _⟩
      · apply mem_image_of_mem
        simpa only [dist_eq_norm, mem_closedBall, mem_closedBall_zero_iff, sub_zero] using zr
      · rw [mem_closedBall_iff_norm, add_sub_cancel_right]
        calc
          ‖f z - f x - A (z - x)‖ ≤ δ * ‖z - x‖ := hf _ zs _ xs
          _ ≤ ε * r := by gcongr
      · simp only [map_sub]
        abel
    have :
      A '' closedBall 0 r + closedBall (f x) (ε * r) =
        {f x} + r • (A '' closedBall 0 1 + closedBall 0 ε) := by
      rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
    rw [this] at K
    calc
      μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=
        measure_mono K
      _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by
        simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]
      _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by
        rw [add_comm]; gcongr
      _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
have h : ∀ (a : ℝ≥0∞) (ha : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) a),
  (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) a
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
have ha₁ : 0 < a
Tactic: rw [mem_Ioi] at ha
Cleared hypotheses: ha
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : 0 < a
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
have h : ∀ (t : Set E) (r : E → ℝ) (t_count : t.Countable) (ts : t ⊆ s) (rpos : ∀ x ∈ t, 0 < r x)
  (st : s ⊆ ⋃ x ∈ t, closedBall x (r x))
  (μt :
    ∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a),
  (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
Tactic: obtain ⟨t, r, t_count, ts, rpos, st, μt⟩ :
      ∃ (t : Set E) (r : E → ℝ),
        t.Countable ∧
          t ⊆ s ∧
            (∀ x : E, x ∈ t → 0 < r x) ∧
              (s ⊆ ⋃ x ∈ t, closedBall x (r x)) ∧
                (∑' x : ↥t, μ (closedBall (↑x) (r ↑x))) ≤ μ s + a :=
      Besicovitch.exists_closedBall_covering_tsum_measure_le μ ha.ne' (fun _ => Ioi 0) s
        fun x _ δ δpos => ⟨δ / 2, by simp [half_pos δpos, δpos]⟩
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : 0 < a
t : Set E
r : E → ℝ
t_count : t.Countable
ts : t ⊆ s
rpos : ∀ x ∈ t, 0 < r x
st : s ⊆ ⋃ x ∈ t, closedBall x (r x)
μt :
  ∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
have h : ∀ (this : Encodable (↑t : Type u_1)),
  (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
Tactic: haveI : Encodable t := t_count.toEncodable
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : 0 < a
t : Set E
r : E → ℝ
t_count : t.Countable
ts : t ⊆ s
rpos : ∀ x ∈ t, 0 < r x
st : s ⊆ ⋃ x ∈ t, closedBall x (r x)
μt :
  ∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
this : Encodable (↑t : Type u_1)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))) : ℝ≥0∞)
have rw : ∀ (st : s ⊆ ⋃ (x : (↑t : Type u_1)), closedBall (↑x : E) (r (↑x : E)))
  (μt :
    ∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a)
  (this : Encodable (↑t : Type u_1)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))) : ℝ≥0∞)
Tactic: rw [biUnion_eq_iUnion] at st
Cleared hypotheses: st, μt, 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : 0 < a
t : Set E
r : E → ℝ
t_count : t.Countable
ts : t ⊆ s
rpos : ∀ x ∈ t, 0 < r x
st : s ⊆ ⋃ (x : (↑t : Type u_1)), closedBall (↑x : E) (r (↑x : E))
μt :
  ∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
this : Encodable (↑t : Type u_1)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))) : ℝ≥0∞)
have h : f '' s ⊆ ⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))
Tactic: apply measure_mono