mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |t| * ‖t⁻¹‖ * ‖x✝‖

Tactic:
norm_eq_abs,

Goal state after:
case e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasStrictFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasStrictFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasStrictFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |t| * |t⁻¹| * ‖x✝‖
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
h : ¬IsRCLikeNormedField 𝕜
hn : n = ω
⊢ ContDiffAt 𝕜 ω f x

Tactic:
simpa [hn] using hf

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: case e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |t| * ‖t⁻¹‖ * ‖x✝‖

Tactic:
norm_eq_abs,

Goal state after:
case e'_11
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : StrongDual ℝ E
x : E
t : ℝ
ht : t ≠ 0
h : HasFDerivAt (fun x ↦ ‖x‖) f x
h1 : HasFDerivAt (fun y ↦ t⁻¹ • y) (t⁻¹ • ContinuousLinearMap.id ℝ E) (t • x)
h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) (t⁻¹ • t • x)
x✝ : E
⊢ ‖x✝‖ = |t| * |t⁻¹| * ‖x✝‖
Module: Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : ↑i ≤ n
⊢ iteratedDeriv i (g ∘ f) x = ∑ c, (iteratedFDeriv 𝕜 c.length g (f x)) fun j ↦ iteratedDeriv (c.partSize j) f x

Tactic:
simp only [← iteratedDerivWithin_univ, ← iteratedFDerivWithin_univ]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
g : E → F
f : 𝕜 → E
x : 𝕜
n : ℕ∞ω
i : ℕ
hg : ContDiffAt 𝕜 n g (f x)
hf : ContDiffAt 𝕜 n f x
hi : ↑i ≤ n
⊢ iteratedDerivWithin i (g ∘ f) univ x =
    ∑ x_1, (iteratedFDerivWithin 𝕜 x_1.length g univ (f x)) fun j ↦ iteratedDerivWithin (x_1.partSize j) f univ x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case pos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]]) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
rw [hf.image_uIcc, ← intervalIntegrable_iff'] at hg1

Goal state after:
case pos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]] volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := ⋯
a_count : a.Countable
s₁ : Set ℝ := ⋯
hs₁ : MeasurableSet s₁
u : Set ℝ := ⋯
hu : u.Countable
b : Set ℝ := ⋯
hb : MeasurableSet b
c : Set ℝ := ⋯
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
⊢ f x ≤ f y

Tactic:
rw [← fpx]

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : p < x
y : ℝ
hy : y ∈ s ∩ Ioo p x
⊢ f p ≤ f y
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := ⋯
a_count : a.Countable
s₁ : Set ℝ := ⋯
hs₁ : MeasurableSet s₁
u : Set ℝ := ⋯
hu : u.Countable
b : Set ℝ := ⋯
hb : MeasurableSet b
c : Set ℝ := ⋯
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
y : ℝ
hy : y ∈ s ∩ Ioo x p
⊢ f y ≤ f x

Tactic:
rw [← fpx]

