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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑δ'' : ℝ)
⊢ dist B A < δ'
have rw : ‖B - A‖ < δ'
Tactic: rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
Tactic: have I'' : ∀ B : E →L[ℝ] E, ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε := by
      intro B hB
      rw [← Real.dist_eq]
      apply (hδ' B _).le
      rw [dist_eq_norm]
      exact hB.trans_lt (half_lt_self δ'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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inl : ∀ (hA : A.det = 0),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: rcases eq_or_ne A.det 0 with (hA | hA)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
inl :
  ∀ (hA : A.det = 0),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                  (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr : ∀ (hA : A.det ≠ 0),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: rcases eq_or_ne A.det 0 with (hA | hA)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det = 0
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inl : ∀ (t : Set E) (g : E → E),
  ApproximatesLinearOn g A t δ'' →
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: refine ⟨δ'', half_pos δ'pos, I'', ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
⊢ (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
have simp : (↑|A.det|.toNNReal : ℝ≥0∞) - (↑ε : ℝ≥0∞) < (↑|A.det|.toNNReal : ℝ≥0∞)
Tactic: simp only [m, ENNReal.ofReal, ENNReal.coe_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
⊢ (↑|A.det|.toNNReal : ℝ≥0∞) - (↑ε : ℝ≥0∞) < (↑|A.det|.toNNReal : ℝ≥0∞)
have ha₀ : (↑|A.det|.toNNReal : ℝ≥0∞) ≠ 0
Tactic: apply ENNReal.sub_lt_self ENNReal.coe_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
ha₀ : (↑|A.det|.toNNReal : ℝ≥0∞) ≠ 0
⊢ (↑|A.det|.toNNReal : ℝ≥0∞) - (↑ε : ℝ≥0∞) < (↑|A.det|.toNNReal : ℝ≥0∞)
have hb : (↑ε : ℝ≥0∞) ≠ 0
Tactic: apply ENNReal.sub_lt_self ENNReal.coe_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
Tactic: have I : (m : ℝ≥0∞) < ENNReal.ofReal |A.det| := by
      simp only [m, ENNReal.ofReal, ENNReal.coe_sub]
      apply ENNReal.sub_lt_self ENNReal.coe_ne_top
      · simpa only [abs_nonpos_iff, Real.toNNReal_eq_zero, ENNReal.coe_eq_zero, Ne] using hA
      · simp only [εpos.ne', ENNReal.coe_eq_zero, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr : ∀ (δ : ℝ≥0)
  (h :
    ∀ (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))
  (δpos : 0 < δ),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: rcases ((mul_le_addHaar_image_of_lt_det μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δ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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (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)
δpos : 0 < δ
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(min δ δ'') : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
Tactic: refine ⟨min δ δ'', lt_min δpos (half_pos δ'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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (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)
δpos : 0 < δ
inr : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(min δ δ'') : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr₁ : ∀ (t : Set E) (g : E → E),
  ApproximatesLinearOn g A t (min δ δ'') →
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: refine ⟨min δ δ'', lt_min δpos (half_pos δ'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
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (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)
δpos : 0 < δ
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
⊢ |B.det - A.det| ≤ (↑ε : ℝ)
have apply : (↑(min δ δ'') : ℝ) ≤ (↑δ'' : ℝ)
Tactic: apply I'' _ (hB.trans _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (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)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr : ∀ (ht : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: rcases eq_or_ne (μ t) ∞ with (ht | ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (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)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
inr :
  ∀ (ht : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr₁ : ∀ (ht : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: rcases eq_or_ne (μ t) ∞ with (ht | ht)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (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)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have this : HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (g '' t)
Tactic: have := h t g (htg.mono_num (min_le_left _ _))