ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : q.degree = 1<GOAL>f.eigenspace (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0))
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : q.degree = 1<GOAL>q.leadingCoeff ≠ 0
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : q.degree = 1<VAR>h : q.leadingCoeff = 0<GOAL>False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : ⊥ = 1<VAR>h : q.leadingCoeff = 0<GOAL>False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : q.degree = 1<GOAL>LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) = LinearMap.ker ((aeval f) (C q.leadingCoeff * X + C (q.coeff 0)))
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : q.degree = 1<GOAL>LinearMap.ker (q.leadingCoeff • f - (algebraMap K (End K V)) (-q.coeff 0)) = LinearMap.ker (eval₂ (algebraMap K (End K V)) f (q.leadingCoeff • X + C (q.coeff 0)))
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>q : K[X]<VAR>hq : q.degree = 1<GOAL>LinearMap.ker ((aeval f) (C q.leadingCoeff * X + C (q.coeff 0))) = LinearMap.ker ((aeval f) q)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>c : F<VAR>e : E<GOAL>HasFPowerSeriesOnBall (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>c : F<VAR>e y✝ : E<VAR>x✝ : y✝ ∈ EMetric.ball 0 ⊤<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>((constFormalMultilinearSeries 𝕜 E c n) fun x => y✝) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n d : ℕ<GOAL>(trunc (n + 2) X).coeff d = Polynomial.X.coeff d
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n d : ℕ<GOAL>(if d < n + 2 then if d = 1 then 1 else 0 else 0) = Polynomial.X.coeff d
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : Group H<VAR>inst✝⁸ : MulAction G α<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MulAction H β<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : MeasurableSMul G α<VAR>inst✝¹ : SMulInvariantMeasure G α μ<VAR>inst✝ : Countable G<VAR>ν : Measure α<VAR>hs : IsFundamentalDomain G s μ<VAR>ht : IsFundamentalDomain G t μ<VAR>A : Set α<VAR>hA₀ : MeasurableSet A<VAR>hA : ∀ (g : G), (fun x => g • x) ⁻¹' A = A<VAR>this : ∫⁻ (x : α) in s, A.indicator 1 x ∂μ = ∫⁻ (x : α) in t, A.indicator 1 x ∂μ<GOAL>μ (A ∩ s) = μ (A ∩ t)
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ a b : α<VAR>inst✝ : DecidablePred fun x => x ≤ a<VAR>hab : a < b<GOAL>filter (fun x => x ≤ a) (Ico a b) = {a}
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ a b : α<VAR>inst✝ : DecidablePred fun x => x ≤ a<VAR>hab : a < b<GOAL>{a}.val = {a}
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<GOAL>Tendsto μs F (𝓝 μ)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<GOAL>∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<GOAL>Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<GOAL>Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<VAR>f₀_nn : 0 ≤ ⇑f₀<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<VAR>f₀_nn : 0 ≤ ⇑f₀<VAR>f₀_ae_nn : 0 ≤ᶠ[ae ↑μ] ⇑f₀<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<VAR>f₀_nn : 0 ≤ ⇑f₀<VAR>f₀_ae_nn : 0 ≤ᶠ[ae ↑μ] ⇑f₀<VAR>f₀_ae_nns : ∀ (i : γ), 0 ≤ᶠ[ae ↑(μs i)] ⇑f₀<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<VAR>f₀_nn : 0 ≤ ⇑f₀<VAR>f₀_ae_nn : 0 ≤ᶠ[ae ↑μ] ⇑f₀<VAR>f₀_ae_nns : ∀ (i : γ), 0 ≤ᶠ[ae ↑(μs i)] ⇑f₀<VAR>aux : ∫ (a : Ω), f₀ a ∂↑μ = (∫⁻ (a : Ω), ENNReal.ofReal (f₀ a) ∂↑μ).toReal<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<VAR>f₀_nn : 0 ≤ ⇑f₀<VAR>f₀_ae_nn : 0 ≤ᶠ[ae ↑μ] ⇑f₀<VAR>f₀_ae_nns : ∀ (i : γ), 0 ≤ᶠ[ae ↑(μs i)] ⇑f₀<VAR>aux : ∫ (a : Ω), f₀ a ∂↑μ = (∫⁻ (a : Ω), ENNReal.ofReal (f₀ a) ∂↑μ).toReal<VAR>auxs : ∀ (i : γ), ∫ (a : Ω), f₀ a ∂↑(μs i) = (∫⁻ (a : Ω), ENNReal.ofReal (f₀ a) ∂↑(μs i)).toReal<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ))<VAR>f : Ω →ᵇ ℝ≥0<VAR>key : Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal) ↔ Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>lip : LipschitzWith 1 NNReal.toReal<VAR>f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f<VAR>_def_f₀ : f₀ = comp NNReal.toReal lip f<VAR>f₀_eq : ⇑f₀ = NNReal.toReal ∘ ⇑f<VAR>f₀_nn : 0 ≤ ⇑f₀<VAR>f₀_ae_nn : 0 ≤ᶠ[ae ↑μ] ⇑f₀<VAR>f₀_ae_nns : ∀ (i : γ), 0 ≤ᶠ[ae ↑(μs i)] ⇑f₀<VAR>aux : ∫ (a : Ω), ↑(f a) ∂↑μ = (∫⁻ (a : Ω), ↑(f a) ∂↑μ).toReal<VAR>auxs : ∀ (i : γ), ∫ (a : Ω), ↑(f a) ∂↑(μs i) = (∫⁻ (a : Ω), ↑(f a) ∂↑(μs i)).toReal<GOAL>Tendsto (fun n => (∫⁻ (x : Ω), ↑(f x) ∂↑(μs n)).toReal) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>AEMeasurable g ((μ.restrict s).withDensity f)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.withDensity f)<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>AEMeasurable g ((μ.withDensity f).restrict s)
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>U : Set G<VAR>hU : U ∈ B<GOAL>U ∈ 𝓝 1
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>U : Set G<VAR>hU : U ∈ B<GOAL>∃ i ∈ B, id i ⊆ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀
<VAR>μ ν : Measure ℝ<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>inst✝ : IsProbabilityMeasure ν<VAR>h : cdf μ = cdf ν<GOAL>μ = ν
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>round x = 0 ↔ x ∈ Ico (-(1 / 2)) (1 / 2)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>x ∈ Ico (0 - 1 / 2) (1 - 1 / 2) ↔ x ∈ Ico (-(1 / 2)) (1 / 2)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))<GOAL>L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))<VAR>this : HasMFDerivAt I 𝓘(ℝ, E) (⇑L ∘ ⇑f.embeddingPiTangent) x (L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))<GOAL>L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))<VAR>this : HasMFDerivAt I 𝓘(ℝ, E) (⇑L ∘ ⇑f.embeddingPiTangent) x (L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))<GOAL>HasMFDerivAt I 𝓘(ℝ, E) (⇑L ∘ ⇑f.embeddingPiTangent) x (mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))<VAR>this : HasMFDerivAt I 𝓘(ℝ, E) (⇑L ∘ ⇑f.embeddingPiTangent) x (L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))<GOAL>⇑L ∘ ⇑f.embeddingPiTangent =ᶠ[𝓝 x] ↑(extChartAt I (f.c (f.ind x hx)))
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))<VAR>this : HasMFDerivAt I 𝓘(ℝ, E) (⇑L ∘ ⇑f.embeddingPiTangent) x (L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))<VAR>y : M<VAR>hy : ↑(f.toFun (f.ind x hx)) y = 1 y<GOAL>(⇑L ∘ ⇑f.embeddingPiTangent) y = ↑(extChartAt I (f.c (f.ind x hx))) y
<VAR>ι : Type uι<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>inst✝ : T2Space M<VAR>hi : Fintype ι<VAR>s : Set M<VAR>f : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<VAR>L : (ι → E × ℝ) →L[ℝ] E := (ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))<VAR>this : HasMFDerivAt I 𝓘(ℝ, E) (⇑L ∘ ⇑f.embeddingPiTangent) x (L.comp (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))<VAR>y : M<VAR>hy : ↑(f.toFun (f.ind x hx)) y = 1 y<GOAL>↑(f.toFun (f.ind x hx)) y • ↑(extChartAt I (f.c (f.ind x hx))) y = ↑(extChartAt I (f.c (f.ind x hx))) y
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>ι' : Sort u_2<VAR>inst✝ : UniformSpace β<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>ha : (𝓤 α).HasBasis p s<VAR>q : ι' → Prop<VAR>t : ι' → Set (β × β)<VAR>hb : (𝓤 β).HasBasis q t<VAR>f : α → β<VAR>S : Set α<GOAL>(∀ (ib : ι'), q ib → ∃ ia, p ia ∧ ∀ x ∈ s ia ∩ S ×ˢ S, (f x.1, f x.2) ∈ t ib) ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
<VAR>R : CommRingCat<VAR>X✝ : Scheme<VAR>V✝ U✝ : X✝.Opens<VAR>f✝ g : ↑Γ(X✝, U✝)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : X.Opens<VAR>V : Y.Opens<VAR>e : U ≤ f ⁻¹ᵁ V<VAR>s : ↑Γ(Y, V)<GOAL>X.basicOpen ((Hom.appLE f V U e) s) = U ⊓ f ⁻¹ᵁ Y.basicOpen s
<VAR>R : CommRingCat<VAR>X✝ : Scheme<VAR>V✝ U✝ : X✝.Opens<VAR>f✝ g : ↑Γ(X✝, U✝)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : X.Opens<VAR>V : Y.Opens<VAR>e : U ≤ f ⁻¹ᵁ V<VAR>s : ↑Γ(Y, V)<GOAL>X.basicOpen ((X.presheaf.map (homOfLE e).op) ((Hom.app f V) s)) = U ⊓ X.basicOpen ((Hom.app f V) s)
<VAR>M G : Type u<VAR>inst✝³ : Monoid M<VAR>inst✝² : Group G<VAR>N : Type v<VAR>inst✝¹ : Monoid N<VAR>C : Type v<VAR>inst✝ : Category.{w, v} C<VAR>f : C → G<VAR>X✝ : C<GOAL>{ obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.map (𝟙 X✝) = 𝟙 ({ obj := fun x => (), map := fun {x y} x_1 => f y * (f x)⁻¹ }.obj X✝)
<VAR>M G : Type u<VAR>inst✝³ : Monoid M<VAR>inst✝² : Group G<VAR>N : Type v<VAR>inst✝¹ : Monoid N<VAR>C : Type v<VAR>inst✝ : Category.{w, v} C<VAR>f : C → G<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>f Z✝ * (f X✝)⁻¹ = (f Y✝ * (f X✝)⁻¹) ≫ (f Z✝ * (f Y✝)⁻¹)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<GOAL>multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<GOAL>multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<GOAL>multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<GOAL>multiplicity 2 (x ^ n - y ^ n) = multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<GOAL>multiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = multiplicity 2 (x - y) + multiplicity 2 ↑(n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 n.succ).Dom<GOAL>multiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = multiplicity 2 (x - y) + multiplicity 2 ↑(n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<GOAL>multiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = multiplicity 2 (x - y) + multiplicity 2 ↑(n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>multiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = multiplicity 2 (x - y) + multiplicity 2 ↑(n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>multiplicity 2 (x - y) + multiplicity 2 (n + 1) = multiplicity 2 (x - y) + multiplicity 2 ↑(n + 1)
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hx_odd : Odd x<VAR>hxy_even : Even (x - y)<VAR>hy_odd : Odd y<VAR>n : ℕ<VAR>h : (multiplicity 2 (n + 1)).Dom<VAR>hpn : ¬2 ^ ((multiplicity 2 (n + 1)).get h + 1) ∣ n + 1<VAR>k : ℕ<VAR>hk : n + 1 = 2 ^ (multiplicity 2 (n + 1)).get h * k<GOAL>Prime 2