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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
this :
  ∀ (A : E →L[ℝ] E),
    ∃ (δ : ℝ≥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∞))
choose :
  ∀ (δ : (A : E →L[ℝ] E) → ℝ≥0)
    (hδ :
      ∀ (A : E →L[ℝ] E),
        0 < δ A ∧
          (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
            ∀ (t : Set E) (g : E → E),
              ApproximatesLinearOn g A t (δ A) →
                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∞))),
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
choose δ hδ using this
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
⊢ ∃ (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) (δ (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'

Premises used: exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, LT.lt.ne', And.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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))),
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))

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) (δ (A n))) ∧
              (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
    exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'

Premises used: exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, LT.lt.ne', And.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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
⊢ 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
⊢ 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
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
⊢ s = ⋃ (n : ℕ), s ∩ t n

Tactic:
have s_eq : s = ⋃ n, s ∩ t n := by
    rw [← inter_iUnion]
    exact Subset.antisymm (subset_inter Subset.rfl t_cover) inter_subset_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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
rw : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
| ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
rw [s_eq]
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
conv_lhs :
  ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
conv_lhs => rw [s_eq]
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
hm : ∀ (i : ℕ), MeasurableSet (s ∩ t i)
hd : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ t n)
⊢ ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
rw [lintegral_iUnion]

Premises used: MeasureTheory.lintegral_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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ ∀ (i : ℕ), MeasurableSet (s ∩ t i)

Tactic:
fun n => hs.inter (t_meas n)

Premises used: MeasurableSet.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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ ∀ (i : ℕ), MeasurableSet (s ∩ t i)

Tactic:
exact fun n => hs.inter (t_meas n)

Premises used: MeasurableSet.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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ t n)

Tactic:
pairwise_disjoint_mono t_disj fun n => inter_subset_right

Premises used: pairwise_disjoint_mono, Set.inter_subset_right
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ t n)

Tactic:
exact pairwise_disjoint_mono t_disj fun n => inter_subset_right

Premises used: pairwise_disjoint_mono, Set.inter_subset_right
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
apply :
  ∀ (n : ℕ),
    ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ ≤
      ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ)
    (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ)

Tactic:
apply ENNReal.tsum_le_tsum fun n => ?_

Premises used: ENNReal.tsum_le_tsum
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
n : ℕ
h : ∀ᵐ (a : E) ∂μ.restrict (s ∩ t n), ENNReal.ofReal |(f' a).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)
⊢ ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ ≤
    ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- 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
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            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∞))
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) (δ (A n))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
n : ℕ
h : ∀ (a : E), ‖f' a - A n‖₊ ≤ δ (A n) → ENNReal.ofReal |(f' a).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)
⊢ ∀ᵐ (a : E) ∂μ.restrict (s ∩ t n), ENNReal.ofReal |(f' a).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)

Tactic:
filter_upwards [(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>
          (hf' x hx.1).mono inter_subset_left]

Premises used: ApproximatesLinearOn.norm_fderiv_sub_le, Set.inter_subset_left, And.left, HasFDerivWithinAt.mono, MeasurableSet.inter