case a
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝[Ioi 0] 0, ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
apply nhdsWithin_le_nhds
case a.inl
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
hm : ↑0 < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑0 * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0

case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
case a
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
rcases eq_or_lt_of_le (zero_le m) with (rfl | mpos)
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
have hA : A.det ≠ 0 := by
  intro h; simp only [h, ENNReal.not_lt_zero, ENNReal.ofReal_zero, abs_zero] at hm
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
let B := A.toContinuousLinearEquivOfDetNeZero hA
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
have I : ENNReal.ofReal (|(B.symm : E →L[ℝ] E).det|) < (m⁻¹ : ℝ≥0) := by
  simp only [ENNReal.ofReal, abs_inv, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm,
    ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero, ENNReal.coe_lt_coe] at hm ⊢
  exact NNReal.inv_lt_inv mpos.ne' hm
case a.inr.intro.intro
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
case a.inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
obtain ⟨δ₀, δ₀pos, hδ₀⟩ :
  ∃ δ : ℝ≥0,
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t := by
  have :
    ∀ᶠ δ : ℝ≥0 in 𝓝[>] 0,
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t :=
    addHaar_image_le_mul_of_det_lt μ B.symm I
  rcases(this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩
  exact ⟨δ₀, h', h⟩
case h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
⊢ ∀ (a : ℝ≥0),
    Subsingleton E ∨
        a < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ →
      ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
              (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - a)⁻¹ *
            a <
          δ₀ →
        ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s a → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
case a.inr.intro.intro
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
filter_upwards [L1, L2]
case h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
case h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
⊢ ∀ (a : ℝ≥0),
    Subsingleton E ∨
        a < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ →
      ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
              (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - a)⁻¹ *
            a <
          δ₀ →
        ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s a → ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
intro δ h1δ h2δ s f hf
case h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
case h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
have hf' : ApproximatesLinearOn f (B : E →L[ℝ] E) s δ := by convert hf
case h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
case h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
let F := hf'.toLocalEquiv h1δ
case h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)

