mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_1
X : Type v
inst✝ : TopologicalSpace X
ι : X → Sort u_1
p : (x : X) → ι x → Prop
s : (x : X) → ι x → Set X
hb : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h :
  ∀ (f : (x : X) → ι x),
    (∀ (x : X), p x (f x)) →
      ∃ β t, (∀ (b : β), IsOpen[inst✝] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ x, t b ⊆ s x (f x)
α : Type v
S : α → Set X
ho : ∀ (a : α), IsOpen[inst✝] (S a)
hu : ⋃ a, S a = univ
a : X → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst✝] (t b)
ht : ⋃ b, t b = univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ x, t b ⊆ s x (f x)
⊢ ⋃ x, ⋃ (hx : x ∈ range t), ↑⟨x, hx⟩ = univ

Tactic:
biUnion_range

Goal state after:
case refine_1
X : Type v
inst✝ : TopologicalSpace X
ι : X → Sort u_1
p : (x : X) → ι x → Prop
s : (x : X) → ι x → Set X
hb : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h :
  ∀ (f : (x : X) → ι x),
    (∀ (x : X), p x (f x)) →
      ∃ β t, (∀ (b : β), IsOpen[inst✝] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ x, t b ⊆ s x (f x)
α : Type v
S : α → Set X
ho : ∀ (a : α), IsOpen[inst✝] (S a)
hu : ⋃ a, S a = univ
a : X → α
f : (x : X) → ι x
hp : ∀ (x : X), p x (f x)
hsub : ∀ (x : X), s x (f x) ⊆ S (a x)
β : Type u
t : β → Set X
hto : ∀ (b : β), IsOpen[inst✝] (t b)
ht : ⋃ b, t b = univ
htf : LocallyFinite t
hts : ∀ (b : β), ∃ x, t b ⊆ s x (f x)
⊢ ⋃ y, t y = univ
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
i : ι
hi : i ∈ chainSupCarrier c
v : PartialRefinement u s p
hv : i ∈ ⋃ (_ : v ∈ c), v.carrier
⊢ p ((find c ne i).toFun i)

Tactic:
simp only [mem_iUnion, exists_prop] at hv

Goal state after:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite
hU : s ⊆ ⋃ i, u i
i : ι
hi : i ∈ chainSupCarrier c
v : PartialRefinement u s p
hv : v ∈ c ∧ i ∈ v.carrier
⊢ p ((find c ne i).toFun i)
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case mk.mk
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type u_1
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i ↦ support ⇑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
sum_eq_one'✝¹ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝¹ i) x = 1
sum_le_one'✝¹ : ∀ (x : X), ∑ᶠ (i : ι), (toFun✝¹ i) x ≤ 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
sum_eq_one'✝ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : X), ∑ᶠ (i : ι), (toFun✝ i) x ≤ 1
h :
  { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, sum_eq_one' := sum_eq_one'✝¹,
        sum_le_one' := sum_le_one'✝¹ }.toFun =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
        sum_le_one' := sum_le_one'✝ }.toFun
⊢ { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, sum_eq_one' := sum_eq_one'✝¹,
      sum_le_one' := sum_le_one'✝¹ } =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
      sum_le_one' := sum_le_one'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
j : ι
hj : ¬j = i ∧ j ∉ v.carrier
⊢ v.toFun j = u j

Tactic:
v.apply_eq hj.2

Goal state after:
case refine_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
j : ι
hj : ¬j = i ∧ j ∉ v.carrier
⊢ u j = u j
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: case mk.mk
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
toFun✝¹ : ι → C(X, ℝ)
locallyFinite'✝¹ : LocallyFinite fun i ↦ support ⇑(toFun✝¹ i)
nonneg'✝¹ : 0 ≤ toFun✝¹
le_one'✝¹ : toFun✝¹ ≤ 1
eventuallyEq_one'✝¹ : ∀ x ∈ s, ∃ i, ⇑(toFun✝¹ i) =ᶠ[𝓝 x] 1
toFun✝ : ι → C(X, ℝ)
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : 0 ≤ toFun✝
le_one'✝ : toFun✝ ≤ 1
eventuallyEq_one'✝ : ∀ x ∈ s, ∃ i, ⇑(toFun✝ i) =ᶠ[𝓝 x] 1
h :
  { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, le_one' := le_one'✝¹,
        eventuallyEq_one' := eventuallyEq_one'✝¹ }.toFun =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
        eventuallyEq_one' := eventuallyEq_one'✝ }.toFun
