awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
H : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) : ℝ≥0∞) (0 : ℝ≥0∞)
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' ⋃ (n : ℕ), s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 (↑n : ℝ))) : ℝ≥0∞)
μ₂ : LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 (↑n : ℝ)))) 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' ⋃ (n : ℕ), s ∩ closedBall 0 (↑n : ℝ)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
calc
      μ (f '' ⋃ n : ℕ, s ∩ closedBall 0 n) ≤ ∑' n : ℕ, μ (f '' (s ∩ closedBall 0 n)) := by
        rw [image_iUnion]; exact measure_iUnion_le _
      _ ≤ 0 := by simp only [H, tsum_zero, nonpos_iff_eq_zero]

Premises used: Nat.cast, Inter.inter, Set.image, Metric.closedBall, OfNat.ofNat, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
suffices : ∀ (R : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
suffices H : ∀ R, μ (f '' (s ∩ closedBall 0 R)) = 0 by
    rw [← nonpos_iff_eq_zero, ← iUnion_inter_closedBall_nat s 0]
    calc
      μ (f '' ⋃ n : ℕ, s ∩ closedBall 0 n) ≤ ∑' n : ℕ, μ (f '' (s ∩ closedBall 0 n)) := by
        rw [image_iUnion]; exact measure_iUnion_le _
      _ ≤ 0 := by simp only [H, tsum_zero, nonpos_iff_eq_zero]
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
⊢ ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)

Tactic:
have A : ∀ (ε : ℝ≥0), 0 < ε → μ (f '' (s ∩ closedBall 0 R)) ≤ ε * μ (closedBall 0 R) :=
    fun ε εpos =>
    addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux μ
      (fun x hx => (hf' x hx.1).mono inter_subset_left) R inter_subset_right ε εpos
      fun x hx => h'f' x hx.1
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ Tendsto (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)))

Tactic:
have :
      Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝 0)
        (𝓝 (((0 : ℝ≥0) : ℝ≥0∞) * μ (closedBall 0 R))) :=
      ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 tendsto_id)
        (Or.inr measure_closedBall_lt_top.ne)
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
this :
  Tendsto (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝 0) (𝓝 0)

Tactic:
simp only [zero_mul, ENNReal.coe_zero] at this

Premises used: MulZeroClass.zero_mul, ENNReal.coe_zero
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝 0) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)

Tactic:
Tendsto.mono_left this nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝 0) (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)

Tactic:
exact Tendsto.mono_left this nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)

Tactic:
have B : Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝[>] 0) (𝓝 0) := by
    have :
      Tendsto (fun ε : ℝ≥0 => (ε : ℝ≥0∞) * μ (closedBall 0 R)) (𝓝 0)
        (𝓝 (((0 : ℝ≥0) : ℝ≥0∞) * μ (closedBall 0 R))) :=
      ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 tendsto_id)
        (Or.inr measure_closedBall_lt_top.ne)
    simp only [zero_mul, ENNReal.coe_zero] at this
    exact Tendsto.mono_left this nhdsWithin_le_nhds
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
apply :
  ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply ge_of_tendsto B

Premises used: ge_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
h :
  ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Ioi 0) a →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
⊢ ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Ioi 0) a →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)

Tactic:
A

Premises used: Set.Ioi, Set.Mem, setOf
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h'f' : ∀ x ∈ s, (f' x).det = 0
R : ℝ
A :
  ∀ (ε : ℝ≥0),
    0 < ε →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
B :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 0)
⊢ ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Ioi 0) a →
      (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall 0 R)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)

Tactic:
exact A
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
aemeasurable_of_unif_approx fun ε εpos => ?_

Premises used: aemeasurable_of_unif_approx
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
refine :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
refine aemeasurable_of_unif_approx fun ε εpos => ?_

Premises used: aemeasurable_of_unif_approx
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
⊢ 0 < δ

Tactic:
have δpos : 0 < δ := εpos
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
⊢ ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' (fun _ => δ) fun _ =>
      δpos.ne'

Premises used: exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
obtain :
  ∀ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E) (t_disj : Pairwise (Disjoint on t)) (t_meas : ∀ (n : ℕ), MeasurableSet (t n))
    (t_cover : s ⊆ ⋃ (n : ℕ), t n) (ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ),
    (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y) →
      ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
⊢ ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε

Tactic:
obtain ⟨t, A, t_disj, t_meas, t_cover, ht, _⟩ :
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
      Pairwise (Disjoint on t) ∧
        (∀ n : ℕ, MeasurableSet (t n)) ∧
          (s ⊆ ⋃ n : ℕ, t n) ∧
            (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) δ) ∧
              (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
    exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' (fun _ => δ) fun _ =>
      δpos.ne'

Premises used: exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
i j : ℕ
h : (Disjoint on t) i j
⊢ EqOn (β := E →L[ℝ] E) ((fun (n : ℕ) (x : E) ↦ A n) i) ((fun (n : ℕ) (x : E) ↦ A n) j) (t i ∩ t j)

Tactic:
simp only [h.inter_eq, eqOn_empty]

Premises used: Disjoint.inter_eq, Set.eqOn_empty
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
obtain :
  ∀ (g : E → E →L[ℝ] E) (g_meas : Measurable g) (hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n),
    ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε
⊢ ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε

Tactic:
obtain ⟨g, g_meas, hg⟩ :
      ∃ g : E → E →L[ℝ] E, Measurable g ∧ ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n :=
    exists_measurable_piecewise t t_meas (fun n _ => A n) (fun n => measurable_const) <|
      t_disj.mono fun i j h => by simp only [h.inter_eq, eqOn_empty]

Premises used: exists_measurable_piecewise, measurable_const, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
⊢ ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε

Tactic:
⟨g, g_meas.aemeasurable, ?_⟩

Premises used: Measurable.aemeasurable, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
refine : ∀ᵐ (x : E) ∂μ.restrict s, dist (g x) (f' x) ≤ ε
⊢ ∃ (f : E → E →L[ℝ] E), AEMeasurable f (μ.restrict s) ∧ ∀ᵐ (x : E) ∂μ.restrict s, dist (f x) (f' x) ≤ ε

Tactic:
refine ⟨g, g_meas.aemeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun (n : ℕ) ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
rw : s = s ∩ ⋃ (i : ℕ), t i
⊢ s = ⋃ (n : ℕ), s ∩ t n

Tactic:
rw [← inter_iUnion]

Premises used: Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun (n : ℕ) ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = s ∩ ⋃ (i : ℕ), t i

Tactic:
Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_left

Premises used: Set.Subset.antisymm, Set.inter_subset_left, Set.Subset.rfl, Set.subset_inter
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) ε ⋯
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ), ∀ x ∈ t n, g x = A n
H : ∀ᵐ (x : E) ∂sum fun (n : ℕ) ↦ μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = s ∩ ⋃ (i : ℕ), t i

Tactic:
exact Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_left

Premises used: Set.Subset.antisymm, Set.inter_subset_left, Set.Subset.rfl, Set.subset_inter