case H
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
⊢ ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
case h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
suffices H : μ (F.symm '' F.target) ≤ (m⁻¹ : ℝ≥0) * μ F.target
no goals
case H
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
⊢ ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
exact hδ₀ _ _ ((hf'.to_inv h1δ).mono_num h2δ.le)
case a.inl.hp
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
hm : ↑0 < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ ∀ (x : ℝ≥0) (s : Set E) (f : E → E), ApproximatesLinearOn f A s x → ↑0 * ↑↑μ s ≤ ↑↑μ (f '' s)
case a.inl
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
hm : ↑0 < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ {x | (fun δ => ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑0 * ↑↑μ s ≤ ↑↑μ (f '' s)) x} ∈ 𝓝 0
apply eventually_of_forall
no goals
case a.inl.hp
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
hm : ↑0 < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
⊢ ∀ (x : ℝ≥0) (s : Set E) (f : E → E), ApproximatesLinearOn f A s x → ↑0 * ↑↑μ s ≤ ↑↑μ (f '' s)
simp only [forall_const, MulZeroClass.zero_mul, imp_true_iff, zero_le, ENNReal.coe_zero]
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
h : ContinuousLinearMap.det A = 0
⊢ False
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
⊢ ContinuousLinearMap.det A ≠ 0
intro h
no goals
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
h : ContinuousLinearMap.det A = 0
⊢ False
simp only [h, ENNReal.not_lt_zero, ENNReal.ofReal_zero, abs_zero] at hm
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
hm : m < Real.toNNReal (abs (ContinuousLinearMap.det A))
⊢ (Real.toNNReal (abs (ContinuousLinearMap.det A)))⁻¹ < m⁻¹
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
⊢ ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
simp only [ENNReal.ofReal, abs_inv, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm,
  ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero, ENNReal.coe_lt_coe] at hm ⊢
no goals
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
hm : m < Real.toNNReal (abs (ContinuousLinearMap.det A))
⊢ (Real.toNNReal (abs (ContinuousLinearMap.det A)))⁻¹ < m⁻¹
exact NNReal.inv_lt_inv mpos.ne' hm
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[Ioi 0] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
have :
  ∀ᶠ δ : ℝ≥0 in 𝓝[>] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t :=
  addHaar_image_le_mul_of_det_lt μ B.symm I
case intro.intro
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[Ioi 0] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
δ₀ : ℝ≥0
h :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h' : 0 < δ₀
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[Ioi 0] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
rcases(this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩
no goals
case intro.intro
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[Ioi 0] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
δ₀ : ℝ≥0
h :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h' : 0 < δ₀
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
exact ⟨δ₀, h', h⟩
case pos
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹

case neg
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : ¬Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
by_cases Subsingleton E
case neg
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : ¬Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0,
    δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
case neg
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : ¬Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
simp only [h, false_or_iff]
case neg.h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : ¬Subsingleton E
⊢ 0 < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
case neg
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : ¬Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0,
    δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
apply Iio_mem_nhds
no goals
case neg.h
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : ¬Subsingleton E
⊢ 0 < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
simpa only [h, false_or_iff, inv_pos] using B.subsingleton_or_nnnorm_symm_pos
no goals
case pos
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
h : Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
simp only [h, true_or_iff, eventually_const]
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
this :
  Tendsto
    (fun δ =>
      ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
          (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
        δ)
    (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
this :
  Tendsto (fun δ => ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹ * 0))
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
simp only [MulZeroClass.mul_zero] at this
no goals
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
this :
  Tendsto
    (fun δ =>
      ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
          (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
        δ)
    (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
exact (tendsto_order.1 this).2 δ₀ δ₀pos
case inl
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ = 0
⊢ Tendsto (fun δ => ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹ * 0))

case inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ ≠ 0
⊢ Tendsto (fun δ => ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹ * 0))
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
⊢ Tendsto (fun δ => ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹ * 0))
rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
case inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ ≠ 0
⊢ Tendsto (fun δ => (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹)
case inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ ≠ 0
⊢ Tendsto (fun δ => ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹ * 0))
refine' Tendsto.mul (tendsto_const_nhds.mul _) tendsto_id
case inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ ≠ 0
⊢ ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0 ≠ 0
case inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ ≠ 0
⊢ Tendsto (fun δ => (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹)
refine' (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ _
no goals
case inr
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ ≠ 0
⊢ ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0 ≠ 0
simpa only [tsub_zero, inv_eq_zero, Ne.def] using H
no goals
case inl
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
H : ‖↑(ContinuousLinearEquiv.symm B)‖₊ = 0
⊢ Tendsto (fun δ => ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - 0)⁻¹ * 0))
simpa only [H, MulZeroClass.zero_mul] using tendsto_const_nhds
no goals
E : Type u_1
F : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ApproximatesLinearOn f (↑B) s δ
convert hf
case h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m * ↑↑μ F.source ≤ ↑↑μ F.target
case h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m * ↑↑μ s ≤ ↑↑μ (f '' s)
change (m : ℝ≥0∞) * μ F.source ≤ μ F.target
case h.h0
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m ≠ 0 ∨ ↑↑μ F.target ≠ 0

case h.ht
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m ≠ ⊤ ∨ ↑↑μ F.target ≠ ⊤
case h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m * ↑↑μ F.source ≤ ↑↑μ F.target
rwa [← F.symm_image_target_eq_source, mul_comm, ← ENNReal.le_div_iff_mul_le, div_eq_mul_inv,
  mul_comm, ← ENNReal.coe_inv mpos.ne']
case h.h0.h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m ≠ 0
case h.h0
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m ≠ 0 ∨ ↑↑μ F.target ≠ 0
apply Or.inl
no goals
case h.h0.h
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m ≠ 0
simpa only [ENNReal.coe_eq_zero, Ne.def] using mpos.ne'
no goals
case h.ht
E : Type u_1
F✝ : Type ?u.415283
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
s✝ : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
A : E →L[ℝ] E
m : ℝ≥0
hm : ↑m < ENNReal.ofReal (abs (ContinuousLinearMap.det A))
mpos : 0 < m
hA : ContinuousLinearMap.det A ≠ 0
B : E ≃L[ℝ] E := ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA
I : ENNReal.ofReal (abs (ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm B))) < ↑m⁻¹
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g (↑(ContinuousLinearEquiv.symm B)) t δ₀ → ↑↑μ (g '' t) ≤ ↑m⁻¹ * ↑↑μ t
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖↑(ContinuousLinearEquiv.symm B)‖₊ * (‖↑(ContinuousLinearEquiv.symm B)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ :
  Subsingleton E ∨ δ < ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹
h2δ :
  ‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊ *
        (‖↑(ContinuousLinearEquiv.symm (ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero A hA))‖₊⁻¹ - δ)⁻¹ *
      δ <
    δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B) s δ
F : LocalEquiv E E := ApproximatesLinearOn.toLocalEquiv hf' h1δ
H : ↑↑μ (↑(LocalEquiv.symm F) '' F.target) ≤ ↑m⁻¹ * ↑↑μ F.target
⊢ ↑m ≠ ⊤ ∨ ↑↑μ F.target ≠ ⊤
simp only [ENNReal.coe_ne_top, true_or_iff, Ne.def, not_false_iff]