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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i, μ s / ↑N ≤ ∑ i, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
l : α
hl : l ∈ ↑(Finset.image (fun x ↦ ↑↑x) w)
k' : ↑(u i)
left✝ : k' ∈ w
hk : ↑↑k' ∈ ↑(Finset.image (fun x ↦ ↑↑x) w)
hkl : ↑↑k' ≠ l
⊢ ∃ l' ∈ w, ↑↑l' = l

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i, μ s / ↑N ≤ ∑ i, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
l : α
hl : l ∈ ↑(Finset.image (fun x ↦ ↑↑x) w)
k' : ↑(u i)
left✝ : k' ∈ w
hk : ↑↑k' ∈ ↑(Finset.image (fun x ↦ ↑↑x) w)
hkl : ↑↑k' ≠ l
⊢ ∃ l' ∈ w, ↑↑l' = l
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
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
⊢ ‖a.c j‖ ≤ 2 ↔ False

Tactic:
simpa using

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
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
⊢ 2 < ‖a.c j‖
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
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
⊢ ‖a.c i‖ ≤ 2 ↔ False

Tactic:
simpa using

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
hδ2 : δ ≤ 1
c' : Fin N.succ → E := fun i ↦ if ‖a.c i‖ ≤ 2 then a.c i else (2 / ‖a.c i‖) • a.c i
norm_c'_le : ∀ (i : Fin N.succ), ‖c' i‖ ≤ 2
i j : Fin N.succ
inej : i ≠ j
hij : ‖a.c i‖ ≤ ‖a.c j‖
Hj : 2 < ‖a.c j‖
H'j : ‖a.c j‖ ≤ 2 ↔ False
Hi : 2 < ‖a.c i‖
⊢ 2 < ‖a.c i‖
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : 0 ≤ r
⊢ HolderOnWith (C * D ^ (↑r - ↑0)) 0 f A

Tactic:
simpa using

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : 0 ≤ r
⊢ HolderOnWith (C * D ^ ↑r) 0 f A
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
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD
gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B ∘SL ↑↑isoE).flip ∘SL ↑↑isoF).flip
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
Bu_eq : (fun y ↦ (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y ↦ (B (f y)) (g y)) ∘ ⇑isoD
Bu_le : ‖Bu‖ ≤ ‖B‖
su : Set Du := ⇑isoD ⁻¹' s
hsu : UniqueDiffOn 𝕜 su
xu : Du := isoD.symm x
⊢ xu ∈ su

Tactic:
simpa using

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
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD
gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B ∘SL ↑↑isoE).flip ∘SL ↑↑isoF).flip
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
Bu_eq : (fun y ↦ (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y ↦ (B (f y)) (g y)) ∘ ⇑isoD
Bu_le : ‖Bu‖ ≤ ‖B‖
su : Set Du := ⇑isoD ⁻¹' s
hsu : UniqueDiffOn 𝕜 su
xu : Du := isoD.symm x
⊢ x ∈ s
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : ↑s ≤ ↑r
ht : 0 < s
hr : 0 < ↑r
θ₁ : ℝ≥0 := NNReal.mk (↑s / ↑r) ⋯
⊢ 0 ≤ 1 - ↑s / ↑r

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : ↑s ≤ ↑r
ht : 0 < s
hr : 0 < ↑r
θ₁ : ℝ≥0 := NNReal.mk (↑s / ↑r) ⋯
⊢ ↑s / ↑r ≤ 1
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
f : E → F
a : E
h : ContDiffAt ℝ (↑k) f a
⊢ (fun x ↦ iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑0

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
f : E → F
a : E
h : ContDiffAt ℝ (↑k) f a
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 a) fun x ↦ ‖iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a‖
Module: Mathlib.Analysis.Calculus.Darboux

Goal state before:
pp: f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' s

Tactic:
rcases le_total a b with hab | hab

Goal state after:
case inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s

case inr
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ m ∈ f' '' s
Module: Mathlib.Analysis.Calculus.Darboux

Goal state before:
pp: case inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s

Tactic:
have : Icc a b ⊆ s := hs.out ha hb

Goal state after:
case inl
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
⊢ m ∈ f' '' s
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
k : ℕ
α : ↑I
f : E → F
a : E
g : F ≃L[ℝ] G
h : ContDiffPointwiseHolderAt k α (⇑g ∘ f) a
⊢ ContDiffPointwiseHolderAt k α f a

Tactic:
simpa using

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
k : ℕ
α : ↑I
f : E → F
a : E
g : F ≃L[ℝ] G
h : ContDiffPointwiseHolderAt k α (⇑g ∘ f) a
⊢ ContDiffPointwiseHolderAt k α f a
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k l : ℕ
α : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
hl : l < k
⊢ (fun x ↦ ‖iteratedFDeriv ℝ l (fderiv ℝ f) x - iteratedFDeriv ℝ l (fderiv ℝ f) a‖) =O[𝓝 a] fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k l : ℕ
α : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
hl : l < k
⊢ (fun x ↦ dist (iteratedFDeriv ℝ l (fderiv ℝ f) x) (iteratedFDeriv ℝ l (fderiv ℝ f) a)) =O[𝓝 a] fun x ↦ dist x a ^ ↑α
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case zero
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
l : ℕ
hl : l + 0 ≤ k
⊢ ContDiffPointwiseHolderAt l α (iteratedFDeriv ℝ 0 f) a

Tactic:
simpa using

Goal state after:
case zero
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
l : ℕ
hl : l + 0 ≤ k
⊢ ContDiffPointwiseHolderAt l α f a
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
m : ℕ
ihm : ∀ {l : ℕ}, l + m ≤ k → ContDiffPointwiseHolderAt l α (iteratedFDeriv ℝ m f) a
l : ℕ
hl : l + 1 + m ≤ k
⊢ ContDiffPointwiseHolderAt l α (iteratedFDeriv ℝ (m + 1) f) a

Tactic:
simpa using

Goal state after:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
m : ℕ
ihm : ∀ {l : ℕ}, l + m ≤ k → ContDiffPointwiseHolderAt l α (iteratedFDeriv ℝ m f) a
l : ℕ
hl : l + 1 + m ≤ k
⊢ ContDiffPointwiseHolderAt l α (fderiv ℝ (iteratedFDeriv ℝ m f)) a
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x ↦ |x|) (↑(SignType.sign x)) x

