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

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
this : T1Space M
hf : HasMFDerivAt[s] f x f'
⊢ HasMFDerivAt[insert y s] f x f'

Tactic:
rcases eq_or_ne x y with rfl | h

Goal state after:
case inl
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
this : T1Space M
hf : HasMFDerivAt[s] f x f'
⊢ HasMFDerivAt[insert x s] f x f'

case inr
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
this : T1Space M
hf : HasMFDerivAt[s] f x f'
h : x ≠ y
⊢ HasMFDerivAt[insert y s] f x f'
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁰ : NontriviallyNormedField R
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module R (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace R F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → TopologicalSpace (E x)
inst✝² : FiberBundle F E
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((continuousLinearEquivAt R e b ⋯).symm.trans (continuousLinearEquivAt R e' b ⋯)) v = (coordChangeL R e e' b) v

Tactic:
rw [coordChangeL_apply e e' hb]

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝¹⁰ : NontriviallyNormedField R
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module R (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace R F
inst✝⁵ : TopologicalSpace B
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → TopologicalSpace (E x)
inst✝² : FiberBundle F E
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((continuousLinearEquivAt R e b ⋯).symm.trans (continuousLinearEquivAt R e' b ⋯)) v =
    (↑e' { proj := b, snd := e.symm b v }).2
Module: Mathlib.Geometry.Manifold.MFDeriv.Basic

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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hz : z ∈ ↑(extChartAt I x).symm ⁻¹' u ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ)
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
⊢ (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) z ↔ (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) z

Tactic:
change z ∈ (extChartAt I x).symm ⁻¹' s ∩ range I ↔ z ∈ (extChartAt I x).symm ⁻¹' t ∩ range I

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
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hz : z ∈ ↑(extChartAt I x).symm ⁻¹' u ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ)
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
⊢ z ∈ ↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I ↔ z ∈ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
Module: Mathlib.Topology.VectorBundle.Basic

Goal state before:
pp: R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i✝ j i i' : ι
⊢ ContinuousOn
    (fun b ↦ ↑(Trivialization.coordChangeL R (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)

Tactic:
refine (Z.continuousOn_coordChange i i').congr fun b hb => ?_

Goal state after:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁸ : NontriviallyNormedField R
inst✝⁷ : (x : B) → AddCommMonoid (E x)
inst✝⁶ : (x : B) → Module R (E x)
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace R F
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace (TotalSpace F E)
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b✝ : B
a : F
i✝ j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
⊢ ↑(Trivialization.coordChangeL R (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b) =
    Z.coordChange i i' b
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedSpace 𝕜 F
inst✝¹⁰ : TopologicalSpace (TotalSpace F E)
inst✝⁹ : (x : B) → TopologicalSpace (E x)
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✝³ : FiberBundle F E
inst✝² : (x : B) → AddCommMonoid (E x)
inst✝¹ : (x : B) → Module 𝕜 (E x)
inst✝ : VectorBundle 𝕜 F E
⊢ ContMDiff IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E)

Tactic:
by
  intro x
  unfold zeroSection
  rw [contMDiffAt_section]
  apply (contMDiffAt_const (c := 0)).congr_of_eventuallyEq
  filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds
    (mem_baseSet_trivializationAt F E x)] with y hy
    using congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy

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

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
n : ℕ∞ω
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedSpace 𝕜 E'
H : Type u_4
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_6
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
this : IsManifold I (0 + 1) M
i j k : ↑(atlas H M)
x✝ : M
hxk : x✝ ∈ (↑k).source
hxi : x✝ ∈ (↑i).source
hxj : x✝ ∈ (↑j).source
v x : E
a✝ : x ∈ range ↑I
⊢ (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) x ∈ range ↑I

Tactic:
exact mem_range_self _

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

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
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
EM : Type u_9
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst✝ : Z.IsContMDiff IB n
⊢ ∀ (e e' : Trivialization F TotalSpace.proj) [inst : MemTrivializationAtlas e] [inst_1 : MemTrivializationAtlas e'],
    ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)

Tactic:
rintro - - ⟨i, rfl⟩ ⟨i', rfl⟩

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
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
EM : Type u_9
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
inst✝⁹ : (x : B) → AddCommMonoid (E x)
inst✝⁸ : (x : B) → Module 𝕜 (E x)
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
ι : Type u_11
Z : VectorBundleCore 𝕜 B F ι
inst✝ : Z.IsContMDiff IB n
i i' : ι
⊢ ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n
    (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i') b))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

Goal state before:
pp: case hf
𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ MDiffAt[range ↑I] ↑(extChartAt I x).symm y

pp: case hxs
𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ UniqueMDiffAt[range ↑I] y

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ mfderiv[range ↑I] (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

Tactic:
· exact mdifferentiableWithinAt_extChartAt_symm hy

Goal state after:
case hxs
𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ UniqueMDiffAt[range ↑I] y

𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffAt[range ↑I] y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ mfderiv[range ↑I] (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)
Module: Mathlib.Geometry.Manifold.BumpFunction

Goal state before:
pp: case h₁.refine_1
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
s : Set M
hse : s ⊆ (extChartAt I c).source
hsf : ↑(extChartAt I c) '' s ⊆ ball (↑(extChartAt I c) c) f.rOut
x : M
⊢ ↑(extChartAt I c) x ∈ range ↑I

Tactic:
exact mem_range_self _

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport x₀ ⊆ I
this : ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0
⊢ ∑ i ∈ I \ ρ.finsupport x₀, 0 = 0

Tactic:
Finset.sum_const_zero

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
I : Finset ι
hI : ρ.finsupport x₀ ⊆ I
this : ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0
⊢ 0 = 0
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
p : (X → ℝ) → Prop
h01 :
  ∀ (s t : Set X),
    IsClosed[inst✝²] s →
      IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
hs : IsCompact s
U : ι → Set X
ho : ∀ (i : ι), IsOpen[inst✝²] (U i)
hf : LocallyFinite U
hU : s ⊆ ⋃ i, U i
⊢ ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)

Tactic:
by
  rcases exists_subset_iUnion_closure_subset_t2space hs ho (fun x _ => hf.point_finite x) hU with
    ⟨V, hsV, hVo, hVU, hcp⟩
  have hVU' i : V i ⊆ U i := subset_closure.trans (hVU i)
  rcases exists_subset_iUnion_closure_subset_t2space hs hVo
    (fun x _ => (hf.subset hVU').point_finite x) hsV with ⟨W, hsW, hWo, hWV, hWc⟩
  choose f hfp hf0 hf1 hf01 using fun i =>
    h01 _ _ (isClosed_compl_iff.2 <| hVo i) (hWc i)
      (disjoint_right.2 fun x hx => Classical.not_not.2 (hWV i hx))
  have hsupp i : support (f i) ⊆ V i := support_subset_iff'.2 (hf0 i)
  refine ⟨⟨f, hf.subset fun i => Subset.trans (hsupp i) (hVU' i), fun i x => (hf01 i x).1,
      fun i x => (hf01 i x).2, fun x hx => ?_⟩,
    hfp, fun i => Subset.trans (closure_mono (hsupp i)) (hVU i),
    fun i => IsCompact.of_isClosed_subset (hcp i) isClosed_closure <| closure_mono (hsupp i)⟩
  rcases mem_iUnion.1 (hsW hx) with ⟨i, hi⟩
  exact ⟨i, ((hf1 i).mono subset_closure).eventuallyEq_of_mem ((hWo i).mem_nhds hi)⟩

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

Goal state before:
pp: ι : 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
s : Set M
f : BumpCovering ι M s
hf : ∀ (i : ι), ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑(f i)
i : ι
⊢ LocallyFinite fun i ↦ mulSupport fun x ↦ 1 - (f i) x

Tactic:
by
    simp only [mulSupport_one_sub]
    exact f.locallyFinite

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : 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)
⊢ ∃ v', v < v' ∧ IsCompact (closure (v'.toFun i))

Tactic:
classical
  refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ⟨?_, ?_⟩, ?_⟩
  · intro j
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*, v.isOpen]
  · refine fun x hx => mem_iUnion.2 ?_
    by_cases! h : ∃ j ≠ i, x ∈ v j
    · rcases h with ⟨j, hji, hj⟩
      use j
      rwa [update_of_ne hji]
    · use i
      rw [update_self]
      apply hvi.2.1
      rw [hsi]
      exact ⟨hx, mem_iInter₂_of_mem h⟩
  · rintro j (rfl | hj)
    · rw [update_self]
      exact subset_trans hvi.2.2.1 <| PartialRefinement.subset v j
    · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
      exact v.closure_subset hj
  · intro j hj
    rw [mem_insert_iff] at hj
    by_cases h : j = i
    · rw [← h]
      simp only [update_self]
      exact hvi.2.2.2
    · apply hj.elim
      · intro hji
        exact False.elim (h hji)
      · intro hjmemv
        rw [update_of_ne h]
        exact v.pred_of_mem hjmemv
  · intro j hj
    rw [mem_insert_iff, not_or] at hj
    rw [update_of_ne hj.1, v.apply_eq hj.2]
  · refine ⟨subset_insert _ _, fun j hj => ?_⟩
    exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm
  · exact fun hle => hi (hle.1 <| mem_insert _ _)
  · simp only [update_self]
    exact hvi.2.2.2

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

Goal state before:
pp: case refine_3
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
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a ↦ support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst✝⁴] (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
i : ι
⊢ tsupport
      ↑({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
              eventuallyEq_one' := ⋯ }.toFun
          i) ⊆
    U
      ({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
            eventuallyEq_one' := ⋯ }.c
        i)

Tactic:
simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i

Goal state after:
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
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ ι f, f.IsSubordinate U

Tactic:
by
  -- First we deduce some missing instances
  have : LocallyCompactSpace H := I.locallyCompactSpace
  have : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace H M
  -- Next we choose a covering by supports of smooth bump functions
  have hB := fun x hx => SmoothBumpFunction.nhds_basis_support (I := I) (hU x hx)
  rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with
    ⟨ι, c, f, hf, hsub', hfin⟩
  choose hcs hfU using hf
  -- Then we use the shrinking lemma to get a covering by smaller open
  rcases exists_subset_iUnion_closed_subset hs (fun i => (f i).isOpen_support)
    (fun x _ => hfin.point_finite x) hsub' with ⟨V, hsV, hVc, hVf⟩
  choose r hrR hr using fun i => (f i).exists_r_pos_lt_subset_ball (hVc i) (hVf i)
  refine ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, ?_, fun x hx => ?_⟩, fun i => ?_⟩
  · simpa only [SmoothBumpFunction.support_updateRIn]
  · refine (mem_iUnion.1 <| hsV hx).imp fun i hi => ?_
    exact ((f i).updateRIn _ _).eventuallyEq_one_of_dist_lt
      ((f i).support_subset_source <| hVf _ hi) (hr i hi).2
  · simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i

Goal state after:
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 : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
i : M
⊢ IsOpen[inst✝⁶] ((chartAt H i).target ∩ ↑(chartAt H i).symm ⁻¹' s)

Tactic:
exact OpenPartialHomeomorph.isOpen_inter_preimage_symm _ hs

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ∞ → 0 ≤ ∫ (x : α) in s, (g - f) x ∂μ

Tactic:
integral_sub' hg.integrableOn hf.integrableOn,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ∞ → 0 ≤ ∫ (a : α) in s, g a ∂μ - ∫ (a : α) in s, f a ∂μ