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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i : Ordinal.{u}
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)
g : ℕ → Ordinal.{u}
n : ℕ
hN : IsEmpty (SatelliteConfig α n p.τ)
IH : ∀ y < i, y < p.lastStep → p.color y < n
N_mem : n ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = n
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_1 ↦ if n_1 = n then i else g n_1
color_G : ∀ n_1 ≤ n, p.color (G n_1) = n_1
hn : n ≤ n
⊢ G n < p.lastStep

Tactic:
simp only [G]

Goal state after:
case inl
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i : Ordinal.{u}
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)
g : ℕ → Ordinal.{u}
n : ℕ
hN : IsEmpty (SatelliteConfig α n p.τ)
IH : ∀ y < i, y < p.lastStep → p.color y < n
N_mem : n ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = n
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_1 ↦ if n_1 = n then i else g n_1
color_G : ∀ n_1 ≤ n, p.color (G n_1) = n_1
hn : n ≤ n
⊢ (if True then i else g n) < p.lastStep
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : 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 : ℕ
hn : n ≤ N
H : n < N
⊢ G n < p.lastStep

Tactic:
simp only [G]

Goal state after:
case inr
α : 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 : ℕ
hn : n ≤ N
H : n < N
⊢ (if n = N then i else g n) < p.lastStep
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case pos
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : 1 < R
⊢ 0 ≤ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ∧ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) ≤ 1

pp: case neg
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : ¬1 < R
⊢ 0 ≤ 0 ∧ 0 ≤ 1

Tactic:
· refine ⟨y_nonneg _ _, y_le_one _ (IR R h)⟩

Goal state after:
case neg
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h : ¬1 < R
⊢ 0 ≤ 0 ∧ 0 ≤ 1
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ≤ multiplicity E

Tactic:
apply le_csSup
  · refine ⟨5 ^ finrank ℝ E, ?_⟩
    rintro _ ⟨s, ⟨rfl, h⟩⟩
    exact Besicovitch.card_le_of_separated s h.1 h.2
  · simp only [mem_ofPred_eq, Ne]
    exact ⟨s, rfl, hs, h's⟩

Goal state after:
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 := ⋯ }
⊢ ContDiff ℝ ∞ fun a ↦ convolution (φ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ a

Tactic:
exact φ.hasCompactSupport_normed.contDiff_convolution_left _ φ.contDiff_normed hf

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

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
b : β
⊢ ∃ a < p.lastStep, dist (p.c b) (p.c (p.index a)) < p.r (p.index a)

Tactic:
by
      simpa only [iUnionUpTo, exists_prop, mem_iUnion, mem_ball, Subtype.exists,
        Subtype.coe_mk] using p.mem_iUnionUpTo_lastStep b

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case pos
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
s_eq : s = ⋃ n, s ∩ f n • (k * k⁻¹)
I : μ' s = ∑' (n : ℕ), μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
J : ν s = ∑' (n : ℕ), ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
⊢ ∑' (n : ℕ), μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n) =
    ∑' (n : ℕ), ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)

Tactic:
congr with n

Goal state after:
case pos.e_f
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
f : ℕ → G
m_max : Maximal (fun x ↦ x ∈ A) (range f)
hms : range f ⊆ s
hdj : (range f).PairwiseDisjoint fun x ↦ x • k
hm : (range f).Nonempty
h'm : (range f).Countable
M : ∀ (i : ℕ), MeasurableSet (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) i)
sm : s ⊆ ⋃ y, f y • (k * k⁻¹)
s_eq : s = ⋃ n, s ∩ f n • (k * k⁻¹)
I : μ' s = ∑' (n : ℕ), μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
J : ν s = ∑' (n : ℕ), ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
n : ℕ
⊢ μ' (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n) = ν (disjointed (fun n ↦ s ∩ f n • (k * k⁻¹)) n)
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
inst✝⁵ : LocallyCompactSpace G
μ' μ : Measure G
inst✝⁴ : μ.IsHaarMeasure
inst✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ∞
h's : μ' s ≠ ∞
⊢ μ' s = μ'.haarScalarFactor μ • μ s

Tactic:
let c := haarScalarFactor μ' μ

Goal state after:
G : Type u_1
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : Group G
inst✝⁸ : IsTopologicalGroup G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : LocallyCompactSpace G
μ' μ : Measure G
inst✝⁴ : μ.IsHaarMeasure
inst✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ∞
h's : μ' s ≠ ∞
c : ℝ≥0 := μ'.haarScalarFactor μ
⊢ μ' s = μ'.haarScalarFactor μ • μ s
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
⊢ i < last N

Tactic:
apply lt_top_iff_ne_top.2

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
⊢ i ≠ ⊤
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:
rw [huniv]

Goal state after:
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 < ∞
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
α : ↑I
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : i ≤ 0
⊢ i = 0

Tactic:
nonpos_iff_eq_zero

Goal state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
α : ↑I
f : E → F
a : E
g : F → G
hd : DifferentiableAt ℝ g (f a) ∨ DifferentiableAt ℝ f a
i : ℕ
hfd : ¬DifferentiableAt ℝ f a
hg : ContDiffPointwiseHolderAt 0 α g (f a)
hf : ContDiffPointwiseHolderAt 0 α f a
hi : i = 0
⊢ i = 0
Module: Mathlib.Analysis.Calculus.Deriv.Star

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : StarRing 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : StarAddMonoid F
inst✝² : StarModule 𝕜 F
inst✝¹ : ContinuousStar F
f : 𝕜 → F
x : 𝕜
inst✝ : TrivialStar 𝕜
s : Set 𝕜
⊢ derivWithin (fun y ↦ star (f y)) s x = star (derivWithin f s x)