⊢ { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, le_one' := le_one'✝¹,
      eventuallyEq_one' := eventuallyEq_one'✝¹ } =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, le_one' := le_one'✝,
      eventuallyEq_one' := eventuallyEq_one'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝² : TopologicalSpace (TotalSpace F V)
inst✝¹ : (x : M) → TopologicalSpace (V x)
inst✝ : FiberBundle F V
toFun✝¹ : (x : M) → V x
contMDiff_toFun✝¹ : ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x ↦ ⟨x, toFun✝¹ x⟩
toFun✝ : (x : M) → V x
contMDiff_toFun✝ : ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x ↦ ⟨x, toFun✝ x⟩
h :
  { toFun := toFun✝¹, contMDiff_toFun := contMDiff_toFun✝¹ }.toFun =
    { toFun := toFun✝, contMDiff_toFun := contMDiff_toFun✝ }.toFun
⊢ { toFun := toFun✝¹, contMDiff_toFun := contMDiff_toFun✝¹ } = { toFun := toFun✝, contMDiff_toFun := contMDiff_toFun✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
ι : Type uι
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
F : Type uF
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s✝ : Set M
f : SmoothPartitionOfUnity ι I M s✝
n : ℕ∞
s : Set M
toFun✝¹ : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite'✝¹ : LocallyFinite fun i ↦ support ⇑(toFun✝¹ i)
nonneg'✝¹ : ∀ (i : ι) (x : M), 0 ≤ (toFun✝¹ i) x
sum_eq_one'✝¹ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝¹ i) x = 1
sum_le_one'✝¹ : ∀ (x : M), ∑ᶠ (i : ι), (toFun✝¹ i) x ≤ 1
toFun✝ : ι → C^∞⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite'✝ : LocallyFinite fun i ↦ support ⇑(toFun✝ i)
nonneg'✝ : ∀ (i : ι) (x : M), 0 ≤ (toFun✝ i) x
sum_eq_one'✝ : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : M), ∑ᶠ (i : ι), (toFun✝ i) x ≤ 1
h :
  { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, sum_eq_one' := sum_eq_one'✝¹,
        sum_le_one' := sum_le_one'✝¹ }.toFun =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
        sum_le_one' := sum_le_one'✝ }.toFun
⊢ { toFun := toFun✝¹, locallyFinite' := locallyFinite'✝¹, nonneg' := nonneg'✝¹, sum_eq_one' := sum_eq_one'✝¹,
      sum_le_one' := sum_le_one'✝¹ } =
    { toFun := toFun✝, locallyFinite' := locallyFinite'✝, nonneg' := nonneg'✝, sum_eq_one' := sum_eq_one'✝,
      sum_le_one' := sum_le_one'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case neg.right
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : ¬j = i
hjmemv : j ∈ v.carrier
⊢ IsCompact (closure (update v.toFun i vi j))

Tactic:
rw [update_of_ne h]

Goal state after:
case neg.right
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : ¬j = i
hjmemv : j ∈ v.carrier
⊢ IsCompact (closure (v.toFun j))
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_5
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : ¬j = i ∧ j ∉ v.carrier
⊢ v.toFun j = u j

Tactic:
v.apply_eq hj.2

Goal state after:
case refine_5
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : ¬j = i ∧ j ∉ v.carrier
⊢ u j = u j
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1

Tactic:
rcases ht.isOpen_compl.exists_contMDiff_support_eq I with ⟨g, g_supp, g_diff, g_pos⟩

Goal state after:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s t : Set M
hs : IsOpen[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.68) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : ContMDiff I 𝓘(ℝ, ℝ) (↑?m.109) g
g_pos : ∀ (x : M), 0 ≤ g x
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) (↑n) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f g : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
hg : AbsolutelyContinuousOnInterval g a b
⊢ Tendsto ?m.14 (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) (𝓝 0)

Tactic:
by simpa using Tendsto.add hf hg

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

Goal state before:
pp: case e'_3
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ comap (fun x ↦ (1, fun x_1 ↦ x)) totalLengthFilter ⊓ 𝓟 (uIcc a b ×ˢ uIcc a b) =
    comap ?convert_2 totalLengthFilter ⊓ 𝓟 (?convert_2 ⁻¹' disjWithin a b)

Tactic:
congr

Goal state after:
case e_a
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf :
  totalLengthFilter ⊓ 𝓟 (disjWithin a b) ≤
    comap (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (𝓝 0)
⊢ uIcc a b ×ˢ uIcc a b = (fun x ↦ (1, fun x_1 ↦ x)) ⁻¹' disjWithin a b
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (PolynomialModule.eval (Polynomial.eval x (Polynomial.X - Polynomial.C x₀)))
        (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀)) =
    (PolynomialModule.eval x) (taylorWithin f n s x₀) +
      (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀

Tactic:
congr

Goal state after:
case e_a
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval (Polynomial.eval x (Polynomial.X - Polynomial.C x₀)))
      (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀)) =
    (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}

