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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
⊢ ∀ n ≤ N, G n < p.lastStep

Tactic:
intro n

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
n : ℕ
⊢ n ≤ N → G n < p.lastStep
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
⊢ ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))

Tactic:
intro n

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
n : ℕ
⊢ n ≤ N → p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
⊢ D * (1 + D - ‖1 • x‖) / (1 + D) + dist z (1 • x) ≤ 1

Tactic:
dist_eq_norm,

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
⊢ D * (1 + D - ‖1 • x‖) / (1 + D) + ‖z - 1 • x‖ ≤ 1
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
⊢ ∀ (n : ℕ), F (u n) ∈ closedBall 0 2

Tactic:
intro n

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
n : ℕ
⊢ F (u n) ∈ closedBall 0 2
Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f : E → F
ε : ℝ
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ∃ g, ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ

Tactic:
refine ⟨_, ?_, fun a δ ↦ φ.dist_normed_convolution_le hf.aestronglyMeasurable⟩

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f : E → F
ε : ℝ
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hf : LocallyIntegrable f μ
hε : 0 < ε
φ : ContDiffBump 0 := { rIn := ε / 2, rOut := ε, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
⊢ ContDiff ℝ ∞ fun a ↦ convolution (φ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ a
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst✝¹², inst✝⁶] ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
⊢ ν univ < ∞

Tactic:
apply measure_lt_top

Goal state after:
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
hi : 2 < ‖a.c i‖
hij : ‖a.c i‖ ≤ ‖a.c j‖
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
this : i < last N
⊢ ‖a.c i‖ = dist (a.c i) (a.c (last N))

Tactic:
dist_eq_norm,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
hi : 2 < ‖a.c i‖
hij : ‖a.c i‖ ≤ ‖a.c j‖
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
this : i < last N
⊢ ‖a.c i‖ = ‖a.c i - a.c (last N)‖
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y ↦ (B (f y)) (g y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Tactic:
have isoE : Eu ≃ₗᵢ[𝕜] E := LinearIsometryEquiv.ulift 𝕜 E

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y ↦ (B (f y)) (g y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Module: Mathlib.Analysis.Calculus.Darboux

Goal state before:
pp: a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' Ioo a b

Tactic:
rcases hab.eq_or_lt with (rfl | hab')
  · exact (lt_asymm hma hmb).elim
  set g : ℝ → ℝ := fun x => f x - m * x
  have hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x := by
    intro x hx
    simpa using! (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
  obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt
  have cmem' : c ∈ Ioo a b := by
    rcases cmem.1.eq_or_lt with (rfl | hac)
    -- Show that `c` can't be equal to `a`
    · refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)
      have : b - a ∈ posTangentConeAt (Icc a b) a :=
        sub_mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.rfl)
      simpa only [ContinuousLinearMap.smulRight_apply, one_apply_eq_self]
        using! hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
    rcases cmem.2.eq_or_lt' with (rfl | hcb)
    -- Show that `c` can't be equal to `b`
    · refine absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right ?_ (sub_lt_zero.2 hab'))
        (not_le_of_gt hmb)
      have : a - b ∈ posTangentConeAt (Icc a b) b :=
        sub_mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
      simpa only [ContinuousLinearMap.smulRight_apply, one_apply_eq_self]
        using! hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
    exact ⟨hac, hcb⟩
  use c, cmem'
  rw [← sub_eq_zero]
  have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]
  exact (hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : 0 < f x
⊢ HasFDerivAt (fun x ↦ |f x|) f' x

Tactic:
by
  convert! (hasDerivAt_abs_pos h₀).hasFDerivAt.comp x hf using 1
  ext y
  simp

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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)
⊢ ∀ (n : ℕ), P (u n)

Tactic:
intro n

Goal state after:
α : 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)
n : ℕ
⊢ P (u n)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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)
⊢ ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)

Tactic:
intro n

Goal state after:
α : 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)
n : ℕ
⊢ μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
⊢ ContinuousOn f (Icc a b)

Tactic:
by_cases! g₀ : a ≤ b

Goal state after:
case pos
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a ≤ b
⊢ ContinuousOn f (Icc a b)

case neg
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : b < a
⊢ ContinuousOn f (Icc a b)
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: case refine_2
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x
⊢ MonotoneOn f (Ico b c)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ico b c) (continuousOn_Ico h hd₁) <;> simp_all

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
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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
this : Tendsto (fun h ↦ h * (‖v‖ + ‖w‖)) (𝓝[>] 0) (𝓝 (0 * (‖v‖ + ‖w‖)))
⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ

Tactic:
apply (tendsto_order.1 this).2 δ

Goal state after:
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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝[interior s] x, ‖f' x_1 - f' x - f'' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ : Metric.ball x δ ∩ interior s ⊆ {x_1 | (fun x_2 ↦ ‖f' x_2 - f' x - f'' (x_2 - x)‖ ≤ ε * ‖x_2 - x‖) x_1}
this : Tendsto (fun h ↦ h * (‖v‖ + ‖w‖)) (𝓝[>] 0) (𝓝 (0 * (‖v‖ + ‖w‖)))
⊢ δ > 0 * (‖v‖ + ‖w‖)
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
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + 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:
have h2vw : x + (2 • v + w) ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1
    module

Goal state after:
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
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + 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
Module: Mathlib.Analysis.Calculus.LineDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v

Tactic:
apply derivWithin_eq ?_ (by simpa using hx)

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₁ : E → F
s : Set E
x v : E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fun t ↦ f₁ (x + t • v)) =ᶠ[𝓝[(fun t ↦ x + t • v) ⁻¹' s] 0] fun t ↦ f (x + t • v)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
have : closedBall x r = closedBall x (δ / 2) := Subset.antisymm ht (by gcongr)

Goal state after:
case inr
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun r ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun x ↦ {r | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
this : closedBall x r = closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty
Module: Mathlib.Analysis.Calculus.FDeriv.Norm

Goal state before:
pp: 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)
⊢ HasFDerivAt (fun x ↦ ‖x‖) (↑(SignType.sign t) • f) (t • x)

Tactic:
have h2 : HasFDerivAt (fun y ↦ |t| * ‖y‖) (|t| • f) x := h.const_smul |t|

Goal state after:
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) x
⊢ HasFDerivAt (fun x ↦ ‖x‖) (↑(SignType.sign t) • f) (t • x)