ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>s : Set E<VAR>hs : Orthonormal 𝕜 Subtype.val<VAR>this : ∃ m ∈ {b | Orthonormal 𝕜 Subtype.val}, s ⊆ m ∧ ∀ a ∈ {b | Orthonormal 𝕜 Subtype.val}, m ⊆ a → a = m<GOAL>∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>s : Set E<VAR>hs : Orthonormal 𝕜 Subtype.val<GOAL>∀ c ⊆ {b | Orthonormal 𝕜 Subtype.val}, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ {b | Orthonormal 𝕜 Subtype.val}, ∀ s ∈ c, s ⊆ ub
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>(∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>x : V<VAR>hx : ∀ (n : V), (B.flip x) n = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>x : V<VAR>hx : ∀ (n : V), (B.flip x) n = 0<GOAL>(Module.evalEquiv K V) x = (Module.evalEquiv K V) 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>x : V<VAR>hx : ∀ (n : V), (B.flip x) n = 0<VAR>f : Module.Dual K V<GOAL>((Module.evalEquiv K V) x) f = ((Module.evalEquiv K V) 0) f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>x : V<VAR>hx : ∀ (n : V), (B.flip x) n = 0<VAR>y : V<GOAL>((Module.evalEquiv K V) x) ((B.toDual hB) y) = ((Module.evalEquiv K V) 0) ((B.toDual hB) y)
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy₁ : x₁ ≡ y₁ [SMOD U]<VAR>hxy₂ : x₂ ≡ y₂ [SMOD U]<GOAL>x₁ - x₂ ≡ y₁ - y₂ [SMOD U]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁<VAR>hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂<GOAL>Submodule.Quotient.mk (x₁ - x₂) = Submodule.Quotient.mk (y₁ - y₂)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(λ_ (X₁ ⊗ X₂)).hom = (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv ≫ 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂ ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<VAR>this : (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv = 𝟙_ C ◁ (λ_ X₁).inv ▷ X₂<GOAL>(λ_ (X₁ ⊗ X₂)).hom = (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ ((α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv ≫ 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂ ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<VAR>this : (λ_ (𝟙_ C)).inv ▷ (X₁ ⊗ X₂) ≫ (α_ (𝟙_ C) (𝟙_ C) (X₁ ⊗ X₂)).hom ≫ 𝟙_ C ◁ (α_ (𝟙_ C) X₁ X₂).inv = 𝟙_ C ◁ (λ_ X₁).inv ▷ X₂<GOAL>(λ_ (X₁ ⊗ X₂)).hom = (((𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ ≫ 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂) ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(λ_ (X₁ ⊗ X₂)).hom = (((𝟙_ C ◁ (λ_ X₁).inv ▷ X₂ ≫ 𝟙_ C ◁ (β_ (𝟙_ C) X₁).hom ▷ X₂) ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ : C<GOAL>(λ_ (X₁ ⊗ X₂)).hom = ((𝟙_ C ◁ (ρ_ X₁).inv ▷ X₂ ≫ 𝟙_ C ◁ (α_ X₁ (𝟙_ C) X₂).hom) ≫ (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).inv) ≫ ((λ_ X₁).hom ⊗ (λ_ X₂).hom)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>H : IsJacobson R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>H : IsJacobson R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>∀ {I : Ideal S}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>H : IsJacobson R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>p : Ideal S<VAR>hp : p.IsPrime<GOAL>∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ p = sInf M
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>H : IsJacobson R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>p : Ideal S<VAR>hp : p.IsPrime<GOAL>(∀ J ∈ map f '' {J | comap f p ≤ J ∧ J.IsMaximal}, J.IsMaximal ∨ J = ⊤) ∧ p = sInf (map f '' {J | comap f p ≤ J ∧ J.IsMaximal})
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>H : IsJacobson R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>p : Ideal S<VAR>hp : p.IsPrime<GOAL>p = sInf (map f '' {J | comap f p ≤ J ∧ J.IsMaximal})
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>H : IsJacobson R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>p : Ideal S<VAR>hp : p.IsPrime<VAR>this : p = map f (comap f p).jacobson<GOAL>p = sInf (map f '' {J | comap f p ≤ J ∧ J.IsMaximal})
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<GOAL>Tendsto (fun i => μs i) atTop (𝓝 μ)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<GOAL>∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) atTop (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<GOAL>∀ (f : Ω →ᵇ ℝ), 0 ≤ f → ∫ (x : Ω), f x ∂↑μ ≤ liminf (fun i => ∫ (x : Ω), f x ∂↑(μs i)) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<GOAL>∫ (x : Ω), f x ∂↑μ ≤ liminf (fun i => ∫ (x : Ω), f x ∂↑(μs i)) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<GOAL>∀ (G : Set Ω), IsOpen G → ↑μ G ≤ liminf (fun i => ↑(μs i) G) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>aux : ↑(liminf (fun i => (μs i) G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i => (μs i) G) atTop<GOAL>↑μ G ≤ liminf (fun i => ↑(μs i) G) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>aux : ↑(liminf (fun i => (μs i) G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i => (μs i) G) atTop<VAR>obs : ↑(μ G) ≤ ↑(liminf (fun i => (μs i) G) atTop)<GOAL>↑μ G ≤ liminf (fun i => ↑(μs i) G) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>aux : ↑(liminf (fun i => (μs i) G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i => (μs i) G) atTop<VAR>obs : ↑μ G ≤ liminf (ENNReal.ofNNReal ∘ fun i => (μs i) G) atTop<GOAL>↑μ G ≤ liminf (fun i => ↑(μs i) G) atTop
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>μs : ℕ → ProbabilityMeasure Ω<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>G : Set Ω<VAR>G_open : IsOpen G<VAR>h_opens : μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>aux : ↑(liminf (fun i => (μs i) G) atTop) = liminf (ENNReal.ofNNReal ∘ fun i => (μs i) G) atTop<VAR>obs : ↑μ G ≤ liminf (ENNReal.ofNNReal ∘ fun i => (μs i) G) atTop<VAR>x✝ : ℕ<GOAL>↑(μs x✝) G = (ENNReal.ofNNReal ∘ fun i => (μs i) G) x✝
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Icc a b))] f<GOAL>0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Icc a b))] f<VAR>H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), 0 x ≤ f x := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf<GOAL>0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<GOAL>Fintype (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<VAR>h : Ideal.span {hζ.toInteger - 1} = ⊥<GOAL>False
<VAR>p : ℕ+<VAR>k✝ : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : NumberField K<VAR>k : ℕ+<VAR>hk : 1 < k<VAR>hζ : IsPrimitiveRoot ζ ↑k<VAR>h : hζ.toInteger = 1<GOAL>False
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : LinearOrder α<GOAL>∃ x y, x < y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : LinearOrder α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>∃ x y, x < y
<VAR>x : ℂ<VAR>hx : x = 0<GOAL>x ^ 1 = x
<VAR>x : ℂ<VAR>hx : ¬x = 0<GOAL>x ^ 1 = x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>c : β<GOAL>(∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>c : β<GOAL>μ {a | ¬c ≤ f a} = 0 ↔ ∀ b < c, μ {x | f x ≤ b} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>c : β<VAR>hc : ∀ b < c, μ {x | f x ≤ b} = 0<VAR>H : IsLUB (Set.Iio c) c<VAR>h : ∃ b, b < c<GOAL>μ {a | f a < c} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>c : β<VAR>hc : ∀ b < c, μ {x | f x ≤ b} = 0<VAR>H : IsLUB (Set.Iio c) c<VAR>h : ∃ b, b < c<VAR>u : ℕ → β<VAR>left✝ : StrictMono u<VAR>u_lt : ∀ (n : ℕ), u n < c<VAR>u_lim : Tendsto u atTop (𝓝 c)<GOAL>μ {a | f a < c} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>c : β<VAR>hc : ∀ b < c, μ {x | f x ≤ b} = 0<VAR>H : IsLUB (Set.Iio c) c<VAR>h : ∃ b, b < c<VAR>u : ℕ → β<VAR>left✝ : StrictMono u<VAR>u_lt : ∀ (n : ℕ), u n < c<VAR>u_lim : Tendsto u atTop (𝓝 c)<VAR>h_Union : {x | f x < c} = ⋃ n, {x | f x ≤ u n}<GOAL>μ {a | f a < c} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>β : Type u_3<VAR>inst✝³ : LinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : FirstCountableTopology β<VAR>f : α → β<VAR>c : β<VAR>hc : ∀ b < c, μ {x | f x ≤ b} = 0<VAR>H : IsLUB (Set.Iio c) c<VAR>h : ∃ b, b < c<VAR>u : ℕ → β<VAR>left✝ : StrictMono u<VAR>u_lt : ∀ (n : ℕ), u n < c<VAR>u_lim : Tendsto u atTop (𝓝 c)<VAR>h_Union : {x | f x < c} = ⋃ n, {x | f x ≤ u n}<GOAL>∀ (i : ℕ), μ {x | f x ≤ u i} = 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 = p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<VAR>hpq : p.IsConjExponent q<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<VAR>hpq : p.IsConjExponent q<VAR>hp₁ : 1 / p * p = 1<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>p : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<VAR>hpq : p.IsConjExponent q<VAR>hp₁ : 1 / p * p = 1<VAR>hq : 1 / q * p = p - 1<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>Fq F : Type<VAR>inst✝² : Field Fq<VAR>inst✝¹ : Field F<VAR>inst✝ : DecidableEq (RatFunc Fq)<GOAL>↑(Multiplicative.ofAdd (RatFunc.intDegree 1)) = 1
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v x✝ y✝ : V<VAR>he : s(x✝, y✝) ∈ G'.edgeSet<VAR>hv : v ∈ s(x✝, y✝)<GOAL>v ∈ G'.verts
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v y✝ : V<VAR>he : s(v, y✝) ∈ G'.edgeSet<VAR>hv : v ∈ s(v, y✝)<GOAL>v ∈ G'.verts
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>G' : G.Subgraph<VAR>v x✝ : V<VAR>he : s(x✝, v) ∈ G'.edgeSet<VAR>hv : v ∈ s(x✝, v)<GOAL>v ∈ G'.verts
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>f : α ↪o β<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderBot β<VAR>a₁ a₂ : α<VAR>h : Disjoint (f a₁) (f a₂)<VAR>x : α<VAR>h₁ : x ≤ a₁<VAR>h₂ : x ≤ a₂<GOAL>x ≤ ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>f : α ↪o β<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderBot β<VAR>a₁ a₂ : α<VAR>h : Disjoint (f a₁) (f a₂)<VAR>x : α<VAR>h₁ : f x ≤ f a₁<VAR>h₂ : f x ≤ f a₂<GOAL>f x ≤ f ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ η : Kernel α β<VAR>μ : Measure β<VAR>inst✝ : IsFiniteMeasure μ<GOAL>(dirac () ⊗ₘ Kernel.const Unit μ).snd = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ η : Kernel α β<VAR>μ : Measure β<VAR>inst✝ : IsFiniteMeasure μ<GOAL>map (Prod.snd ∘ Prod.mk ()) μ = μ
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>Measure.map (fun x => a * x) volume = ofReal |a⁻¹| • volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedAddCommGroup F<VAR>a : ℝ<GOAL>¬IntegrableOn (fun x => x⁻¹) (Ici a) volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedAddCommGroup F<VAR>a : ℝ<VAR>A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x<GOAL>¬IntegrableOn (fun x => x⁻¹) (Ici a) volume
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedAddCommGroup F<VAR>a : ℝ<VAR>A : ∀ᶠ (x : ℝ) in atTop, HasDerivAt (fun x => Real.log x) x⁻¹ x<VAR>B : Tendsto (fun x => ‖Real.log x‖) atTop atTop<GOAL>¬IntegrableOn (fun x => x⁻¹) (Ici a) volume
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : HasBinaryProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ prod.fst ≫ prod.fst = prod.fst
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>hurwitzZeta (↑x) (-↑k) = -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))
<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>n : ℕ<VAR>hk : 2 * n ≠ 0<GOAL>hurwitzZeta (↑x) (-↑(2 * n)) = -1 / (↑(2 * n) + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))
<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>n : ℕ<VAR>hk : 2 * n + 1 ≠ 0<GOAL>hurwitzZeta (↑x) (-↑(2 * n + 1)) = -1 / (↑(2 * n + 1) + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1 + 1)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>a⁻¹ ≤ b ↔ 1 ≤ a * b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>1 / a ≤ b ↔ 1 ≤ a * b
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w₁ w₂ : W<GOAL>cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2