Tactic:
obtain ⟨y, yq, hy⟩ : ∃ y ∈ q, ‖w - y‖ < δ := by simpa [← dist_eq_norm] using hq w_mem

Goal state after:
case inr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
⊢ v ∈ {x_1 | (fun x_2 ↦ ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖f (x + ρ • w) - f x - ρ • L w‖ =
    ‖f (x + ρ • w) - f (x + ρ • y) + (ρ • L y - ρ • L w) + (f (x + ρ • y) - f x - ρ • L y)‖

Tactic:
congr

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ f (x + ρ • w) - f x - ρ • L w = f (x + ρ • w) - f (x + ρ • y) + (ρ • L y - ρ • L w) + (f (x + ρ • y) - f x - ρ • L y)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: a b : ℝ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
hf : ContDiffOn ℝ 1 f (uIcc a b)
⊢ AbsolutelyContinuousOnInterval f a b

Tactic:
obtain ⟨K, hK⟩ := hf.exists_lipschitzOnWith (by decide) (convex_Icc _ _) isCompact_Icc
  exact hK.absolutelyContinuousOnInterval

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

Goal state before:
pp: case succ.inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h : ∀ {f : ℝ → E}, ContDiffOn ℝ (↑n) f s → (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n + 1) f s
x : ℝ
hx : x ∈ s
⊢ HasDerivWithinAt (fun x ↦ f x - taylorWithinEval f (n + 1) s x₀ x)
    (derivWithin f s x - taylorWithinEval (derivWithin f s) n s x₀ x) s x

Tactic:
refine HasDerivWithinAt.sub ?_ (hasDerivAt_taylorWithinEval_succ f n).hasDerivWithinAt

Goal state after:
case succ.inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x₀ : ℝ
s : Set ℝ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
n : ℕ
h : ∀ {f : ℝ → E}, ContDiffOn ℝ (↑n) f s → (fun x ↦ f x - taylorWithinEval f n s x₀ x) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n
f : ℝ → E
hs' : UniqueDiffOn ℝ s
hf : ContDiffOn ℝ (↑n + 1) f s
x : ℝ
hx : x ∈ s
⊢ HasDerivWithinAt f (derivWithin f s x) s x
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun y ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !

Tactic:
simp only [taylorWithinEval_self] at this

Goal state after:
case inr
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b C x : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
hx : x ∈ Icc a b
hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C
h : a < b
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)
h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C
A :
  ∀ t ∈ Icc a x,
    HasDerivWithinAt (fun y ↦ taylorWithinEval f n (Icc a b) y x)
      (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t
this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ LipschitzOnWith ?C (⇑A ∘ f) s

pp: case C
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
s : Set E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
hf : LipschitzOnWith C f s
A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ
⊢ ℝ≥0

Tactic:
exact A.lipschitz.comp_lipschitzOnWith hf

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

Goal state before:
pp: case inr.zero
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this : x₀ ≠ x
hf :
  ∀ k ≤ 0,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ f x - taylorWithinEval f 0 [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ 0 / ↑0!) • iteratedDerivWithin (0 + 1) f [[x₀, x]] t

Tactic:
simp only [taylor_within_zero_eval, pow_zero, Nat.factorial_zero, Nat.cast_one, ne_eq,
      one_ne_zero, not_false_eq_true, div_self, zero_add, iteratedDerivWithin_one, one_smul]
    simp only [nonpos_iff_eq_zero, sub_self, deriv_div_const, forall_eq, pow_zero,
      Nat.factorial_zero, Nat.cast_one, ne_eq, one_ne_zero, not_false_eq_true, div_self,
      iteratedDerivWithin_zero, one_smul, deriv_const', div_one, zero_smul,
      intervalIntegral.integral_zero, sub_zero] at hf
    rw [← hf]
    refine intervalIntegral.integral_congr_uIoo fun _ ⟨h1, h2⟩ => ?_
    rw [← derivWithin_of_mem_nhds <| Icc_mem_nhds h1 h2]
    rfl

Goal state after: