mathlib-initiative/mathlib-tactics huggingface dataset:
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
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := eball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), n + k + 1 ≤ m → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : eball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ 2 * 2⁻¹ ^ m + 2⁻¹ ^ m = 2 * 2⁻¹ ^ m + 2⁻¹ ^ m

Tactic:
]

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
⊢ s ⊆ interior ?m.105

Tactic:
]

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
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
⊢ s ⊆ interior ?m.105
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 : C^↑n⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
h0 : ∀ᶠ (x : M) in 𝓝ˢ (interior t)ᶜ, f x = 0
h1 : ∀ᶠ (x : M) in 𝓝ˢ s, f x = 1
hf : ∀ (x : M), f x ∈ Icc 0 1
x : M
hx : x ∉ t
⊢ f x = 0

Tactic:
exact h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx'

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
⊢ Tendsto (fun n ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), s.indicator f x ∂μ))

Tactic:
]

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
⊢ Tendsto (fun n ↦ ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M), s.indicator f x ∂μ))
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

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

Tactic:
]

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) μ
⊢ IntegrableOn (fun x ↦ ‖f x‖) K μ
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
⊢ ⟪f x, f x⟫_𝕜 = 0

Tactic:
]

Goal state after:
α : 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
⊢ ⟪f x, f x⟫_𝕜 = 0
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⟩
i x : M
hx : x ∈ {x | (ρ i) x • s_loc i x ≠ 0}
⊢ x ∈ {x | (ρ i) x ≠ 0}

Tactic:
]

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
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⟩
i x : M
hx : x ∈ {x | (ρ i) x • s_loc i x ≠ 0}
⊢ x ∈ {x | (ρ i) x ≠ 0}
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
⊢ ‖g n x‖ * ‖f x‖ ≤ bound x

Tactic:
]

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
⊢ ‖g n x‖ * ‖f x‖ ≤ bound x
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⟩
i x : M
hx : (ρ i) x • s_loc i x ≠ 0
⊢ (ρ i) x ≠ 0

Tactic:
]

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
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⟩
i x : M
hx : (ρ i) x • s_loc i x ≠ 0
⊢ (ρ i) x ≠ 0
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:
]

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.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
⊢ x ∉ v n

Tactic:
]

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
hxK : x ∉ K
⊢ x ∉ v n