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
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
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
⊢ (μ : (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]⟩

Premises used: Set.Ioi, Besicovitch.exists_closedBall_covering_tsum_measure_le, HDiv.hDiv, LT.lt.ne', Exists.intro, OfNat.ofNat, DFunLike.coe, Set
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
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
⊢ (μ : (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
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
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∞)
⊢ 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

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
h : f '' s ⊆ ⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))
⊢ 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:
apply measure_mono

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
h : f '' s ⊆ f '' (s ∩ ⋃ (i : (↑t : Type u_1)), closedBall (↑i : E) (r (↑i : E)))
⊢ f '' s ⊆ ⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))

Tactic:
rw [← image_iUnion, ← inter_iUnion]

Premises used: Set.image_iUnion, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
⊢ f '' s ⊆ f '' (s ∩ ⋃ (i : (↑t : Type u_1)), closedBall (↑i : E) (r (↑i : E)))

Tactic:
Set.image_mono (subset_inter (Subset.refl _) st)

Premises used: Set.Subset.refl, Set.image_mono, Set.subset_inter
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
⊢ f '' s ⊆ f '' (s ∩ ⋃ (i : (↑t : Type u_1)), closedBall (↑i : E) (r (↑i : E)))

Tactic:
exact Set.image_mono (subset_inter (Subset.refl _) st)

Premises used: Set.Subset.refl, Set.image_mono, Set.subset_inter
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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∞) (⋃ (x : (↑t : Type u_1)), f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))) : ℝ≥0∞)
    (∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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∞) (∑' (x : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall (↑x : E) (r (↑x : E)))))
    (∑' (x : (↑t : Type u_1)),
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) : ℝ≥0∞))

Tactic:
(ENNReal.tsum_le_tsum fun x => I x (r x) (ts x.2) (rpos x x.2).le)

Premises used: ENNReal.tsum_le_tsum, LT.lt.le, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
rw :
  (↑m : ℝ≥0∞) * ∑' (i : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑i : E) (r (↑i : E))) ≤
    (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
⊢ ∑' (x : (↑t : Type u_1)),
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) : ℝ≥0∞) ≤
    (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a

Tactic:
rw [ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
⊢ (↑m : ℝ≥0∞) * ∑' (i : (↑t : Type u_1)), (μ : (a : Set E) → ℝ≥0∞) (closedBall (↑i : E) (r (↑i : E))) ≤
    (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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∞)
μ₂ :
  ∑' (x : (↑t : Type u_1)),
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall (↑x : E) (r (↑x : E))) : ℝ≥0∞) ≤
    (↑m : ℝ≥0∞) * 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:
calc
      μ (f '' s) ≤ μ (⋃ x : t, f '' (s ∩ closedBall x (r x))) := by
        rw [biUnion_eq_iUnion] at st
        apply measure_mono
        rw [← image_iUnion, ← inter_iUnion]
        exact Set.image_mono (subset_inter (Subset.refl _) st)
      _ ≤ ∑' x : t, μ (f '' (s ∩ closedBall x (r x))) := measure_iUnion_le _
      _ ≤ ∑' x : t, m * μ (closedBall x (r x)) :=
        (ENNReal.tsum_le_tsum fun x => I x (r x) (ts x.2) (rpos x x.2).le)
      _ ≤ m * (μ s + a) := by rw [ENNReal.tsum_mul_left]; gcongr

Premises used: Inter.inter, MeasureTheory.measure_iUnion_le, HAdd.hAdd, Set.image, Metric.closedBall, Subtype.val, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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

Tactic:
have J : ∀ᶠ a in 𝓝[>] (0 : ℝ≥0∞), μ (f '' s) ≤ m * (μ s + a) := by
    filter_upwards [self_mem_nhdsWithin] with a ha
    rw [mem_Ioi] at ha
    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]⟩
    haveI : Encodable t := t_count.toEncodable
    calc
      μ (f '' s) ≤ μ (⋃ x : t, f '' (s ∩ closedBall x (r x))) := by
        rw [biUnion_eq_iUnion] at st
        apply measure_mono
        rw [← image_iUnion, ← inter_iUnion]
        exact Set.image_mono (subset_inter (Subset.refl _) st)
      _ ≤ ∑' x : t, μ (f '' (s ∩ closedBall x (r x))) := measure_iUnion_le _
      _ ≤ ∑' x : t, m * μ (closedBall x (r x)) :=
        (ENNReal.tsum_le_tsum fun x => I x (r x) (ts x.2) (rpos x x.2).le)
      _ ≤ m * (μ s + a) := by rw [ENNReal.tsum_mul_left]; gcongr