awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), (fun (q : ℕ) ↦ K (F q).1 (F q).2.1 (F q).2.2) n) x
have apply : x ∈ K (F q).1 (F q).2.1 (F q).2.2
Tactic: apply mem_iUnion.2 ⟨q, _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F_1 : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F_1
inst_4 : NormedSpace ℝ F_1
inst_5 : SecondCountableTopology F_1
f : E → F_1
s : Set E
f' : E → E →L[ℝ] F_1
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F_1) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F_1), r A ≠ 0
hs : s.Nonempty
T : Set (↑s : Type u_1)
T_count : T.Countable
hT :
  Eq (α := Set (E →L[ℝ] F_1)) (⋃ x ∈ T, ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
    (⋃ (x : (↑s : Type u_1)), ball (f' (↑x : E)) (↑(r (f' (↑x : E))) : ℝ))
u : ℕ → ℝ
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
M : ℕ → (↑T : Type u_1) → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) ↦
    {x : E |
      x ∈ s ∧
        ∀ y ∈ s ∩ ball x (u n),
          ‖HSub.hSub (β := F_1) (f y - f x) ((f' (↑(↑z : (↑s : Type u_1)) : E) : (a : E) → F_1) (y - x) : F_1)‖ ≤
            (↑(r (f' (↑(↑z : (↑s : Type u_1)) : E))) : ℝ) * ‖y - x‖}
s_subset : ∀ x ∈ s, ∃ (n : ℕ) (z : (↑T : Type u_1)), x ∈ M n z
closure_M_subset :
  ∀ (n : ℕ) (z : (↑T : Type u_1)), s ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ⊆ M n z
d : ℕ → E
hd : DenseRange d
K : ℕ → (↑T : Type u_1) → ℕ → Set E :=
  fun (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ) ↦
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z) ∩ closedBall (d p) (u n / 3)
K_approx :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ),
    ApproximatesLinearOn f (f' (↑(↑z : (↑s : Type u_1)) : E)) (s ∩ K n z p) (r (f' (↑(↑z : (↑s : Type u_1)) : E)))
K_closed :
  ∀ (n : ℕ) (z : (↑T : Type u_1)) (p : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K n z p)
F : ℕ → ℕ × (↑T : Type u_1) × ℕ
hF : Function.Surjective F
x : E
xs : x ∈ s
n : ℕ
z : (↑T : Type u_1)
hnz : x ∈ M n z
p : ℕ
hp : x ∈ closedBall (d p) (u n / 3)
q : ℕ
hq : F q = (n, z, p)
⊢ x ∈ K (F q).1 (F q).2.1 (F q).2.2
have simp : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (M n z)
Tactic: simp -zeta only [K, hq, mem_inter_iff, hp, and_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
have rcases : ∀ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F)
  (t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)) (st : s ⊆ ⋃ (n : ℕ), t n)
  (t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n)))
  (ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y),
  ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
Tactic: rcases exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' r rpos with
    ⟨t, A, t_closed, st, t_approx, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
have refine_1 : s ⊆ ⋃ (n : ℕ), disjointed t n
Tactic: refine
    ⟨disjointed t, A, disjoint_disjointed _,
      MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : SecondCountableTopology F
f : E → F
s : Set E
f' : E → E →L[ℝ] F
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
r : (E →L[ℝ] F) → ℝ≥0
rpos : ∀ (A : E →L[ℝ] F), r A ≠ 0
t : ℕ → Set E
A : ℕ → E →L[ℝ] F
t_closed : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (t n)
st : s ⊆ ⋃ (n : ℕ), t n
t_approx : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))
ht : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
refine_1 : s ⊆ ⋃ (n : ℕ), disjointed t n
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] F),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (r (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)
have refine_2 : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ disjointed t n) (r (A n))
Tactic: refine
    ⟨disjointed t, A, disjoint_disjointed _,
      MeasurableSet.disjointed fun n => (t_closed n).measurableSet, ?_, ?_, ht⟩
-- 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∞)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (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∞)
have a : Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
  {x : ℝ≥0 |
    (fun (δ : ℝ≥0) ↦
        ∀ (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∞))
      x}
Tactic: apply nhdsWithin_le_nhds
-- 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|
⊢ ∃ (ε : ℝ),
    (μ : (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∞) ∧
      0 < ε
have HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
Tactic: have HC : IsCompact (A '' closedBall 0 1) :=
      (ProperSpace.isCompact_closedBall _ _).image A.continuous
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
have apply : Tendsto (β := ℝ≥0∞)
  (fun (ε : ℝ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
  (𝓝 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
Tactic: apply Tendsto.mono_left _ nhdsWithin_le_nhds
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
⊢ ∃ (ε : ℝ),
    (μ : (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∞) ∧
      0 < ε
have L0 : Tendsto (β := ℝ≥0∞)
  (fun (ε : ℝ) ↦ ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
  (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
Tactic: have L0 :
      Tendsto (fun ε => μ (cthickening ε (A '' closedBall 0 1))) (𝓝[>] 0)
        (𝓝 (μ (A '' closedBall 0 1))) := by
      apply Tendsto.mono_left _ nhdsWithin_le_nhds
      exact tendsto_measure_cthickening_of_isCompact HC
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
have apply : EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
  (fun (ε : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
  fun (ε : ℝ) ↦
  (μ : (a : Set E) → ℝ≥0∞)
    (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)))
Tactic: apply L0.congr' _
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (ε : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    fun (ε : ℝ) ↦
    (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)))
have h : ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (Ioi 0) r),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (cthickening r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
Tactic: filter_upwards [self_mem_nhdsWithin] with r hr
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (cthickening r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 r)) :
    ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
    ℝ≥0∞)
Tactic: rw [← HC.add_closedBall_zero (le_of_lt hr), 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
h :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 r)) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (cthickening r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
    ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
    ℝ≥0∞)
Tactic: rw [← HC.add_closedBall_zero (le_of_lt hr), add_comm]
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
⊢ ∃ (ε : ℝ),
    (μ : (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∞) ∧
      0 < ε
have L1 : Tendsto (β := ℝ≥0∞)
  (fun (ε : ℝ) ↦
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞))
  (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
Tactic: have L1 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (μ (A '' closedBall 0 1))) := by
      apply L0.congr' _
      filter_upwards [self_mem_nhdsWithin] with r hr
      rw [← HC.add_closedBall_zero (le_of_lt hr), 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
⊢ Tendsto
    (fun (ε : ℝ) ↦
      (μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    (𝓝[>] 0) (𝓝 (HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
have h : HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
  (μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
Tactic: convert! L1
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
⊢ ∃ (ε : ℝ),
    (μ : (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∞) ∧
      0 < ε
have L2 : Tendsto
  (fun (ε : ℝ) ↦
    (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
  (𝓝[>] 0) (𝓝 (HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
Tactic: have L2 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (d * μ (closedBall 0 1))) := by
      convert! L1
      exact (addHaar_image_continuousLinearMap _ _ _).symm
-- 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L2 :
  Tendsto
    (fun (ε : ℝ) ↦
      (μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    (𝓝[>] 0) (𝓝 (HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
⊢ HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
have h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: gcongr