Goal state after:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c | ∃ x y, x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
hb : MeasurableSet b
c : Set ℝ := s₁ \ b
hc : MeasurableSet c
x : ℝ
hx : x ∈ b
p : ℝ
ps₁ : p ∈ s₁
px✝ : p ≠ x
fpx : f p = f x
px : x < p
y : ℝ
hy : y ∈ s ∩ Ioo x p
⊢ f y ≤ f p
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case pos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntervalIntegrable g volume (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]]))
hg2 : IntervalIntegrable (fun x ↦ f' x • (g ∘ f) x) volume a b
hE : CompleteSpace E
h_cont : ContinuousOn (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) [[a, b]]
h_der :
  ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun u ↦ ∫ (t : ℝ) in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
simp_rw [integral_eq_sub_of_hasDeriv_right h_cont h_der hg2, integral_same, sub_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case hf'_nonneg
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
⊢ ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ deriv f x

Tactic:
intro z hz

Goal state after:
case hf'_nonneg
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
z : ℝ
hz : z ∈ Ioo (min a b) (max a b)
⊢ 0 ≤ deriv f z
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case inr
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ ∫ (x : ℝ) in a..b, f' x • g (f x) = ∫ (u : ℝ) in f a..f b, g u

Tactic:
rw [integral_of_ge hab.le, ← integral_Icc_eq_integral_Ioc,
      integral_Icc_deriv_smul_of_deriv_nonneg, integral_of_ge, ← integral_Icc_eq_integral_Ioc]
    · apply M right_mem_uIcc left_mem_uIcc hab.le
    · rwa [uIcc_of_ge hab.le] at hf
    · grind
    · grind
    · exact hab.le

Goal state after:
Module: Mathlib.Analysis.Calculus.LHopital

Goal state before:
pp: a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Ici a \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[Ici a \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun x ↦ deriv f x / deriv g x) (𝓝[Ici a \ {a}] a) l
⊢ Tendsto (fun x ↦ f x / g x) (𝓝[Ici a \ {a}] a) l

Tactic:
exact lhopital_zero_nhdsWithin_convex (convex_Ici a) hdf hg' hfa hga hdiv

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case inr
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ IntervalIntegrable (fun x ↦ f' x • g (f x)) volume a b ↔ IntervalIntegrable g volume (f a) (f b)

Tactic:
rw [IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le hab.le,
      integrableOn_Icc_deriv_smul_iff_of_deriv_nonneg,
      IntervalIntegrable.symm_iff, intervalIntegrable_iff_integrableOn_Icc_of_le]

Goal state after:
case inr
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ f b ≤ f a

case inr.hf
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ ContinuousOn f (Icc b a)

case inr.hff'
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, HasDerivAt f (f' x) x

case inr.hf'
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ ∀ x ∈ Ioo b a, 0 ≤ f' x

case inr.hab
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ f' x
M : MonotoneOn f [[a, b]]
hab : b < a
⊢ b ≤ a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: case hf'_nonpos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
⊢ ∀ x ∈ Ioo (min a b) (max a b), deriv f x ≤ 0

Tactic:
intro z hz

Goal state after:
case hf'_nonpos
a b : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo (min a b) (max a b), f' x ≤ 0
z : ℝ
hz : z ∈ Ioo (min a b) (max a b)
⊢ deriv f z ≤ 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : OpensMeasurableSpace α
d : ι → α
B : α
hd : Tendsto d l atTop
inst✝ : NoMaxOrder α
⊢ ∀ᵐ (x : α) ∂μ.restrict (Ici B), ∀ᶠ (i : ι) in l, x ∈ Ico B (d i)

Tactic:
by
    refine (ae_restrict_mem measurableSet_Ici).mono fun _x hx ↦ ?_
    simp only [mem_Ico, eventually_and]
    exact⟨.of_forall fun i => hx, hd.eventually (eventually_gt_atTop _x)⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ f z ∈ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)

Tactic:
apply Set.mem_add.2 ⟨A (z - x), _, f z - f x - A (z - x) + f x, _, _⟩

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ⋯
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ A (z - x) ∈ ⇑A '' closedBall 0 r

E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ⋯
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ f z - f x - A (z - x) + f x ∈ closedBall (f x) (ε * r)

E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ⋯
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio (NNReal.mk ε ⋯) ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ A (z - x) + (f z - f x - A (z - x) + f x) = f z
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf'_nonneg
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
⊢ ∀ x ∈ Ioo a b, 0 ≤ deriv f x

Tactic:
intro z hz

Goal state after:
case hf'_nonneg
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, 0 ≤ f' x
hab : a ≤ b
z : ℝ
hz : z ∈ Ioo a b
⊢ 0 ≤ deriv f z
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))

Tactic:
let φ i := Iic (b i)

Goal state after:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : ι → Set ℝ := fun i ↦ Iic (b i)
⊢ Tendsto (fun i ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : AntitoneOn f s
g : ℝ → F
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x ↦ -f' x • g (f x)) s volume

Tactic:
let n : ℝ → ℝ := (fun x ↦ -x)
  let e := n ∘ f
  have hg' (x) (hx : x ∈ s) : HasDerivWithinAt e (-f' x) s x := (hf' x hx).neg
  have A : IntegrableOn (fun x ↦ g (n x)) (e '' s)
      ↔ IntegrableOn (fun x ↦ (-f' x) • (g ∘ n) (e x)) s := by
    rw [← integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hg' hf.neg (g ∘ n)]; rfl
  have B : IntegrableOn g (n '' e '' s) ↔ IntegrableOn (fun x ↦ (|-1| : ℝ) • g (n x)) (e '' s) :=
    integrableOn_image_iff_integrableOn_abs_deriv_smul (hs.image_of_monotoneOn hf.neg)
      (fun x hx ↦ hasDerivWithinAt_neg _ _) neg_injective.injOn _
  simp only [abs_neg, abs_one, one_smul] at B
  rw [A, ← image_comp] at B
  convert! B using 3 with x hx x <;> simp [n, e]

Goal state after:
Module: Mathlib.MeasureTheory.Function.JacobianOneDim

Goal state before:
pp: case hf'_nonpos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
⊢ ∀ x ∈ Ioo a b, deriv f x ≤ 0

Tactic:
intro z hz

Goal state after:
case hf'_nonpos
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
g : ℝ → F
hf : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hf' : ∀ x ∈ Ioo a b, f' x ≤ 0
hab : a ≤ b
z : ℝ
hz : z ∈ Ioo a b
⊢ deriv f z ≤ 0
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ [[a, b]] ⊆ Ici a

Tactic:
rw [uIcc_of_le hb.le]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a) volume
hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
i1 : Ioo (min a b) (max a b) ⊆ Ioi a
⊢ Icc a b ⊆ Ici a
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := Ioi 0
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ InjOn (fun x ↦ x ^ p) S

Tactic:
apply StrictAntiOn.injOn

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
S : Set ℝ := ⋯
a1 : ∀ x ∈ S, HasDerivWithinAt (fun t ↦ t ^ p) (p * x ^ (p - 1)) S x
h : p < 0
⊢ StrictAntiOn (fun x ↦ x ^ p) S
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧ ∀ (t : Set E), ApproximatesLinearOn f A t (δ A) → μ (f '' t) ≤ ↑(|A.det|.toNNReal + ε) * μ t
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))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)

Tactic:
calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      rw [← image_iUnion, ← inter_iUnion]
      gcongr
      exact subset_inter Subset.rfl t_cover
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + ε : ℝ≥0) * μ (s ∩ t n) := by
      gcongr
      exact (hδ (A _)).2 _ (ht _)
    _ = ∑' n, ε * μ (s ∩ t n) := by
      congr with n
      rcases Af' h's n with ⟨y, ys, hy⟩
      simp only [hy, h'f' y ys, Real.toNNReal_zero, abs_zero, zero_add]
    _ ≤ ε * ∑' n, μ (closedBall 0 R ∩ t n) := by
      rw [ENNReal.tsum_mul_left]
      gcongr
    _ = ε * μ (⋃ n, closedBall 0 R ∩ t n) := by
      rw [measure_iUnion]
      · exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
      · intro n
        exact measurableSet_closedBall.inter (t_meas n)
    _ ≤ ε * μ (closedBall 0 R) := by grw [← inter_iUnion, inter_subset_left]

Goal state after:
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
A : f '' s =ᵐ[μ] f '' t
⊢ NullMeasurableSet (f '' s) μ

Tactic:
apply NullMeasurableSet.congr _ A.symm

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᵐ[μ] s
A : f '' s =ᵐ[μ] f '' t
⊢ NullMeasurableSet (f '' t) μ
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
have A : s = ⋃ n, s ∩ u n := by
    rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