Tactic:
simpa using

Goal state after:
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun x ↦ |x|) (-1) x
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun x ↦ |x|) (↑(SignType.sign x)) x

Tactic:
simpa using

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun x ↦ |x|) 1 x
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: case inl
⊢ deriv (fun x ↦ |x|) 0 = ↑(SignType.sign 0)

Tactic:
simpa using

Goal state after:
case inl
⊢ deriv (fun x ↦ |x|) 0 = 0
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: case inr
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x ↦ |x|) x = ↑(SignType.sign x)

Tactic:
simpa using

Goal state after:
case inr
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x ↦ |x|) x = ↑(SignType.sign x)
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
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : α → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : ↑v ⊆ s'
hμv : μ (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s'
hv : (↑v).PairwiseDisjoint fun x ↦ closedBall x (r x)
⊢ ∀ p ∈ t ∪ Finset.image (fun x ↦ (x, r x)) v, p.2 ∈ f p.1

Tactic:
intro p hp
      rcases Finset.mem_union.1 hp with (h'p | h'p)
      · exact ht.2.2 p h'p
      · rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩
        exact (hr p' (vs' p'v)).1.1

Goal state after:
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 : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ (B (f y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
by
  simp_rw [← iteratedFDerivWithin_univ]
  exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
    (mem_univ x) hn

Goal state after:
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
f' : F
inst✝ : TrivialStar 𝕜
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (fun x ↦ star (f x)) (star f') L

Tactic:
simpa using

Goal state after:
𝕜 : 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
f' : F
inst✝ : TrivialStar 𝕜
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (fun x ↦ star (f x)) (star f') L
Module: Mathlib.Analysis.Calculus.FDeriv.Star

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : StarRing 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : StarModule 𝕜 F
inst✝⁴ : ContinuousStar F
inst✝³ : StarAddMonoid E
inst✝² : StarModule 𝕜 E
inst✝¹ : ContinuousStar E
inst✝ : NormedStarGroup 𝕜
f : E → F
z : E
f' : E →L[𝕜] F
hf : HasFDerivAt f f' z
⊢ HasFDerivAt f f' (↑(starL 𝕜) (star z))

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : StarRing 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : StarModule 𝕜 F
inst✝⁴ : ContinuousStar F
inst✝³ : StarAddMonoid E
inst✝² : StarModule 𝕜 E
inst✝¹ : ContinuousStar E
inst✝ : NormedStarGroup 𝕜
f : E → F
z : E
f' : E →L[𝕜] F
hf : HasFDerivAt f f' z
⊢ HasFDerivAt f f' z
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
u : Finset ι
f : ι → E → A'
N : ℕ∞ω
hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun x ↦ ∏ j ∈ u, f j x) x‖ ≤
    ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
u : Finset ι
f : ι → E → A'
N : ℕ∞ω
hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun x ↦ ∏ j ∈ u, f j x) x‖ ≤
    ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
this : 1 ≤ n + 1
⊢ 0 ≤ D

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
this : 1 ≤ n + 1
⊢ 0 ≤ D
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₁)

Goal state after:
case refine_2.hf'
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
⊢ DifferentiableOn ℝ f (interior (Ico b c))

case refine_2.hf'_nonneg
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
⊢ ∀ x ∈ interior (Ico b c), 0 ≤ deriv f x
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

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
n : ℕ
f : E →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 2) → E
⊢ (alternatizeUncurryFin (alternatizeUncurryFinCLM 𝕜 E F ∘SL f)) v =
    ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
            ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

Tactic:
simpa using

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
n : ℕ
f : E →L[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 2) → E
⊢ ∑ x, (-1) ^ ↑x • ∑ i, (-1) ^ ↑i • ((f (v x)) (x.removeNth v i)) (i.removeNth (x.removeNth v)) =
    ∑ i,
      ∑ j ≥ i,
        (-1) ^ (↑i + ↑j) •
          (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
            ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in 𝓝 x₀, sign (f x) = sign (x₀ - x)

Tactic:
simpa using

Goal state after:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in 𝓝 x₀, sign (f x) = sign (x₀ - x)