mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_3
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
C : Tendsto (fun n ↦ (↑N / (↑N + 1)) ^ n * μ s) atTop (𝓝 (0 * μ s))
⊢ μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) = 0

Tactic:
rw [zero_mul] at C

Goal state after:
case refine_3
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
B : ∀ (n : ℕ), μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
C : Tendsto (fun n ↦ (↑N / (↑N + 1)) ^ n * μ s) atTop (𝓝 0)
⊢ μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) = 0
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
⊢ ε / 2 / ↑N ≠ 0

Tactic:
by simp only [ne_eq, ENNReal.div_eq_zero_iff, hε, ENNReal.ofNat_ne_top, or_self,
          ENNReal.natCast_ne_top, not_false_eq_true]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hf : DifferentiableAt 𝕜 f x
hW : DifferentiableAt 𝕜 W x
⊢ lieBracket 𝕜 V (fun y ↦ f y • W y) x = (fderiv 𝕜 f x) (V x) • W x + f x • lieBracket 𝕜 V W x

Tactic:
simp_rw [← differentiableWithinAt_univ, ← lieBracketWithin_univ, fderiv] at hW hf ⊢
  exact lieBracketWithin_smul_right hf hW uniqueDiffWithinAt_univ

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ lieBracket 𝕜 V (W + W₁) x = lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x

Tactic:
by
  simp only [lieBracket, Pi.add_apply, map_add]
  rw [fderiv_add hW hW₁, add_apply]
  abel

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ lieBracketWithin 𝕜 U (lieBracketWithin 𝕜 V W s) s x =
    lieBracketWithin 𝕜 (lieBracketWithin 𝕜 U V s) W s x + lieBracketWithin 𝕜 V (lieBracketWithin 𝕜 U W s) s x

Tactic:
apply leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt hs hx
    (hU.of_le (le_minSmoothness.trans hn)) (hV.of_le (le_minSmoothness.trans hn))
    (hW.of_le (le_minSmoothness.trans hn))

Goal state after:
case h'U
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 U s x

case h'V
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 V s x

case h'W
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
hn : minSmoothness 𝕜 2 ≤ n
U V W : E → E
s : Set E
x : E
hs : UniqueDiffOn 𝕜 s
h'x : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior s)
hx : x ∈ s
hU : ContDiffWithinAt 𝕜 n U s x
hV : ContDiffWithinAt 𝕜 n V s x
hW : ContDiffWithinAt 𝕜 n W s x
⊢ IsSymmSndFDerivWithinAt 𝕜 W s x
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
⊢ (fun h ↦
      f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w) =o[𝓝[>] 0]
    fun h ↦ h ^ 2

Tactic:
by
  have A : (1 : ℝ) / 2 ∈ Ioc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
  have B : (1 : ℝ) / 2 ∈ Icc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
  have h2v2w : x + (2 : ℝ) • v + (2 : ℝ) • w ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h4v h4w B using 1
    module
  have h2vww : x + (2 • v + w) + w ∈ interior s := by
    convert! h2v2w using 1
    module
  have h2v : x + (2 : ℝ) • v ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h4v A using 1
    module
  have h2w : x + (2 : ℝ) • w ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h4w A using 1
    module
  have hvw : x + (v + w) ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h2v2w A using 1
    module
  have h2vw : x + (2 • v + w) ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1
    module
  have hvww : x + (v + w) + w ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h2w h2v2w B using 1
    module
  have TA1 := s_conv.taylor_approx_two_segment hf xs hx h2vw h2vww
  have TA2 := s_conv.taylor_approx_two_segment hf xs hx hvw hvww
  convert! TA1.sub TA2 using 1
  ext h
  simp only [two_smul, smul_add, ← add_assoc, map_add,
    add_apply]
  abel

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
hne : (interior s).Nonempty
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
⊢ (f'' v) w = (f'' w) v

