ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>this✝³ : Algebra R S := f.toAlgebra<VAR>this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝¹ : Algebra R' S' := f'.toAlgebra<VAR>this✝ : IsScalarTower R R' S'<VAR>n : ℕ<VAR>g : MvPolynomial (Fin n) R →ₐ[R] S<VAR>hgsurj : Function.Surjective ⇑g<VAR>hgker : (ker g.toRingHom).FG<VAR>MX : Submonoid (MvPolynomial (Fin n) R) := Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M<VAR>this : IsLocalization MX (MvPolynomial (Fin n) R')<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>this✝⁴ : Algebra R S := f.toAlgebra<VAR>this✝³ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝² : Algebra R' S' := f'.toAlgebra<VAR>this✝¹ : IsScalarTower R R' S'<VAR>n : ℕ<VAR>g : MvPolynomial (Fin n) R →ₐ[R] S<VAR>hgsurj : Function.Surjective ⇑g<VAR>hgker : (ker g.toRingHom).FG<VAR>MX : Submonoid (MvPolynomial (Fin n) R) := Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M<VAR>this✝ : IsLocalization MX (MvPolynomial (Fin n) R')<VAR>this : IsScalarTower R S S'<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>this✝⁵ : Algebra R S := f.toAlgebra<VAR>this✝⁴ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝³ : Algebra R' S' := f'.toAlgebra<VAR>this✝² : IsScalarTower R R' S'<VAR>n : ℕ<VAR>g : MvPolynomial (Fin n) R →ₐ[R] S<VAR>hgsurj : Function.Surjective ⇑g<VAR>hgker : (ker g.toRingHom).FG<VAR>MX : Submonoid (MvPolynomial (Fin n) R) := Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M<VAR>this✝¹ : IsLocalization MX (MvPolynomial (Fin n) R')<VAR>this✝ : IsScalarTower R S S'<VAR>this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'<VAR>g' : MvPolynomial (Fin n) R' →ₐ[R'] S' := IsLocalization.mapₐ M R' (MvPolynomial (Fin n) R') S' g<VAR>k : ↥(ker g) →ₛₗ[id (MvPolynomial (Fin n) R)] ↥(ker g') := AlgHom.toKerIsLocalization M R' (MvPolynomial (Fin n) R') S' g<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>this✝⁶ : Algebra R S := f.toAlgebra<VAR>this✝⁵ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝⁴ : Algebra R' S' := f'.toAlgebra<VAR>this✝³ : IsScalarTower R R' S'<VAR>n : ℕ<VAR>g : MvPolynomial (Fin n) R →ₐ[R] S<VAR>hgsurj : Function.Surjective ⇑g<VAR>hgker : (ker g.toRingHom).FG<VAR>MX : Submonoid (MvPolynomial (Fin n) R) := Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M<VAR>this✝² : IsLocalization MX (MvPolynomial (Fin n) R')<VAR>this✝¹ : IsScalarTower R S S'<VAR>this✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'<VAR>g' : MvPolynomial (Fin n) R' →ₐ[R'] S' := IsLocalization.mapₐ M R' (MvPolynomial (Fin n) R') S' g<VAR>k : ↥(ker g) →ₛₗ[id (MvPolynomial (Fin n) R)] ↥(ker g') := AlgHom.toKerIsLocalization M R' (MvPolynomial (Fin n) R') S' g<VAR>this : IsLocalizedModule MX k<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>this✝⁷ : Algebra R S := f.toAlgebra<VAR>this✝⁶ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝⁵ : Algebra R' S' := f'.toAlgebra<VAR>this✝⁴ : IsScalarTower R R' S'<VAR>n : ℕ<VAR>g : MvPolynomial (Fin n) R →ₐ[R] S<VAR>hgsurj : Function.Surjective ⇑g<VAR>hgker : (ker g.toRingHom).FG<VAR>MX : Submonoid (MvPolynomial (Fin n) R) := Algebra.algebraMapSubmonoid (MvPolynomial (Fin n) R) M<VAR>this✝³ : IsLocalization MX (MvPolynomial (Fin n) R')<VAR>this✝² : IsScalarTower R S S'<VAR>this✝¹ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'<VAR>g' : MvPolynomial (Fin n) R' →ₐ[R'] S' := IsLocalization.mapₐ M R' (MvPolynomial (Fin n) R') S' g<VAR>k : ↥(ker g) →ₛₗ[id (MvPolynomial (Fin n) R)] ↥(ker g') := AlgHom.toKerIsLocalization M R' (MvPolynomial (Fin n) R') S' g<VAR>this✝ : IsLocalizedModule MX k<VAR>this : Module.Finite (MvPolynomial (Fin n) R) ↥(ker g)<GOAL>(IsLocalization.map S' f ⋯).FinitePresentation
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>S : Type u_3<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Algebra S R<VAR>inst✝⁷ : Module S M<VAR>inst✝⁶ : IsScalarTower S R M<VAR>R₁ : Type u_4<VAR>M₁ : Type u_5<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_6<VAR>K : Type u_7<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>r : S<VAR>x y : M<GOAL>(B (r • x)) y = r • (B x) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddGroup n<VAR>v w : n → α<VAR>i j : n<GOAL>(circulant v * circulant w) i j = circulant (circulant v *ᵥ w) i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddGroup n<VAR>v w : n → α<VAR>i j : n<GOAL>∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddGroup n<VAR>v w : n → α<VAR>i j : n<GOAL>∀ (x : n), v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddGroup n<VAR>v w : n → α<VAR>i j x : n<GOAL>v (i - x) * w (x - j) = v (i - j - (Equiv.subRight j) x) * w ((Equiv.subRight j) x)
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : CountableInterFilter l<VAR>ι : Type u_4<VAR>S : Set ι<VAR>hS : S.Countable<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<VAR>this : Encodable ↑S<GOAL>⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (limitProcess f ℱ μ ω))
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>injectiveSeminorm ≤ projectiveSeminorm
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>sSup {p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)} ≤ projectiveSeminorm
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>{p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}.Nonempty
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>∀ b ∈ {p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}, b ≤ projectiveSeminorm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : ∃ i, IntegrableOn f (s i) μ<VAR>S : Set X := ⋂ i, s i<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : ∃ i, IntegrableOn f (s i) μ<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : ∃ i, IntegrableOn f (s i) μ<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : ∃ i, IntegrableOn f (s i) μ<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<GOAL>Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>hfi : ∃ i, IntegrableOn f (s i) μ<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<VAR>νS : ν S ≠ ⊤<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<VAR>νS : ν S ≠ ⊤<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<GOAL>∀ᶠ (x : ι) in atTop, ∫ (x : X) in s x, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<VAR>νS : ν S ≠ ⊤<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>h'i : i ∈ Ici i₀<GOAL>∫ (x : X) in s i, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<VAR>νS : ν S ≠ ⊤<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>h'i : i ∈ Ici i₀<GOAL>↑‖∫ (x : X) in s i \ S, f x ∂μ‖₊ ≤ ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<VAR>νS : ν S ≠ ⊤<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>h'i : i ∈ Ici i₀<GOAL>∫⁻ (a : X) in s i \ S, ↑‖f a‖₊ ∂μ ≤ ↑ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f g : X → E<VAR>s✝ t : Set X<VAR>μ ν✝ : Measure X<VAR>l l' : Filter X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>inst✝ : SemilatticeSup ι<VAR>s : ι → Set X<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>h_anti : Antitone s<VAR>S : Set X := ⋂ i, s i<VAR>hSm : MeasurableSet S<VAR>hsub : ∀ (i : ι), S ⊆ s i<VAR>ν : Measure X := μ.withDensity fun x => ↑‖f x‖₊<VAR>hν : ν = μ.withDensity fun x => ↑‖f x‖₊<VAR>ε : ℝ≥0<VAR>ε0 : 0 < ↑ε<VAR>i₀ : ι<VAR>hi₀ : IntegrableOn f (s i₀) μ<VAR>νi₀ : ν (s i₀) ≠ ⊤<VAR>νS : ν S ≠ ⊤<VAR>this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>i : ι<VAR>hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)<VAR>h'i : i ∈ Ici i₀<GOAL>ν (s i) - ν S ≤ ↑ε
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsLowerModularLattice α<VAR>a b : α<GOAL>b ⋖ a ⊔ b → a ⊓ b ⋖ a
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsLowerModularLattice α<VAR>a b : α<GOAL>b ⋖ b ⊔ a → b ⊓ a ⋖ a
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>mk0 ⟨integralRep ↑I, ⋯⟩ = mk I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = (FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0<GOAL>∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = (FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0<GOAL>I * (toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero) = (FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0<GOAL>↑(I * (toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero)) = ↑((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : DecidableEq L<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : IsFractionRing R K<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra R L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0<GOAL>spanSingleton R⁰ ((algebraMap R (FractionRing R)) ↑(↑I).den) * ↑I = ↑((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)
<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>inst✝ : ParacompactSpace 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>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U