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

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
⊢ ∃ β t,
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a

Tactic:
set W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y

Goal state after:
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen[instTopologicalSpaceProd] (s a)
hu : ⋃ a, s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen[inst✝³] (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen[inst✝²] (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ x ∈ T y, U x y = ⊤
W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
⊢ ∃ β t,
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
i : ι
hi : i ∈ ρ.finsupport x₀
⊢ x₀ ∈ support ⇑(ρ i)

Tactic:
exact (ρ.mem_finsupport x₀).mp hi

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

Goal state before:
pp: case succ
𝕜 : 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
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : Cₛ^n⟮I; F, V⟯
k : ℕ
ih : ⇑(k • s) = k • ⇑s
⊢ ⇑((k + 1) • s) = (k + 1) • ⇑s

Tactic:
simp_rw [succ_nsmul, ← ih]; rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.PartitionOfUnity

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i

Tactic:
by
  simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_comm ι X] using!
    exists_continuous_forall_mem_convex_of_local_const exists_forall_closedEBall_subset_aux₂
      (exists_forall_closedEBall_subset_aux₁ hK hU hKU hfin)

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case neg.left
ι : 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 := ⋯
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
⊢ j = i → IsCompact (closure (update v.toFun i vi j))

Tactic:
intro hji

Goal state after:
case neg.left
ι : 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
hji : j = i
⊢ IsCompact (closure (update v.toFun i vi j))
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_8
ι : 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)
⊢ IsCompact
    (closure
      ({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
            closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
        i))

Tactic:
simp only [update_self]
    exact hvi.2.2.2

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case h
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ i, closure (v i) ∧
    (∀ (i : ι), IsClosed ((fun i ↦ closure (v i)) i)) ∧
      (∀ (i : ι), (fun i ↦ closure (v i)) i ⊆ u i) ∧ ∀ (i : ι), IsCompact ((fun i ↦ closure (v i)) i)

Tactic:
refine ⟨?_, ?_, hv⟩

Goal state after:
case h.refine_1
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ s ⊆ ⋃ i, closure (v i)

case h.refine_2
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
v : ι → Set X
hsv : s ⊆ iUnion v
left✝ : ∀ (i : ι), IsOpen (v i)
hv : (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
⊢ ∀ (i : ι), IsClosed ((fun i ↦ closure (v i)) i)
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝³ : LocallyCompactSpace H
this✝² : LocallyCompactSpace M
this✝¹ : SecondCountableTopology H
this✝ : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
this : ∀ (n : ℕ), ∃ g, support g = v n ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1 ∧ ∀ x ∈ s, g x = 1
⊢ 0 = ∫ (x : M) in s, f x ∂μ

Tactic:
choose g g_supp g_diff g_range hg using this

Goal state after:
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
⊢ 0 = ∫ (x : M) in s, f x ∂μ
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
⊢ Tendsto (fun n ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), s.indicator f x ∂μ))

Tactic:
let bound : M → ℝ := K.indicator (fun x ↦ ‖f x‖)

Goal state after:
E : Type u_1
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
inst✝⁴ : IsManifold I ∞ M
inst✝³ : MeasurableSpace M
inst✝² : BorelSpace M
inst✝¹ : T2Space M
f : M → F
μ : Measure M
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
⊢ Tendsto (fun n ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), s.indicator f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν

Tactic:
have L'_cont : Continuous L' := LinearMap.continuous_of_finiteDimensional _

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this✝ : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous ⇑M.symm
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous ⇑P
I : Function.Bijective ⇑(L.domRestrict T)
L' : ↥T ≃ₗ[𝕜] F := LinearEquiv.ofBijective (L.domRestrict T) I
L'_cont : Continuous ⇑L'
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
p : E
this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (fun t ↦ s + t) 0
⊢ LineDifferentiableAt ℝ f (p + s • v) v

Tactic:
simp only [LineDifferentiableAt]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
p : E
this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s
h's : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (fun t ↦ s + t) 0
⊢ DifferentiableAt ℝ (fun t ↦ f (p + s • v + t • v)) 0
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
S1 : ∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ
⊢ ∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ =
    ∑ i ∈ s, ∫ (a_1 : E), g a_1 * (a i * lineDeriv ℝ f a_1 (v i)) ∂μ

Tactic:
← mul_assoc,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
ι : Type u_3
s : Finset ι
a : ι → ℝ
v : ι → E
g : E → ℝ
g_smooth : ContDiff ℝ (↑⊤) g
g_comp : HasCompactSupport g
A : ∀ i ∈ s, Integrable (fun x ↦ g x • (a i • fun x ↦ lineDeriv ℝ f x (v i)) x) μ
S1 : ∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ
⊢ ∫ (x : E), g x * lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ =
    ∑ x ∈ s, ∫ (a_1 : E), g a_1 * a x * lineDeriv ℝ f a_1 (v x) ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x

Tactic:
have h {a b : ℝ} : ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t :=
    integral_Icc_eq_integral_Ioc (x := a) (y := b) (X := ℝ) |>.symm

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
⊢ ∀ᵐ (x : ℝ), ∀ (c : ℝ), HasDerivAt (fun x ↦ ∫ (t : ℝ) in c..x, f t) (f x) x
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
hs : s.Countable
⊢ ∀ᵐ (x : E) ∂μ, ∃ L, ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v

Tactic:
by
  have B := Basis.ofVectorSpace ℝ E
  have I1 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, lineDeriv ℝ f x (∑ i, (B.repr v i) • B i) =
                                  ∑ i, B.repr v i • lineDeriv ℝ f x (B i) :=
    (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDeriv_sum_eq _ _ _)
  have I2 : ∀ᵐ (x : E) ∂μ, ∀ v ∈ s, LineDifferentiableAt ℝ f x v :=
    (ae_ball_iff hs).2 (fun v _ ↦ hf.ae_lineDifferentiableAt v)
  filter_upwards [I1, I2] with x hx h'x
  let L : StrongDual ℝ E :=
    LinearMap.toContinuousLinearMap (B.constr ℝ (fun i ↦ lineDeriv ℝ f x (B i)))
  refine ⟨L, fun v hv ↦ ?_⟩
  have J : L v = lineDeriv ℝ f x v := by convert! (hx v hv).symm <;> simp [L, B.sum_repr v]
  simpa [J] using (h'x v hv).hasLineDerivAt

Goal state after:
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.comp (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:
map_add,

Goal state after:
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 x)
        ((PolynomialModule.comp (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₀
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 : ℝ
⊢ taylorWithinEval f (n + 1) s x₀ x =
    taylorWithinEval f n s x₀ x + (((↑n + 1) * ↑n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀

Tactic:
by
  simp_rw [taylorWithinEval, taylorWithin_succ, map_add, PolynomialModule.comp_eval]
  congr
  simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C,
    PolynomialModule.eval_single, mul_inv_rev]
  dsimp only [taylorCoeffWithin]
  rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one,
    mul_inv_rev]

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

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
⊢ eVariationOn f (Icc x y) ≤ 1

Tactic:
simp only [eVariationOn, iSup_le_iff]

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ 1
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) / ↑n ! * (x - a) ^ (n + 1)

Tactic:
rw [div_mul_eq_mul_div₀]

Goal state after:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / ↑n !
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
⊢ ∃ C, ∀ x ∈ uIcc a b, f x = C

Tactic:
suffices ∀ x ∈ uIcc a b, f x = f b by use f b

Goal state after:
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
⊢ ∀ x ∈ uIcc a b, f x = f b