Tactic:
rcases hne with ⟨y, hy⟩
  obtain ⟨z, hz⟩ : ∃ z, z = ((1 : ℝ) / 4) • (y - x) := ⟨((1 : ℝ) / 4) • (y - x), rfl⟩
  have A : ∀ m : E, Filter.Tendsto (fun t : ℝ => x + (4 : ℝ) • (z + t • m)) (𝓝 0) (𝓝 y) := by
    intro m
    have : x + (4 : ℝ) • (z + (0 : ℝ) • m) = y := by simp [hz]
    rw [← this]
    refine tendsto_const_nhds.add <| tendsto_const_nhds.smul <| tendsto_const_nhds.add ?_
    exact continuousAt_id.smul continuousAt_const
  have B : ∀ m : E, ∀ᶠ t in 𝓝[>] (0 : ℝ), x + (4 : ℝ) • (z + t • m) ∈ interior s := by
    intro m
    apply nhdsWithin_le_nhds
    apply A m
    rw [mem_interior_iff_mem_nhds] at hy
    exact interior_mem_nhds.2 hy
  -- we choose `t m > 0` such that `x + 4 (z + (t m) m)` belongs to the interior of `s`, for any
  -- vector `m`.
  choose t ts tpos using fun m => ((B m).and self_mem_nhdsWithin).exists
  -- applying `second_derivative_within_at_symmetric_of_mem_interior` to the vectors `z`
  -- and `z + (t m) m`, we deduce that `f'' m z = f'' z m` for all `m`.
  have C : ∀ m : E, f'' m z = f'' z m := by
    intro m
    have : f'' (z + t m • m) (z + t 0 • (0 : E)) = f'' (z + t 0 • (0 : E)) (z + t m • m) :=
      s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts 0) (ts m)
    simp only [map_add, map_smul, add_right_inj, add_apply, smul_apply, add_zero, smul_zero] at this
    exact smul_right_injective F (tpos m).ne' this
  -- applying `second_derivative_within_at_symmetric_of_mem_interior` to the vectors `z + (t v) v`
  -- and `z + (t w) w`, we deduce that `f'' v w = f'' w v`. Cross terms involving `z` can be
  -- eliminated thanks to the fact proved above that `f'' m z = f'' z m`.
  have : f'' (z + t v • v) (z + t w • w) = f'' (z + t w • w) (z + t v • v) :=
    s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts w) (ts v)
  simp only [map_add, map_smul, add_apply, smul_apply, C] at this
  have : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v := by
    linear_combination (norm := module) this
  apply smul_right_injective F _ this
  simp [(tpos v).ne', (tpos w).ne']

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

Goal state before:
pp: a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
⊢ Tendsto (fun x ↦ f x / g x) atTop l

