-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero (hf : DifferentiableOn ℝ f s)
    (hs : μ s = 0) : μ (f '' s) = 0

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ f '' s ⊆ f '' (s ∩ ⋃ i, t i)

Tactic:
exact image_subset f (subset_inter Subset.rfl t_cover)

Result:
no goals

Proof state:
case a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))

Tactic:
exact ht n

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (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))

Tactic:
apply measure_mono

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (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)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
this :
  ∀ (A : E →L[ℝ] E),
    ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
⊢ μ (f '' s) ≤ 0

Tactic:
choose δ hδ using this

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
⊢ μ (f '' s) ≤ 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
⊢ μ (f '' s) ≤ 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⟩

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
this :
  ∀ (A : E →L[ℝ] E),
    ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
⊢ μ (f '' s) ≤ 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
A : E →L[ℝ] E
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t

Tactic:
let m : ℝ≥0 := Real.toNNReal |A.det| + 1

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + 1
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + 1
I : ENNReal.ofReal |A.det| < ↑m
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t

Tactic:
rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩

Result:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + 1
I : ENNReal.ofReal |A.det| < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s
h' : 0 < δ
⊢ ∃ δ, 0 < δ ∧ ∀ (t : Set E), ApproximatesLinearOn f A t δ → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : DifferentiableOn ℝ f s
hs : μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + 1) * μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ n, t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ μ (s ∩ t n) ≤ 0

Tactic:
exact le_trans (measure_mono inter_subset_left) (le_of_eq hs)

Result:
no goals