Tactic:
by_cases hxs : UniqueDiffWithinAt 𝕜 s x
  · exact DFunLike.congr_fun (fderivWithin_star hxs) _
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hxs]

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

Goal state before:
pp: case refine_2
α : 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)
p : α × ℝ
hp : p ∈ ⋃ n, ↑(u n)
n : ℕ
hn : p ∈ ↑(u n)
⊢ p.2 ∈ f p.1

Tactic:
exact (Pu n).2.2 p (Finset.mem_coe.1 hn)

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
⊢ ContinuousOn f (Ici a)

Tactic:
rw [← Ioi_union_left]
  exact hd₀.continuousOn.union_continuousAt isOpen_Ioi (by simp [h])

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
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
⊢ AntitoneOn f (Ioc a b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
a b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ AntitoneOn f (Ioc a b)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ioc a b) (continuousOn_Ioc hb hd₀) <;> simp_all

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y ↦ (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
by
  apply ((ContinuousLinearMap.apply 𝕜 G c).norm_iteratedFDerivWithin_comp_left hf hs hx hn).trans
  gcongr
  refine (ContinuousLinearMap.apply 𝕜 G c).opNorm_le_bound (norm_nonneg _) fun f => ?_
  rw [ContinuousLinearMap.apply_apply, mul_comm]
  exact f.le_opNorm c

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
s : Set E
x : E
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ -lieBracketWithin 𝕜 W (fun y ↦ f y • V y) s x = -(fderivWithin 𝕜 f s x) (W x) • V x + f x • lieBracketWithin 𝕜 V W s x

Tactic:
lieBracketWithin_smul_right hf hV hs,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
f : E → 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hV : DifferentiableWithinAt 𝕜 V s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ -((fderivWithin 𝕜 f s x) (W x) • V x + f x • lieBracketWithin 𝕜 W V s x) =
    -(fderivWithin 𝕜 f s x) (W x) • V x + f x • lieBracketWithin 𝕜 V W s x
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 τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
x : α
hx : x ∈ t0
⊢ closedBall x (r0 x) ⊆ u

Tactic:
apply Subset.trans (closedBall_subset_ball (hr0 x hx).2.2) (hR x (t0s hx)).2

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

Goal state before:
pp: case pos.hxs
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
s : Set E
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
t : Set F
hf : IsSymmSndFDerivWithinAt 𝕜 f s x
h'f : ContDiffWithinAt 𝕜 2 f s x
hV : DifferentiableWithinAt 𝕜 V t (f x)
hW : DifferentiableWithinAt 𝕜 W t (f x)
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
hst : MapsTo f s t
h : (fderivWithin 𝕜 f s x).IsInvertible
M : E → E ≃L[𝕜] F
M_symm_smooth : ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(M y).symm) s x
hM : ∀ᶠ (y : E) in 𝓝[s] x, ↑(M y) = fderivWithin 𝕜 f s y
M_diff :
  ∀ (v : E),
    (fderivWithin 𝕜 (fun y ↦ ↑(M y).symm) s x) v =
      -↑(M x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(M x).symm
hMx : ↑(M x) = fderivWithin 𝕜 f s x
AV : fderivWithin 𝕜 (pullbackWithin 𝕜 f V s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (V (f y))) s x
AW : fderivWithin 𝕜 (pullbackWithin 𝕜 f W s) s x = fderivWithin 𝕜 (fun y ↦ ↑(M y).symm (W (f y))) s x
Af : DifferentiableWithinAt 𝕜 f s x
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
exact hu x hx

Goal state after:
Module: Mathlib.Analysis.Calculus.Gradient.Basic

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
x : F
L : Filter F
f₀ f₁ : F → 𝕜
f₀' f₁' : F
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : f₀' = f₁'
⊢ ∀ (x : F), ((toDual 𝕜 F) f₀') x = ((toDual 𝕜 F) f₁') x

Tactic:
by simp [h₁]

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

Goal state before:
pp: 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
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
by_cases hE : CompleteSpace E

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 : 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

case neg
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
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts

Goal state before:
pp: 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
hf' : ContinuousOn f' [[a, b]]
hg : ContinuousOn g (f '' [[a, b]])
⊢ ∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u

Tactic:
by
  refine integral_deriv_smul_comp''' hf hff' (hg.mono <| image_mono Ioo_subset_Icc_self) ?_
    (hf'.smul (hg.comp hf <| subset_preimage_image f _)).integrableOn_Icc
  rw [hf.image_uIcc] at hg ⊢
  exact hg.integrableOn_Icc

Goal state after:
Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : LocallyCompactSpace 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace F
f : E → F
inst✝ : SecondCountableTopology E
hf : Continuous f
⊢ MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}

Tactic:
by
  borelize 𝕜
  let g : (E × E) → 𝕜 → F := fun p t ↦ f (p.1 + t • p.2)
  have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)
  have M_meas : MeasurableSet {q : (E × E) × 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2} :=
    measurableSet_of_differentiableAt_with_param 𝕜 this
  exact measurable_prodMk_right M_meas

Goal state after: