mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
ht : IsClosed[inst✝⁶] t
hd : Disjoint s t
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
by

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
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
hd : s ⊆ interior t
⊢ Disjoint (interior ?m.105)ᶜ s

Tactic:
by

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
n : ℕ∞
inst✝² : T2Space M
inst✝¹ : NormalSpace M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed[inst✝⁶] s
hd : s ⊆ interior t
⊢ ∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
by

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

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsManifold I ∞ M
n : ℕ∞
i : ι
s : Set M
j : ι
⊢ ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑((BumpCovering.single i s) j)

Tactic:
by

Goal state after:
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
hd : Disjoint s t
⊢ ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
rcases exists_contMDiffMap_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩

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 : C^↑?m.169⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hf : EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1
⊢ ∃ 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: ι : 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
⊢ ∃ f, f.IsSubordinate U

Tactic:
by

Goal state after:
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
⊢ ∀ (n : ℕ), ∃ g, support g = v n ∧ ContMDiff I 𝓘(ℝ, ℝ) ∞ g ∧ range g ⊆ Icc 0 1 ∧ ∀ x ∈ s, g x = 1

Tactic:
by

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✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst✝⁵] s
⊢ ∃ f, f.IsSubordinate fun x ↦ (chartAt H ↑x).source

Tactic:
by

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✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
⊢ ∃ f, f.IsSubordinate fun x ↦ (chartAt H x).source

Tactic:
by

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 : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
⊢ univ ⊆ ⋃ x, U x

Tactic:
by

Goal state after:
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
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
⊢ Integrable bound μ

Tactic:
by

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 : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
j : M
⊢ ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x ↦ ⟪c, f x⟫_𝕜) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun c ↦ ⟪c, f x⟫_𝕜

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x ↦ ⟪c, f x⟫_𝕜) =ᵐ[μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
x : α
hx : ∀ (n : ℕ), ⟪s n, f x⟫_𝕜 = 0
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun c ↦ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x ↦ ⟪c, f x⟫_𝕜) =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
⊢ 0 < ‖a‖

Tactic:
by

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 : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
⊢ ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩

Tactic:
by

Goal state after:
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
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
x✝ : x ∈ K
this : g n x ∈ Icc 0 1
⊢ ‖g n x‖ ≤ 1

Tactic:
rw [Real.norm_of_nonneg this.1]

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‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
x✝ : x ∈ K
this : g n x ∈ Icc 0 1
⊢ g n x ≤ 1
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
⊢ ∃ x, dist a ↑x < ‖a‖ / 2

Tactic:
by

Goal state after:
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
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
x✝ : x ∈ K
⊢ ‖g n x‖ ≤ 1

Tactic:
by

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 : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
Hloc :
  ∀ (x₀ : M),
    ∃ U_x₀ ∈ 𝓝 x₀,
      ∃ s_loc, ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x⟩) U_x₀ ∧ ∀ y ∈ U_x₀, s_loc y ∈ t y
⊢ ∃ s, ∀ (x : M), s x ∈ t x

Tactic:
by

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
inst✝⁴ : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst✝³ : EMetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I ∞ M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
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 : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this✝ : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
this : ‖a‖ ≤ ‖↑x‖ + ‖a - ↑x‖
⊢ ‖a - ↑x‖ < ‖a‖ / 2

Tactic:
by

Goal state after:
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
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
n : ℕ
x : M
hxK : x ∉ K
⊢ g n x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
⊢ ‖a‖ / 2 < ‖↑x‖

Tactic:
by

Goal state after: