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

Goal state before:
pp: 𝕜 : 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'
i : ↑(atlas H M)
x : M
hx : x ∈ (↑i).source
v y : E
hy : y ∈ ((↑i).extend I).target
⊢ (↑((↑i).extend I) ∘ ↑((↑i).extend I).symm) y = y

Tactic:
exact (i.1.extend I).right_inv 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
⊢ x ∈ range ↑I → (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) x ∈ range ↑I

Tactic:
_

Goal state after:
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
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.inl x) Sum.swap) id t
⊢ t ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x))

Tactic:
rw [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.inl x) Sum.swap) id t
⊢ ↑I.symm ⁻¹' (chartAt H x).target ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x)) ∧
    range ↑I ∈ 𝓝[range ↑I] ↑I (↑(chartAt H (Sum.inl x)) (Sum.inl x))
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:
rw [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.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'
p : M ⊕ M'
⊢ HasMFDerivAt% Sum.swap p (ContinuousLinearMap.id 𝕜 (TangentSpace I p))

Tactic:
refine ⟨by fun_prop, ?_⟩

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'
p : M ⊕ M'
⊢ HasFDerivWithinAt (writtenInExtChartAt I I p Sum.swap) (ContinuousLinearMap.id 𝕜 (TangentSpace I p)) (range ↑I)
    (↑(extChartAt I p) p)
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
s : Set M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
⊢ HasMFDerivAt[s] Sum.inl q (ContinuousLinearMap.id 𝕜 (TangentSpace I q))

Tactic:
refine ⟨by fun_prop, ?_⟩

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
s : Set M
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I q Sum.inl) (ContinuousLinearMap.id 𝕜 (TangentSpace I q))
    (↑(extChartAt I q).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I q) q)
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'
q' : M'
t : Set M'
⊢ HasMFDerivAt[t] Sum.inr q' (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))

Tactic:
refine ⟨by fun_prop, ?_⟩

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'
q' : M'
t : Set M'
⊢ HasFDerivWithinAt (writtenInExtChartAt I I q' Sum.inr) (ContinuousLinearMap.id 𝕜 (TangentSpace I q'))
    (↑(extChartAt I q').symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I q') q')
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
z : M
F' : Type u_21
inst✝² : NormedCommRing F'
inst✝¹ : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
f' : ι → TangentSpace I z →L[𝕜] F'
inst✝ : DecidableEq ι
hf : ∀ i ∈ t, HasMFDerivAt% (f i) z (f' i)
⊢ HasMFDerivAt% (∏ i ∈ t, f i) z (∑ i ∈ t, (∏ j ∈ t.erase i, f j z) • f' i)

Tactic:
by
  simp_all only [← hasMFDerivWithinAt_univ]
  exact HasMFDerivWithinAt.prod hf

Goal state after:
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
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
ι : Type
t : Finset ι
f : ι → M → F'
hf : ∀ i ∈ t, MDiffAt[univ] (f i) z
⊢ MDiffAt[univ] (∏ i ∈ t, f i) z

Tactic:
exact MDifferentiableWithinAt.prod hf

Goal state after:
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
s : Set M
hsc : IsClosed[inst✝²] s
hs : s ⊆ support ↑f
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(extChartAt I c) '' s)

Tactic:
f.image_eq_inter_preimage_of_subset_support hs

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
s : Set M
hsc : IsClosed[inst✝²] s
hs : s ⊆ support ↑f
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s)
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

Goal state before:
pp: case e'_24
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedField F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivAt[s] p z p'
hq : HasMFDerivAt[s] q z q'
hq_ne : q z ≠ 0
e_21✝ : p / q = p * q⁻¹
⊢ (1 / q z) • p' - (p z / q z ^ 2) • q' = p z • -(q z ^ 2)⁻¹ • q' + q⁻¹ z • p'

Tactic:
ext
    simp [div_eq_mul_inv]
    ring

Goal state after:
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 = ⊤
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

Tactic:
have hWo : ∀ y, IsOpen (W y) := fun y ↦ isOpen_biInter_finset fun _ _ ↦ hVo _ _

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
hWo : ∀ (y : Y), IsOpen[inst✝²] (W y)
⊢ ∃ β t,
    (∀ (b : β), IsOpen[instTopologicalSpaceProd] (t b)) ∧ ⋃ b, t b = univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
n : ℕ
⊢ 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n

Tactic:
simp [pow_succ', ← mul_assoc, ENNReal.mul_inv_cancel two_ne_zero ofNat_ne_top]

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

Goal state before:
pp: case refine_1
𝕜 : 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 : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, s x⟩).2) u x₀
⊢ (fun x ↦ (↑e ⟨x, (-s) x⟩).2) =ᶠ[nhdsWithin x₀ u] fun x ↦ -(↑e ⟨x, s x⟩).2