Tactic:
have fact2 (x) (hx : x ∈ Ioo 0 a'⁻¹) : a < x⁻¹ := lt_trans haa' ((lt_inv_comm₀ ha' hx.1).mpr hx.2)

Goal state after:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹
⊢ Tendsto (fun x ↦ f x / g x) atTop l
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
s : Set α
φ : ι → Set α
hs : MeasurableSet s
ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n
measurable : ∀ (n : ι), MeasurableSet (φ n)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ∀ᶠ (i : ι) in l, x ∈ φ i

Tactic:
ae_restrict_iff' hs

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
l : Filter ι
s : Set α
φ : ι → Set α
hs : MeasurableSet s
ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n
measurable : ∀ (n : ι), MeasurableSet (φ n)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (i : ι) in l, x ∈ φ i
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case h₁
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
a : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * ‖(f' x - A) a‖ ≤ r * (↑δ + ε) * (‖z‖ + ε)
⊢ ‖(f' x - A) a‖ ≤ (↑δ + ε) * (‖z‖ + ε)

Tactic:
mul_assoc

Goal state after:
case h₁
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
a : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * ‖(f' x - A) a‖ ≤ r * ((↑δ + ε) * (‖z‖ + ε))
⊢ ‖(f' x - A) a‖ ≤ (↑δ + ε) * (‖z‖ + ε)
Module: Mathlib.MeasureTheory.Function.Jacobian

Goal state before:
pp: case h₁
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
a : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * ‖(f' x - A) a‖ ≤ r * ((↑δ + ε) * (‖z‖ + ε))
⊢ ‖(f' x - A) a‖ ≤ (↑δ + ε) * (‖z‖ + ε)

Tactic:
exact (mul_le_mul_iff_right₀ rpos).1 I

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y

Tactic:
by
  have a : (· ^ p) '' (Ioi 0) = Ioi (0 : ℝ) := by
    ext1 x; rw [mem_image]; constructor
    · rintro ⟨y, hy, rfl⟩; exact rpow_pos_of_pos hy p
    · exact fun hx ↦ ⟨x ^ (1 / p), rpow_pos_of_pos hx _, by simp [← rpow_mul (le_of_lt hx), hp]⟩
  have := integral_image_eq_integral_abs_deriv_smul measurableSet_Ioi
    (fun x hx ↦ (hasDerivAt_rpow_const (Or.inl (mem_Ioi.mp hx).ne')).hasDerivWithinAt)
    ((rpow_left_injOn hp).mono (by grind)) g
  rw [a] at this; rw [this]
  refine setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
  rw [abs_mul, abs_of_nonneg (rpow_nonneg (le_of_lt hx) _)]

Goal state after:
Module: Mathlib.Analysis.Complex.RemovableSingularity

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z
ho : (fun z ↦ f z - f c) =o[𝓝[≠] c] fun z ↦ (z - c)⁻¹
⊢ Tendsto f (𝓝[≠] c) (𝓝 ((𝓝[≠] c).limUnder f))

Tactic:
by
  rw [eventually_nhdsWithin_iff] at hd
  have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c}) := fun z hz =>
    (hz.1 hz.2).differentiableWithinAt
  have H := differentiableOn_update_limUnder_of_isLittleO hd this ho
  exact continuousAt_update_same.1 (H.differentiableAt hd).continuousAt

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
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
⊢ μ (f '' s) ≤ ↑ε * μ (closedBall 0 R)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | h's); · simp only [measure_empty, zero_le, image_empty]
  have :
      ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧
        ∀ (t : Set E), ApproximatesLinearOn f A t δ →
          μ (f '' t) ≤ (Real.toNNReal |A.det| + ε : ℝ≥0) * μ t := by
    intro A
    let m : ℝ≥0 := Real.toNNReal |A.det| + ε
    have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]
    rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
    exact ⟨δ, h', fun t ht => h t f ht⟩
  choose δ hδ using this
  obtain ⟨t, A, t_disj, t_meas, t_cover, ht, Af'⟩ :
    ∃ (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'
  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.Analysis.Complex.LocallyUniformLimit

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : (sphere z r).Nonempty
e2 : ContinuousOn (fun w ↦ ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : IsMaxOn (fun w ↦ ‖f w‖) (sphere z r) x
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L

Tactic:
exact ⟨‖f x‖, hfM x hx, hx'⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
M : Type u_2
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : T1Space H
⊢ T1Space M

Tactic:
by
  apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
  by_cases hy : y ∈ (chartAt H x).source
  · refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
    · exact OpenPartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton
    · simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage,
        mem_singleton_iff, true_and]
      exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy
  · exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.ChartedSpace

Goal state before:
pp: H : Type u
H' : Type u_1
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
inst✝ : Nonempty H
p : M ⊕ M'
⊢ Sum.elim (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯)
      (fun x ↦ (ChartedSpace.chartAt x).lift_openEmbedding ⋯) p ∈
    (fun e ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas ∪ (fun e ↦ e.lift_openEmbedding ⋯) '' ChartedSpace.atlas

Tactic:
cases p with
    | inl x =>
      rw [Sum.elim_inl]
      left
      use ChartedSpace.chartAt x, cm.chart_mem_atlas x
    | inr x =>
      rw [Sum.elim_inr]
      right
      use ChartedSpace.chartAt x, cm'.chart_mem_atlas x

Goal state after:
Module: Mathlib.Geometry.Manifold.HasGroupoid

Goal state before:
pp: H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
e : OpenPartialHomeomorph M H
he : e ∈ atlas H M
s : Opens M
hs : Nonempty ↥s
G : StructureGroupoid H
inst✝¹ : HasGroupoid M G
inst✝ : ClosedUnderRestriction G
e' : OpenPartialHomeomorph (↥s) H
he' : e' ∈ atlas H ↥s
x : ↥s
this : e' = (chartAt H ↑x).subtypeRestr hs
⊢ (e.subtypeRestr hs).symm ≫ₕ (chartAt H ↑x).subtypeRestr hs ∈ G ∧
    ((chartAt H ↑x).subtypeRestr hs).symm ≫ₕ e.subtypeRestr hs ∈ G

Tactic:
exact ⟨G.trans_restricted he (chart_mem_atlas H (x : M)) hs,
         G.trans_restricted (chart_mem_atlas H (x : M)) he hs⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.LocalInvariantProperties

Goal state before:
pp: case hu.refine_1
H : Type u_1
M : Type u_2
H' : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
e : OpenPartialHomeomorph M H
P : (H → H') → Set H → H → Prop
s : Set M
x : M
hG : G.LocalInvariantProp G' P
g : M → H'
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
⊢ ↑e.symm ⁻¹' (chartAt H x).source ∈ 𝓝 (↑e x)

Tactic:
refine (e.symm.continuousAt <| e.mapsTo xe).preimage_mem_nhds
        ((chartAt H x).open_source.mem_nhds ?_)
      simp_rw [e.left_inv xe, mem_chart_source H x]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (extendCoordChange e e').symm.source = ↑I '' (e.symm ≫ₕ e').target

Tactic:
← OpenPartialHomeomorph.symm_source

Goal state after:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
e e' : OpenPartialHomeomorph M H
⊢ (extendCoordChange e e').symm.source = ↑I '' (e.symm ≫ₕ e').symm.source