mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (contMDiffCoordChange n IB a he he' b) v).1 = (↑e.symm (b, v)).proj

pp: case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e.symm (b, v)).proj ∈ e'.baseSet

Tactic:
e.proj_symm_apply' hb.1

Goal state after:
case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (contMDiffCoordChange n IB a he he' b) v).1 = b

case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e.symm (b, v)).proj ∈ e'.baseSet
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : EqOn (writtenInExtChartAt I I (Sum.inr x) Sum.swap) id t
⊢ t ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))

Tactic:
Filter.inter_mem_iff

Goal state after:
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : EqOn (writtenInExtChartAt I I (Sum.inr x) Sum.swap) id t
⊢ ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x)) ∧
    range ↑I ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inr x)) (Sum.inr x))
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑e.symm (b, v)).proj ∈ e'.baseSet

Tactic:
e.proj_symm_apply' hb.1

Goal state after:
case fst
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
e e' : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
he' : e' ∈ a.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ e'.baseSet
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, 𝕜) n (Prod.fst ∘ id) ∧
    ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n (Prod.snd ∘ id)

Tactic:
← contMDiff_prod_iff

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, E)) n id
Module: Mathlib.Geometry.Manifold.Algebra.SMul

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, E →L[𝕜] E) n (Prod.fst ∘ id) ∧
    ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) 𝓘(𝕜, E) n (Prod.snd ∘ id)

Tactic:
← contMDiff_prod_iff

Goal state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹⁴ : TopologicalSpace H
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
H' : Type u_4
inst✝¹¹ : TopologicalSpace H'
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
H'' : Type u_6
inst✝⁸ : TopologicalSpace H''
E'' : Type u_7
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
I'' : ModelWithCorners 𝕜 E'' H''
G : Type u_8
inst✝⁵ : TopologicalSpace G
inst✝⁴ : ChartedSpace H G
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H' M
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H'' N
n : ℕ∞ω
⊢ ContMDiff (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) (𝓘(𝕜, E →L[𝕜] E).prod 𝓘(𝕜, E)) n id
Module: Mathlib.Geometry.Manifold.BumpFunction

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
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
tsupport,

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
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ closure[inst✝³] (support ↑f) ⊆ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_2
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ⋃ i, (fun i ↦ ⋃ a, ⋃ (_ : ind a = i), t a) i = univ

Tactic:
simp only [eq_univ_iff_forall, mem_iUnion]

Goal state after:
case refine_2
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
⊢ ∀ (x : X), ∃ i i_1, ∃ (_ : ind i_1 = i), x ∈ t i_1
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
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedEBall y r ⊆ U i}

Tactic:
refine ⟨r, hr.mono fun y hy => ⟨hr0, ?_⟩⟩

Goal state after:
ι : 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
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι), (ENNReal.ofReal x_1, y).2 ∈ K i → closedEBall (ENNReal.ofReal x_1, y).2 (ENNReal.ofReal x_1, y).1 ⊆ U i
r : ℝ
hr0 : 0 < r
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).2 ∈ K i → closedEBall (ENNReal.ofReal r, y).2 (ENNReal.ofReal r, y).1 ⊆ U i
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | closedEBall y r ⊆ U i}
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
ι : Type uι
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✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed[inst✝⁵] s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst✝⁵] (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
⊢ Disjoint s t → ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
hd

Goal state after:
case refine_1
ι : Type uι
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✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed[inst✝⁵] s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst✝⁵] (U i)
hU : s✝ ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁵] s
ht : IsClosed[inst✝⁵] t
hd : Disjoint s t
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ support (f ∘ ↑I) = s

Tactic:
rw [support_comp_eq_preimage, f_supp, ← preimage_comp]

Goal state after:
case refine_1
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type uH
inst✝¹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set H
hs : IsOpen[inst✝¹] s
h's : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑I.symm ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑I.symm ⁻¹' s
f_diff : ContDiff ℝ (↑?m.76) f
f_range : range f ⊆ Icc 0 1
⊢ ↑I.symm ∘ ↑I ⁻¹' s = s
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: case refine_1
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ∞ → IntegrableOn f s ((μ.restrict t).trim hm)

pp: case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ∞ → ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 0

Tactic:
· intro s hs hμs
    unfold IntegrableOn
    rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
    rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs,
      trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs
    refine Integrable.trim hm ?_ hf_meas_m
    exact hf_int_finite _ (hs.inter ht_meas) hμs

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero✝ : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᵐ[μ.restrict tᶜ] 0
hf_meas_m : StronglyMeasurable f
⊢ ∀ (s : Set α), MeasurableSet s → ((μ.restrict t).trim hm) s < ∞ → ∫ (x : α) in s, f x ∂(μ.restrict t).trim hm = 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 • fun x ↦ lineDeriv ℝ f x (v i)) a_1 ∂μ

Tactic:
dsimp only [smul_eq_mul, Pi.smul_apply]

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) ∂μ =
    ∑ i ∈ s, ∫ (a_1 : E), g a_1 * (a i * lineDeriv ℝ f a_1 (v i)) ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope

Goal state before:
pp: case inr
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (Icc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 < c
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a

Tactic:
← uIcc_of_le (by linarith)

Goal state after:
case inr
f : ℝ → ℝ
a b c : ℝ
hf : MonotoneOn f (uIcc a (b + c))
hab : a ≤ b
hc✝ : 0 ≤ c
hc : 0 < c
⊢ ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ -∫ (x : ℝ) in b..a, deriv f x ∈ Icc (f b - f a) 0

Tactic:
refine neg_mem_Icc_iff.mpr ?_

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ ∫ (x : ℝ) in b..a, deriv f x ∈ Icc (-0) (-(f b - f a))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case _a
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
a b c d : ℝ
hf :
  map (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b)) ≤ 𝓝 0
habcd : uIcc c d ⊆ uIcc a b
⊢ disjWithin c d ⊆ disjWithin a b

Tactic:
exact disjWithin_mono habcd

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
n : ℕ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hf : ContDiffOn ℝ (↑n) f s
hf' : DifferentiableWithinAt ℝ (iteratedDerivWithin n f s) s y
⊢ HasDerivWithinAt (fun t ↦ taylorWithinEval f n s t x) (((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f s y)
    s' y

Tactic:
have hs'_unique : UniqueDiffWithinAt ℝ s' y :=
    UniqueDiffWithinAt.mono_nhds (hs_unique _ (h hy)) (nhdsWithin_le_iff.mpr hs')
  induction n with
  | zero =>
    simp only [taylor_within_zero_eval, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero,
      mul_one, zero_add, one_smul]
    simp only [iteratedDerivWithin_zero] at hf'
    rw [iteratedDerivWithin_one]
    exact hf'.hasDerivWithinAt.mono h
  | succ k hk =>
    simp_rw [Nat.add_succ, taylorWithinEval_succ]
    simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one]
    have coe_lt_succ : (k : WithTop ℕ) < k.succ := Nat.cast_lt.2 k.lt_succ_self
    have hdiff : DifferentiableOn ℝ (iteratedDerivWithin k f s) s' :=
      (hf.differentiableOn_iteratedDerivWithin (mod_cast coe_lt_succ) hs_unique).mono h
    specialize hk hf.of_succ ((hdiff y hy).mono_of_mem_nhdsWithin hs')
    convert!
      hk.add
        (hasDerivWithinAt_taylor_coeff_within hs'_unique (nhdsWithin_mono _ h self_mem_nhdsWithin)
          hf') using 1
    exact (add_sub_cancel _ _).symm

Goal state after:
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
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
h : LipschitzWith C f
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
by
  rw [← lipschitzOnWith_univ] at h
  simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem

Goal state after:
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 ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
⊢ d ∈ Icc a b → f d = f b

Tactic:
hd

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 ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : d ∈ Icc a b
⊢ f d = f b