pp: case refine_2
𝕜 : 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 : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, s x⟩).2) u x₀
⊢ (↑e ⟨x₀, (-s) x₀⟩).2 = -(↑e ⟨x₀, s x₀⟩).2

Tactic:
· apply eventually_of_mem (U := e.baseSet)
    · exact mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)
    · intro x hx
      apply (e.linear 𝕜 hx).map_neg

Goal state after:
case refine_2
𝕜 : 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 : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization F TotalSpace.proj := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) n (fun x ↦ (↑e ⟨x, s x⟩).2) u x₀
⊢ (↑e ⟨x₀, (-s) x₀⟩).2 = -(↑e ⟨x₀, s x₀⟩).2
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_2
ι : 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
⊢ s ⊆ ⋃ i_1, update v.toFun i vi i_1

Tactic:
refine fun x hx => mem_iUnion.2 ?_

Goal state after:
case refine_2
ι : 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
x : X
hx : x ∈ s
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : R1Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed[inst✝³] s →
      (∀ x ∈ s, ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
        ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
s t : Set X
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hst : Disjoint s t
x : X
hx : x ∈ s
y : X
hy : y ∈ t
⊢ ∃ u v, IsOpen[inst✝³] u ∧ IsOpen[inst✝³] v ∧ y ∈ u ∧ {x} ⊆ v ∧ Disjoint u v

Tactic:
simp_rw [singleton_subset_iff]
    exact r1_separation <| ht.not_inseparable hy <| hst.notMem_of_mem_left hx

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)ᶜ
j : ι
⊢ (j ∈ fun i_1 ↦ i_1 = i → False) → IsOpen (v.toFun j)

Tactic:
_

Goal state after:
ι : 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)ᶜ
j : ι
a✝ : j ∈ fun i_1 ↦ i_1 = i → False
⊢ IsOpen (v.toFun j)
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)ᶜ
this : IsOpen (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)
⊢ IsClosed (s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ)

Tactic:
exact IsClosed.inter (IsCompact.isClosed hs) (IsOpen.isClosed_compl this)

Goal state after:
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case refine_2
ι : 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)
⊢ s ⊆ ⋃ i_1, update v.toFun i vi i_1

Tactic:
refine fun x hx => mem_iUnion.2 ?_

Goal state after:
case refine_2
ι : 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)
x : X
hx : x ∈ s
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
⊢ ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)

Tactic:
have A : (support fun i => toPOUFun f i x) ⊆ s := by
    rw [hs]
    exact fun i hi => f.support_toPOUFun_subset i hi

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
x : X
s : Finset ι := ⋯.toFinset
hs : ↑s = {i | (f i) x ≠ 0}
A : (support fun i ↦ f.toPOUFun i x) ⊆ ↑s
⊢ ∑ᶠ (i : ι), f.toPOUFun i x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : {i | ((fun i ↦ support ⇑(f i)) i ∩ U).Nonempty}.Finite
y : X
hyU : y ∈ U
j : ι
⊢ WellOrderingRel j i → (f j) y ≠ 0 → j ∈ hf.toFinset

Tactic:
_

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : BumpCovering ι X s
i : ι
x : X
U : Set X
hU : U ∈ 𝓝 x
hf : {i | ((fun i ↦ support ⇑(f i)) i ∩ U).Nonempty}.Finite
y : X
hyU : y ∈ U
j : ι
a✝ : WellOrderingRel j i
⊢ (f j) y ≠ 0 → j ∈ hf.toFinset
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: case 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
this✝ : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w ↦ IsCompact (closure w))),
    IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w ↦ IsCompact (closure w)
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Tactic:
· intro i
    by_contra! hi
    rcases exists_gt_t2space v hs i hi with ⟨v', hlt, _⟩
    exact hv.not_lt hlt

Goal state after: