awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
          (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rcases : ∀ (δ₀ : ℝ≥0)
  (h :
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
  (h' : 0 < δ₀),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
          (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rcases (this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s))
        x}
have a : ∀ (δ₀ : ℝ≥0) (δ₀pos : 0 < δ₀)
  (hδ₀ :
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)),
  Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s))
        x}
Tactic: 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
have pos : ∀ (h : Subsingleton E), ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
Tactic: by_cases h : Subsingleton E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
pos : ∀ (h : Subsingleton E), ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
have neg : ∀ (h : ¬Subsingleton E), ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
Tactic: by_cases h : Subsingleton E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
h : ¬Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
have neg : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
Tactic: simp only [h, false_or]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
h : ¬Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
have neg : 0 < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
Tactic: apply Iio_mem_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s))
        x}
have L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
Tactic: have L1 : ∀ᶠ δ in 𝓝 (0 : ℝ≥0), Subsingleton E ∨ δ < ‖(B.symm : E →L[ℝ] E)‖₊⁻¹ := by
    by_cases h : Subsingleton E
    · simp only [h, true_or, eventually_const]
    simp only [h, false_or]
    apply Iio_mem_nhds
    simpa only [h, false_or, inv_pos] using B.subsingleton_or_nnnorm_symm_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
have inl : ∀ (H : ‖(↑B.symm : E →L[ℝ] E)‖₊ = 0),
  Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
Tactic: rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
inl :
  ∀ (H : ‖(↑B.symm : E →L[ℝ] E)‖₊ = 0),
    Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
      (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
have inr : ∀ (H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0),
  Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
Tactic: rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
have inr : Tendsto (fun (δ : ℝ≥0) ↦ (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹)
Tactic: refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
⊢ Tendsto (fun (δ : ℝ≥0) ↦ (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹)
have inr : ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0 ≠ 0
Tactic: refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
have this : Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
  (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
Tactic: have :
      Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
        (𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) := by
      rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
      · simpa only [H, zero_mul] using tendsto_const_nhds
      refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
      refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
      simpa only [tsub_zero, inv_eq_zero, Ne] using 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
this :
  Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
have this₁ : Tendsto (β := ℝ≥0) (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0) (𝓝 0)
Tactic: simp only [mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s))
        x}
have L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
Tactic: have L2 :
    ∀ᶠ δ in 𝓝 (0 : ℝ≥0), ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀ := by
    have :
      Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
        (𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) := by
      rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
      · simpa only [H, zero_mul] using tendsto_const_nhds
      refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
      refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
      simpa only [tsub_zero, inv_eq_zero, Ne] using H
    simp only [mul_zero] at this
    exact (tendsto_order.1 this).2 δ₀ δ₀pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s))
        x}
have h : ∀ (a : ℝ≥0),
  Subsingleton E ∨ a < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ →
    ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - a)⁻¹ * a < δ₀ →
      ∀ (s : Set E) (f : E → E),
        ApproximatesLinearOn f A s a →
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
Tactic: filter_upwards [L1, L2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
Tactic: have hf' : ApproximatesLinearOn f (B : E →L[ℝ] E) s δ := by convert! hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have change : HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.source : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) F.target
Tactic: change (m : ℝ≥0∞) * μ F.source ≤ μ F.target
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.source : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) F.target
have h0 : (↑m : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: 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']