ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : AdicCauchySequence I M<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(transitionMap I M hmn) ((fun n => (I ^ n • ⊤).mkQ (↑f n)) n) = (fun n => (I ^ n • ⊤).mkQ (↑f n)) m
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>f : AdicCauchySequence I M<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>Submodule.Quotient.mk (↑f n) = Submodule.Quotient.mk (↑f m)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<GOAL>ClosedEmbedding ⇑(cfcₙAux ⋯ a ha)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<GOAL>ClosedEmbedding ((⇑↑(cfcHom ⋯) ∘ ⇑↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))) ∘ ⇑ContinuousMapZero.toContinuousMapHom)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<GOAL>ClosedEmbedding ⇑↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>e : C(↑(σₙ 𝕜 a), 𝕜) ≃ₜ C(↑(σ 𝕜 ↑a), 𝕜) := let __src := Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯); { toEquiv := __src.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }<GOAL>ClosedEmbedding ⇑↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : AEMeasurable X ℙ<GOAL>HasPDF X ℙ volume ↔ map X ℙ ≪ volume
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : AEMeasurable X ℙ<GOAL>(map X ℙ).HaveLebesgueDecomposition volume ∧ map X ℙ ≪ volume ↔ map X ℙ ≪ volume
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : CompleteLattice β<VAR>inst✝ : DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>f : α → β<GOAL>⨆ y ∈ s.biUnion t, f y = ⨆ x ∈ s, ⨆ y ∈ t x, f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>s : SignedMeasure α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA₁ : MeasurableSet A<VAR>hB₁ : MeasurableSet B<VAR>hA₂ : 0 ≤ ↑s A<VAR>hB₂ : 0 ≤ ↑s B<VAR>hAB : ↑s (A ∪ B) = 0<GOAL>↑s A = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>v : VectorMeasure α M<VAR>f : ℕ → Set α<VAR>s : SignedMeasure α<VAR>A B : Set α<VAR>h : Disjoint A B<VAR>hA₁ : MeasurableSet A<VAR>hB₁ : MeasurableSet B<VAR>hA₂ : 0 ≤ ↑s A<VAR>hB₂ : 0 ≤ ↑s B<VAR>hAB : ↑s A + ↑s B = 0<GOAL>↑s A = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : InvolutiveStar R<VAR>inst✝¹ : StarRing A<VAR>inst✝ : StarModule R A<VAR>a : A<VAR>x✝ : R<GOAL>x✝ ∈ σ (star a) ↔ x✝ ∈ star (σ a)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a b : M₀<VAR>h : Commute a b<VAR>hab : ¬IsUnit (a * b)<GOAL>inverse (a * b) = inverse b * inverse a
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a b : M₀<VAR>h : Commute a b<VAR>hab : ¬IsUnit (a * b)<VAR>ha : ¬IsUnit a<GOAL>inverse (a * b) = inverse b * inverse a
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a b : M₀<VAR>h : Commute a b<VAR>hab : ¬IsUnit (a * b)<VAR>hb : ¬IsUnit b<GOAL>inverse (a * b) = inverse b * inverse a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : SMulCommClass ℝ 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace E<VAR>c : 𝕜<VAR>f : ↥(Lp E 1 μ)<GOAL>(integralCLM' 𝕜) (c • f) = c • (integralCLM' 𝕜) f
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<VAR>hn : ↑g ∣ num<VAR>hd : g ∣ den<GOAL>maybeNormalize num den g den_nz reduced = normalize num den ⋯
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<VAR>hn : ↑g ∣ num<VAR>hd : g ∣ den<GOAL>normalize (num / ↑g) (den / g) den_nz = normalize num den ⋯
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<VAR>hn : ↑g ∣ num<VAR>hd : g ∣ den<VAR>this : g ≠ 0<GOAL>normalize (num / ↑g) (den / g) den_nz = normalize num den ⋯
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<VAR>hn : ↑g ∣ num<VAR>hd : g ∣ den<VAR>this : g ≠ 0<GOAL>normalize num (den / g * g) ⋯ = normalize num den ⋯
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den / g ≠ 0<VAR>reduced : (num.div ↑g).natAbs.Coprime (den / g)<VAR>hn : ↑g ∣ num<VAR>hd : g ∣ den<VAR>this : g ≠ 0<GOAL>den / g * g = den
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<GOAL>r - ↑‖y‖₊ ≤ (p.changeOrigin y).radius
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<GOAL>r - ↑‖y‖₊ ≤ p.radius - ↑‖y‖₊
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<GOAL>HasSum (fun n => (p.changeOrigin y n) fun x => z) (f (x + y + z))
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<VAR>this : f (x + y + z) = (p.changeOrigin y).sum z<GOAL>HasSum (fun n => (p.changeOrigin y n) fun x => z) (f (x + y + z))
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<VAR>this : f (x + y + z) = (p.changeOrigin y).sum z<GOAL>HasSum (fun n => (p.changeOrigin y n) fun x => z) ((p.changeOrigin y).sum z)
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<VAR>this : f (x + y + z) = (p.changeOrigin y).sum z<GOAL>z ∈ EMetric.ball 0 (p.changeOrigin y).radius
<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>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>h : ↑‖y‖₊ < r<VAR>z : E<VAR>hz : z ∈ EMetric.ball 0 (r - ↑‖y‖₊)<VAR>this : f (x + y + z) = (p.changeOrigin y).sum z<GOAL>r - ↑‖y‖₊ ≤ p.radius - ↑‖y‖₊
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<VAR>hVU' : ∀ (i : ι), V i ⊆ U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<VAR>hVU' : ∀ (i : ι), V i ⊆ U i<VAR>W : ι → Set X<VAR>hsW : s ⊆ iUnion W<VAR>hWo : ∀ (i : ι), IsOpen (W i)<VAR>hWV : ∀ (i : ι), closure (W i) ⊆ V i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f✝ : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<VAR>hVU' : ∀ (i : ι), V i ⊆ U i<VAR>W : ι → Set X<VAR>hsW : s ⊆ iUnion W<VAR>hWo : ∀ (i : ι), IsOpen (W i)<VAR>hWV : ∀ (i : ι), closure (W i) ⊆ V i<VAR>f : ι → C(X, ℝ)<VAR>hfp : ∀ (i : ι), p ⇑(f i)<VAR>hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ<VAR>hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))<VAR>hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f✝ : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<VAR>hVU' : ∀ (i : ι), V i ⊆ U i<VAR>W : ι → Set X<VAR>hsW : s ⊆ iUnion W<VAR>hWo : ∀ (i : ι), IsOpen (W i)<VAR>hWV : ∀ (i : ι), closure (W i) ⊆ V i<VAR>f : ι → C(X, ℝ)<VAR>hfp : ∀ (i : ι), p ⇑(f i)<VAR>hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ<VAR>hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))<VAR>hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1<VAR>hsupp : ∀ (i : ι), support ⇑(f i) ⊆ V i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f✝ : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<VAR>hVU' : ∀ (i : ι), V i ⊆ U i<VAR>W : ι → Set X<VAR>hsW : s ⊆ iUnion W<VAR>hWo : ∀ (i : ι), IsOpen (W i)<VAR>hWV : ∀ (i : ι), closure (W i) ⊆ V i<VAR>f : ι → C(X, ℝ)<VAR>hfp : ∀ (i : ι), p ⇑(f i)<VAR>hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ<VAR>hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))<VAR>hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1<VAR>hsupp : ∀ (i : ι), support ⇑(f i) ⊆ V i<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ i, ⇑(f i) =ᶠ[𝓝 x] 1
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set X<VAR>f✝ : BumpCovering ι X s<VAR>inst✝ : NormalSpace X<VAR>p : (X → ℝ) → Prop<VAR>h01 : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → ∃ f, p ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1<VAR>hs : IsClosed s<VAR>U : ι → Set X<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hf : LocallyFinite U<VAR>hU : s ⊆ ⋃ i, U i<VAR>V : ι → Set X<VAR>hsV : s ⊆ iUnion V<VAR>hVo : ∀ (i : ι), IsOpen (V i)<VAR>hVU : ∀ (i : ι), closure (V i) ⊆ U i<VAR>hVU' : ∀ (i : ι), V i ⊆ U i<VAR>W : ι → Set X<VAR>hsW : s ⊆ iUnion W<VAR>hWo : ∀ (i : ι), IsOpen (W i)<VAR>hWV : ∀ (i : ι), closure (W i) ⊆ V i<VAR>f : ι → C(X, ℝ)<VAR>hfp : ∀ (i : ι), p ⇑(f i)<VAR>hf0 : ∀ (i : ι), EqOn (⇑(f i)) 0 (V i)ᶜ<VAR>hf1 : ∀ (i : ι), EqOn (⇑(f i)) 1 (closure (W i))<VAR>hf01 : ∀ (i : ι) (x : X), (f i) x ∈ Icc 0 1<VAR>hsupp : ∀ (i : ι), support ⇑(f i) ⊆ V i<VAR>x : X<VAR>hx : x ∈ s<VAR>i : ι<VAR>hi : x ∈ W i<GOAL>∃ i, ⇑(f i) =ᶠ[𝓝 x] 1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t✝ u : Set α✝<VAR>α : Type u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : ℝ≥0<VAR>ht : 1 < t<VAR>A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)<VAR>B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {⊤}) + μ (s ∩ f ⁻¹' Ioo 0 ⊤)<VAR>C : μ (s ∩ f ⁻¹' Ioo 0 ⊤) = ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))<GOAL>μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {⊤}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<GOAL>(Function.support fun m => (weightedHomogeneousComponent w m) φ).Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<GOAL>(Function.support fun m => (weightedHomogeneousComponent w m) φ) ⊆ (fun d => (weight w) d) '' ↑φ.support
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>m : M<VAR>hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ<GOAL>m ∈ (fun d => (weight w) d) '' ↑φ.support
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>m : M<VAR>hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ<VAR>hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>m : M<VAR>hm : m ∈ Function.support fun m => (weightedHomogeneousComponent w m) φ<VAR>hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support<GOAL>(fun m => (weightedHomogeneousComponent w m) φ) m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>m : M<VAR>hm' : m ∉ (fun d => (weight w) d) '' ↑φ.support<VAR>hm : ¬(weightedHomogeneousComponent w m) φ = 0<GOAL>(fun m => (weightedHomogeneousComponent w m) φ) m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>m : M<VAR>hm : ¬(weightedHomogeneousComponent w m) φ = 0<VAR>hm' : ∀ x ∈ ↑φ.support, ¬(weight w) x = m<GOAL>(fun m => (weightedHomogeneousComponent w m) φ) m = 0
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : OpenEmbedding ⇑f<VAR>H₂ : OpenEmbedding ⇑g<GOAL>OpenEmbedding ⇑(limit.π (cospan f g) WalkingCospan.one)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : OpenEmbedding ⇑f<VAR>H₂ : OpenEmbedding ⇑g<VAR>e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S<GOAL>⇑(limit.π (cospan f g) WalkingCospan.one) = ⇑g ∘ ⇑(pullback.snd f g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : OpenEmbedding ⇑f<VAR>H₂ : OpenEmbedding ⇑g<VAR>e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S<GOAL>⇑(limit.π (cospan f g) WalkingCospan.one) = ⇑(pullback.snd f g ≫ g)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X✝ Y✝ Z : TopCat<VAR>X Y S : TopCat<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H₁ : OpenEmbedding ⇑f<VAR>H₂ : OpenEmbedding ⇑g<VAR>e_2✝ : ↑((cospan f g).obj WalkingCospan.one) = ↑S<GOAL>⇑(limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr) = ⇑(pullback.snd f g ≫ g)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J✝ : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>J : Box ι<VAR>hJ : ↑J ≤ ↑I<VAR>π : Prepartition J<VAR>hπ : π.IsPartition<GOAL>∑ Ji ∈ π.boxes, (fun J => integral J l f vol) Ji = (fun J => integral J l f vol) J
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J✝ : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>J : Box ι<VAR>hJ : ↑J ≤ ↑I<VAR>π : Prepartition J<VAR>hπ : π.iUnion = ↑J<GOAL>∑ Ji ∈ π.boxes, (fun J => integral J l f vol) Ji = (fun J => integral J l f vol) J
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J✝ : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>J : Box ι<VAR>hJ : ↑J ≤ ↑I<VAR>π : Prepartition J<VAR>hπ : π.iUnion = ⊤.iUnion<GOAL>∑ Ji ∈ π.boxes, (fun J => integral J l f vol) Ji = (fun J => integral J l f vol) J
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set (α × α)<GOAL>s ∈ 𝓤 α ↔ s ∈ comap (fun p => dist p.1 p.2) (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set (α × α)<GOAL>(∃ ε > 0, ∀ {a b : α}, dist a b < ε → (a, b) ∈ s) ↔ ∃ i, 0 < i ∧ (fun p => dist p.1 p.2) ⁻¹' ball 0 i ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>n : ℕ<VAR>h : n.Coprime (orderOf σ)<GOAL>(σ ^ n).support = σ.support
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>n : ℕ<VAR>h : n.Coprime (orderOf σ)<VAR>m : ℕ<VAR>hm : (σ ^ n) ^ m = σ<GOAL>(σ ^ n).support = σ.support
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<VAR>a : R<VAR>ha : a ∈ AddSubmonoid.closure ↑S<GOAL>∀ {b : R}, b ∈ S → a * b ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<GOAL>∀ x ∈ ↑S, ∀ b ∈ S, x * b ∈ AddSubmonoid.closure ↑S