awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + 1
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
Tactic: have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + 1
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rcases : ∀ (δ : ℝ≥0)
  (h :
    ∀ (s : Set E) (f : E → E),
      ApproximatesLinearOn f A s δ →
        (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
  (h' : 0 < δ),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have this : ∀ (A : E →L[ℝ] E),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have :
      ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧
        ∀ (t : Set E), ApproximatesLinearOn f A t δ →
          μ (f '' t) ≤ (Real.toNNReal |A.det| + 1 : ℝ≥0) * μ t := by
    intro A
    let m : ℝ≥0 := Real.toNNReal |A.det| + 1
    have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]
    rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
    exact ⟨δ, h', fun t ht => h t f 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  ∀ (A : E →L[ℝ] E),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t δ →
            (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have choose : ∀ (δ : (A : E →L[ℝ] E) → ℝ≥0)
  (hδ :
    ∀ (A : E →L[ℝ] E),
      0 < δ A ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t (δ A) →
            (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: choose δ hδ using this
Cleared hypotheses: 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
  Pairwise (Disjoint on t) →
    (∀ (n : ℕ), MeasurableSet (t n)) →
      ∀ (t_cover : s ⊆ ⋃ (n : ℕ), t n) (ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))),
        LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨t, A, _, _, t_cover, ht, -⟩ :
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
      Pairwise (Disjoint on t) ∧
        (∀ n : ℕ, MeasurableSet (t n)) ∧
          (s ⊆ ⋃ n : ℕ, t n) ∧
            (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧
              (s.Nonempty → ∀ n, ∃ y ∈ s, A n = fderivWithin ℝ f s y) :=
    exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s (fderivWithin ℝ f s)
      (fun x xs => (hf x xs).hasFDerivWithinAt) δ fun A => (hδ A).1.ne'
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
have h : f '' s ⊆ ⋃ (n : ℕ), f '' (s ∩ t n)
Tactic: apply measure_mono
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ f '' s ⊆ ⋃ (n : ℕ), f '' (s ∩ t n)
have h : f '' s ⊆ f '' (s ∩ ⋃ (i : ℕ), t i)
Tactic: rw [← image_iUnion, ← inter_iUnion]
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)))
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
have apply : ∀ (n : ℕ),
  (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞)
Tactic: apply ENNReal.tsum_le_tsum fun n => ?_
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞)
have a : ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
Tactic: apply (hδ (A n)).2
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
    (∑' (n : ℕ), (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) * 0)
have h : ∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: gcongr with n
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
Tactic: calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      apply measure_mono
      rw [← image_iUnion, ← inter_iUnion]
      exact Set.image_mono (subset_inter Subset.rfl t_cover)
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + 1 : ℝ≥0) * μ (s ∩ t n) := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply (hδ (A n)).2
      exact ht n
    _ ≤ ∑' n, ((Real.toNNReal |(A n).det| + 1 : ℝ≥0) : ℝ≥0∞) * 0 := by
      gcongr with n
      exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)
    _ = 0 := by simp only [tsum_zero, mul_zero]
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₂ : LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)))
  (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
Tactic: calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      apply measure_mono
      rw [← image_iUnion, ← inter_iUnion]
      exact Set.image_mono (subset_inter Subset.rfl t_cover)
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + 1 : ℝ≥0) * μ (s ∩ t n) := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply (hδ (A n)).2
      exact ht n
    _ ≤ ∑' n, ((Real.toNNReal |(A n).det| + 1 : ℝ≥0) : ℝ≥0∞) * 0 := by
      gcongr with n
      exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)
    _ = 0 := by simp only [tsum_zero, mul_zero]
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
μ₂ :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)))
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₃ : LE.le (α := ℝ≥0∞)
  (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
  (∑' (n : ℕ), (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) * 0)
Tactic: calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      apply measure_mono
      rw [← image_iUnion, ← inter_iUnion]
      exact Set.image_mono (subset_inter Subset.rfl t_cover)
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + 1 : ℝ≥0) * μ (s ∩ t n) := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply (hδ (A n)).2
      exact ht n
    _ ≤ ∑' n, ((Real.toNNReal |(A n).det| + 1 : ℝ≥0) : ℝ≥0∞) * 0 := by
      gcongr with n
      exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)
    _ = 0 := by simp only [tsum_zero, mul_zero]
-- 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
s : Set E
f : E → E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left : Pairwise (Disjoint on t)
left_1 : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
μ₂ :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)))
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
μ₃ :
  LE.le (α := ℝ≥0∞)
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
    (∑' (n : ℕ), (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) * 0)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₄ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (↑(|(A n).det|.toNNReal + 1) : ℝ≥0∞) * 0) 0
Tactic: calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      apply measure_mono
      rw [← image_iUnion, ← inter_iUnion]
      exact Set.image_mono (subset_inter Subset.rfl t_cover)
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + 1 : ℝ≥0) * μ (s ∩ t n) := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply (hδ (A n)).2
      exact ht n
    _ ≤ ∑' n, ((Real.toNNReal |(A n).det| + 1 : ℝ≥0) : ℝ≥0∞) * 0 := by
      gcongr with n
      exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)
    _ = 0 := by simp only [tsum_zero, mul_zero]
-- 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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have inl : ∀ (hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x)
  (hs : Subset.{u_1} (α := Set E) ∅ (closedBall 0 R))
  (h'f' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → (f' x).det = 0),
  (μ : (a : Set E) → ℝ≥0∞) (f '' ∅) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty s with (rfl | h's)
Cleared hypotheses: s, hf', hs, h'f'
-- 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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
inl :
  ∀ (hf' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt f (f' x) ∅ x)
    (hs : Subset.{u_1} (α := Set E) ∅ (closedBall 0 R))
    (h'f' : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → (f' x).det = 0),
    (μ : (a : Set E) → ℝ≥0∞) (f '' ∅) ≤
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have inr : ∀ (h's : s.Nonempty),
  (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
Tactic: rcases eq_empty_or_nonempty s with (rfl | h's)
-- 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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
Tactic: have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]
-- 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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rcases : ∀ (δ : ℝ≥0)
  (h :
    ∀ (s : Set E) (f : E → E),
      ApproximatesLinearOn f A s δ →
        (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
  (h' : 0 < δ),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