ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝ : LocallyCompactSpace H<VAR>this : LocallyCompactSpace M<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝¹ : LocallyCompactSpace H<VAR>this✝ : LocallyCompactSpace M<VAR>this : SecondCountableTopology H<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝² : LocallyCompactSpace H<VAR>this✝¹ : LocallyCompactSpace M<VAR>this✝ : SecondCountableTopology H<VAR>this : SecondCountableTopology M<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<GOAL>∀ᵐ (x : M) ∂μ, f x = 0
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set M := fun n => thickening (u n) s<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set M := fun n => thickening (u n) s<VAR>K : Set M<VAR>K_compact : IsCompact K<VAR>vK : ∀ (n : ℕ), v n ⊆ K<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝⁴ : LocallyCompactSpace H<VAR>this✝³ : LocallyCompactSpace M<VAR>this✝² : SecondCountableTopology H<VAR>this✝¹ : SecondCountableTopology M<VAR>this✝ : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set M := fun n => thickening (u n) s<VAR>K : Set M<VAR>K_compact : IsCompact K<VAR>vK : ∀ (n : ℕ), v n ⊆ K<VAR>this : ∀ (n : ℕ), ∃ g, support g = v n ∧ Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1 ∧ ∀ x ∈ s, g x = 1<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝³ : LocallyCompactSpace H<VAR>this✝² : LocallyCompactSpace M<VAR>this✝¹ : SecondCountableTopology H<VAR>this✝ : SecondCountableTopology M<VAR>this : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set M := fun n => thickening (u n) s<VAR>K : Set M<VAR>K_compact : IsCompact K<VAR>vK : ∀ (n : ℕ), v n ⊆ K<VAR>g : ℕ → M → ℝ<VAR>g_supp : ∀ (n : ℕ), support (g n) = v n<VAR>g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)<VAR>g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1<VAR>hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1<VAR>L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>E : Type u_1<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace ℝ E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>F : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : CompleteSpace F<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : BorelSpace M<VAR>inst✝¹ : SigmaCompactSpace M<VAR>inst✝ : T2Space M<VAR>f f' : M → F<VAR>μ : Measure M<VAR>hf : LocallyIntegrable f μ<VAR>h : ∀ (g : M → ℝ), Smooth I 𝓘(ℝ, ℝ) g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0<VAR>this✝⁴ : LocallyCompactSpace H<VAR>this✝³ : LocallyCompactSpace M<VAR>this✝² : SecondCountableTopology H<VAR>this✝¹ : SecondCountableTopology M<VAR>this✝ : MetrizableSpace M<VAR>x✝ : MetricSpace M := metrizableSpaceMetric M<VAR>s : Set M<VAR>hs : IsCompact s<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : IsCompact (cthickening δ s)<VAR>u : ℕ → ℝ<VAR>u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → Set M := fun n => thickening (u n) s<VAR>K : Set M<VAR>K_compact : IsCompact K<VAR>vK : ∀ (n : ℕ), v n ⊆ K<VAR>g : ℕ → M → ℝ<VAR>g_supp : ∀ (n : ℕ), support (g n) = v n<VAR>g_diff : ∀ (n : ℕ), Smooth I 𝓘(ℝ, ℝ) (g n)<VAR>g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1<VAR>hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1<VAR>L : Tendsto (fun n => ∫ (x : M), g n x • f x ∂μ) atTop (𝓝 (∫ (x : M) in s, f x ∂μ))<VAR>this : ∀ (n : ℕ), ∫ (x : M), g n x • f x ∂μ = 0<GOAL>0 = ∫ (x : M) in s, f x ∂μ
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>inst✝¹ : LinearOrderedAddCommGroupWithTop Γ₀<VAR>inst✝ : Ring R<VAR>v : AddValuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>hx : v x < v y<GOAL>v (x - y) = v x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>inst✝¹ : LinearOrderedAddCommGroupWithTop Γ₀<VAR>inst✝ : Ring R<VAR>v : AddValuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>hx : v x < v y<GOAL>v (x + -y) = v x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝² : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>inst✝¹ : LinearOrderedAddCommGroupWithTop Γ₀<VAR>inst✝ : Ring R<VAR>v : AddValuation R Γ₀<VAR>x✝ y✝ z x y : R<VAR>hx : v x < v y<GOAL>v x < v (-y)
<VAR>x y : EReal<GOAL>max (-x) (-y) = -min x y
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.mulAntidiagonal t a)<VAR>h : (↑x).1 = (↑y).1<GOAL>a = (↑x).1 * (↑x).2
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.mulAntidiagonal t a)<VAR>h : (↑x).2 = (↑y).2<GOAL>a = (↑x).1 * (↑x).2
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<GOAL>∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x<GOAL>∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x<GOAL>(fun x => Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) = fun x => ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x<GOAL>↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑(cos (π / 2)) ^ n * (Complex.sin (2 * z * ↑(π / 2)) / (2 * z)) - ↑(cos 0) ^ n * (Complex.sin (2 * z * ↑0) / (2 * z)) - ∫ (x : ℝ) in 0 ..π / 2, -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x<GOAL>IntervalIntegrable (fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) volume 0 (π / 2)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : 2 ≤ n<VAR>hz : z ≠ 0<VAR>der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x<GOAL>IntervalIntegrable (fun x => Complex.cos (2 * z * ↑x)) volume 0 (π / 2)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<VAR>halg : IsAlgebraic F α<GOAL>finSepDegree F ↥F⟮α⟯ ≤ finrank F ↥F⟮α⟯
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<VAR>halg : IsAlgebraic F α<VAR>this : FiniteDimensional F ↥F⟮α⟯<GOAL>finSepDegree F ↥F⟮α⟯ ≤ finrank F ↥F⟮α⟯
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>ϕ : τ → α → α<VAR>s : Set α<GOAL>IsInvariant ϕ s ↔ ∀ (t : τ), ϕ t '' s ⊆ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>GradedMonoid.GMul.mul ((tprod R) a) ((tprod R) b) = (tprod R) (Fin.append a b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>(reindex R (fun x => M) finSumFinEquiv) ((tmulEquiv R M) ((tprod R) a ⊗ₜ[R] (tprod R) b)) = (tprod R) (Fin.append a b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>(reindex R (fun x => M) finSumFinEquiv) ((tprod R) fun i => Sum.elim a b i) = (tprod R) (Fin.append a b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>((tprod R) fun i => Sum.elim a b (finSumFinEquiv.symm i)) = (tprod R) (Fin.append a b)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>(fun i => Sum.elim a b (finSumFinEquiv.symm i)) = Fin.append a b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>(fun i => Sum.elim a b (Fin.addCases Sum.inl Sum.inr i)) = Fin.addCases a b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb : ℕ<VAR>a : Fin na → M<VAR>b : Fin nb → M<GOAL>∀ (x : Fin (na + nb)), Sum.elim a b (Fin.addCases Sum.inl Sum.inr x) = Fin.addCases a b x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y₁ Y₂ : Center C<VAR>f : Y₁ ⟶ Y₂<VAR>U : C<GOAL>(X.fst ◁ f.f) ▷ U ≫ ((X.tensorObj Y₂).snd.β U).hom = ((X.tensorObj Y₁).snd.β U).hom ≫ U ◁ X.fst ◁ f.f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y₁ Y₂ : Center C<VAR>f : Y₁ ⟶ Y₂<VAR>U : C<GOAL>(X.fst ◁ f.f) ▷ U ≫ (α_ X.fst Y₂.fst U).hom ≫ X.fst ◁ (Y₂.snd.β U).hom ≫ (α_ X.fst U Y₂.fst).inv ≫ (X.snd.β U).hom ▷ Y₂.fst ≫ (α_ U X.fst Y₂.fst).hom = ((α_ X.fst Y₁.fst U).hom ≫ X.fst ◁ (Y₁.snd.β U).hom ≫ (α_ X.fst U Y₁.fst).inv ≫ (X.snd.β U).hom ▷ Y₁.fst ≫ (α_ U X.fst Y₁.fst).hom) ≫ U ◁ X.fst ◁ f.f
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : IsFiniteMeasureOnCompacts μ<VAR>inst✝³ : IsFiniteMeasureOnCompacts ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : ν.IsMulRightInvariant<VAR>inst✝ : ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : IsFiniteMeasureOnCompacts μ<VAR>inst✝³ : IsFiniteMeasureOnCompacts ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : ν.IsMulRightInvariant<VAR>inst✝ : ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<VAR>Hf : f = 0<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : IsFiniteMeasureOnCompacts μ<VAR>inst✝³ : IsFiniteMeasureOnCompacts ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : ν.IsMulRightInvariant<VAR>inst✝ : ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<VAR>Hf : LocallyCompactSpace G<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : IsFiniteMeasureOnCompacts μ<VAR>inst✝³ : IsFiniteMeasureOnCompacts ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : ν.IsMulRightInvariant<VAR>inst✝ : ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<VAR>Hf : LocallyCompactSpace G<VAR>D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ ν : Measure G<VAR>inst✝⁴ : IsFiniteMeasureOnCompacts μ<VAR>inst✝³ : IsFiniteMeasureOnCompacts ν<VAR>inst✝² : μ.IsMulLeftInvariant<VAR>inst✝¹ : ν.IsMulRightInvariant<VAR>inst✝ : ν.IsOpenPosMeasure<VAR>f g : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>h'g : HasCompactSupport g<VAR>g_nonneg : 0 ≤ g<VAR>x₀ : G<VAR>g_pos : g x₀ ≠ 0<VAR>Hf : LocallyCompactSpace G<VAR>D : G → ℝ := fun x => ∫ (y : G), g (y⁻¹ * x) ∂ν<VAR>D_cont : Continuous D<GOAL>∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>{a, b}.card = 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>B : E →L⋆[𝕜] E →L[𝕜] 𝕜<VAR>v w : E<GOAL>⟪B♯ v, w⟫_𝕜 = (B v) w