ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Set.range ⇑(pullback.snd f g).val.base = (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>⇑(pullback.snd (Scheme.forgetToTop.map f) (Scheme.forgetToTop.map g)) '' (⇑(pullback.fst f.val.base g.val.base) ⁻¹' Set.univ) = (g ⁻¹ᵁ Scheme.Hom.opensRange f).carrier
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Function.Surjective ⇑(PreservesPullback.iso Scheme.forgetToTop f g).hom
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<GOAL>Epi (PreservesPullback.iso Scheme.forgetToTop f g).hom
<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]<GOAL>-x ≡ -y [SMOD U]
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n k : ℕ<VAR>h : k < count p n<GOAL>nth p k < n
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n k : ℕ<VAR>h : k < count p n<GOAL>count p (nth p k) < count p n
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n k : ℕ<VAR>h : k < count p n<GOAL>∀ (hf : (setOf p).Finite), k < hf.toFinset.card
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝² : StrictOrderedCommSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>a b : E<GOAL>Convex 𝕜 (openSegment 𝕜 a b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝² : StrictOrderedCommSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>a b : E<GOAL>∀ ⦃x : E⦄, x ∈ openSegment 𝕜 a b → ∀ ⦃y : E⦄, y ∈ openSegment 𝕜 a b → openSegment 𝕜 x y ⊆ openSegment 𝕜 a b
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>i j : Fin (n + 1)<VAR>h : j < i<VAR>x : α i<VAR>p : (k : Fin n) → α (i.succAbove k)<GOAL>i.insertNth x p j = Eq.recOn ⋯ (p (j.castPred ⋯))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ ⌊b⌋
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Icc s t).card = 2 ^ (t.card - s.card)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>Set.InjOn (fun x => s ∪ x) ↑(t \ s).powerset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>u : Finset α<VAR>hu : u ∈ ↑(t \ s).powerset<VAR>v : Finset α<VAR>hv : v ∈ ↑(t \ s).powerset<VAR>huv : s ⊔ u = s ⊔ v<GOAL>u = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>u : Finset α<VAR>hu : u ⊆ t \ s<VAR>v : Finset α<VAR>hv : v ⊆ t \ s<VAR>huv : s ⊔ u = s ⊔ v<GOAL>u = v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>r.preimage Set.univ = r.dom
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>x✝³ x✝² x✝¹ x✝ : Associates α<GOAL>DvdNotUnit x✝¹ x✝ ↔ x✝¹ < x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : DecidableEq β<VAR>hf : HasProd f a<VAR>b : β<GOAL>HasProd (fun n => if n = b then 1 else f n) (a / f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : DecidableEq β<VAR>hf : HasProd f a<VAR>b : β<GOAL>(fun n => if n = b then 1 else f n) = update f b 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : CommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : DecidableEq β<VAR>hf : HasProd f a<VAR>b : β<GOAL>a / f b = 1 / f b * a
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝⁴ : TopologicalSpace X✝<VAR>inst✝³ : TopologicalSpace Y<VAR>s t : Set X✝<VAR>X : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : Infinite X<GOAL>∃ z, (𝓝[≠] z).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ<VAR>f : β → α<VAR>hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)<GOAL>IsBounded (range f)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>f : β → α<VAR>hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)<VAR>s : Set β<VAR>hsf : s.Finite<VAR>hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}<GOAL>IsBounded (range f)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>f : β → α<VAR>hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)<VAR>s : Set β<VAR>hsf : s.Finite<VAR>hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}<GOAL>IsBounded (f '' ?m.14806 ∪ f '' ?m.14806ᶜ)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>f : β → α<VAR>hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)<VAR>s : Set β<VAR>hsf : s.Finite<VAR>hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}<GOAL>Set β
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ : α<VAR>s✝ t : Set α<VAR>r : ℝ<VAR>f : β → α<VAR>hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)<VAR>s : Set β<VAR>hsf : s.Finite<VAR>hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}<VAR>x : β<VAR>hx : x ∈ sᶜ<VAR>y : β<VAR>hy : y ∈ sᶜ<GOAL>dist (f x) (f y) ≤ 1
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ comap f I<VAR>h : comap f I ≤ J<GOAL>Injective ⇑(quotientMap I f H)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ comap f I<VAR>h : comap f I ≤ J<VAR>a : R ⧸ J<VAR>ha : (quotientMap I f H) a = 0<GOAL>a = 0
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ comap f I<VAR>h : comap f I ≤ J<VAR>r : R<VAR>ha : (quotientMap I f H) ((Quotient.mk J) r) = 0<GOAL>(Quotient.mk J) r = 0
<VAR>R : Type u<VAR>S✝ : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S✝<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>J : Ideal R<VAR>I : Ideal S<VAR>f : R →+* S<VAR>H : J ≤ comap f I<VAR>h : comap f I ≤ J<VAR>r : R<VAR>ha : f r ∈ I<GOAL>(Quotient.mk J) r = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>a b c : ℕ<GOAL>ofAdd (-↑c) ≤ max (ofAdd (-↑a)) (ofAdd (-↑b)) ↔ min a b ≤ c
<VAR>C : Type uC<VAR>inst✝³ : Category.{vC, uC} C<VAR>D : Type uD<VAR>inst✝² : Category.{vD, uD} D<VAR>G✝ : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.9506, u_1} A<VAR>G : C ⥤ D<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>X Y : C<VAR>i₁ i₂ : X ⟶ Y<VAR>e : G.map i₁ = G.map i₂<VAR>s t : ℱ.val.obj (op (G.obj X))<VAR>h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t<GOAL>s = t
<VAR>C : Type uC<VAR>inst✝³ : Category.{vC, uC} C<VAR>D : Type uD<VAR>inst✝² : Category.{vD, uD} D<VAR>G✝ : C ⥤ D<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.9506, u_1} A<VAR>G : C ⥤ D<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>X Y : C<VAR>i₁ i₂ : X ⟶ Y<VAR>e : G.map i₁ = G.map i₂<VAR>s t : ℱ.val.obj (op (G.obj X))<VAR>h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ → ℱ.val.map (G.map j).op s = ℱ.val.map (G.map j).op t<GOAL>∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄, (Sieve.functorPushforward G (Sieve.equalizer i₁ i₂)).arrows f → ℱ.val.map f.op s = ℱ.val.map f.op t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>r : R<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f ((fun x => r * x) '' spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f (r * x)) a = cfc f (r • a)
<VAR>E : Type u_1<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : T2Space E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<VAR>F : Type u_1 := E<GOAL>μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : T2Space E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<VAR>F : Type u_1 := E<VAR>this : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<GOAL>μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : T2Space E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<VAR>F : Type u_1 := E<VAR>this✝³ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝² : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝¹ : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝ : MeasurableSpace F := borel F<VAR>this : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<GOAL>μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : T2Space E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<VAR>F : Type u_1 := E<VAR>this✝⁴ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝³ : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝² : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<VAR>this : ν.IsAddHaarMeasure<GOAL>μ {x | g x < 1} = ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1))
<VAR>E : Type u_1<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : T2Space E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<VAR>F : Type u_1 := E<VAR>this✝⁴ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝³ : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝² : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<VAR>this : ν.IsAddHaarMeasure<GOAL>μ {x | g x < 1} = ν (Metric.ball 0 1)
<VAR>E : Type u_1<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>mE : MeasurableSpace E<VAR>tE : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : T2Space E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>g : E → ℝ<VAR>h1 : g 0 = 0<VAR>h2 : ∀ (x : E), g (-x) = g x<VAR>h3 : ∀ (x y : E), g (x + y) ≤ g x + g y<VAR>h4 : ∀ {x : E}, g x = 0 → x = 0<VAR>h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x<VAR>p : ℝ<VAR>hp : 0 < p<VAR>F : Type u_1 := E<VAR>this✝⁴ : NormedAddCommGroup F := NormedAddCommGroup.mk ⋯<VAR>this✝³ : NormedSpace ℝ F := NormedSpace.mk ⋯<VAR>this✝² : TopologicalSpace F := UniformSpace.toTopologicalSpace<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>φ : E ≃L[ℝ] F := (LinearEquiv.refl ℝ E).toContinuousLinearEquiv<VAR>ν : Measure F := map (⇑φ) μ<VAR>this : ν.IsAddHaarMeasure<GOAL>ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p) ∂μ) / Real.Gamma (↑(finrank ℝ E) / p + 1)) = ENNReal.ofReal ((∫ (x : F), Real.exp (-‖x‖ ^ p) ∂ν) / Real.Gamma (↑(finrank ℝ F) / p + 1))
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter<GOAL>WithSeminorms p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter<GOAL>𝓝 0 = 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>h : 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter<GOAL>𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>this : DecidableEq V<GOAL>∃ w, w ≠ v ∧ Odd (G.degree w)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>this : DecidableEq V<VAR>k : ℕ<VAR>hg : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card = 2 * k + 1<GOAL>∃ w, w ≠ v ∧ Odd (G.degree w)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>this : DecidableEq V<VAR>k : ℕ<VAR>hg : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card = 2 * k + 1<VAR>hg' : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card > 0<GOAL>∃ w, w ≠ v ∧ Odd (G.degree w)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>this : DecidableEq V<VAR>k : ℕ<VAR>hg : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card = 2 * k + 1<VAR>hg' : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card > 0<VAR>w : V<VAR>hw : w ∈ filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ<GOAL>∃ w, w ≠ v ∧ Odd (G.degree w)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<VAR>this : DecidableEq V<VAR>k : ℕ<VAR>hg : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card = 2 * k + 1<VAR>hg' : (filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ).card > 0<VAR>w : V<VAR>hw : ¬w = v ∧ Odd (G.degree w)<GOAL>∃ w, w ≠ v ∧ Odd (G.degree w)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : AddGroup E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : DistribMulAction 𝕜 E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<GOAL>Absorbs 𝕜 U (-s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : SeminormedRing 𝕜<VAR>inst✝³ : AddGroup E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : DistribMulAction 𝕜 E<VAR>s t : Set E<VAR>hs : IsVonNBounded 𝕜 s<VAR>U : Set E<VAR>hU : U ∈ 𝓝 0<GOAL>Absorbs 𝕜 (- -U) (-s)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>D₃ : Type u₆<VAR>inst✝⁸ : Category.{v₁, u₁} C₁<VAR>inst✝⁷ : Category.{v₂, u₂} C₂<VAR>inst✝⁶ : Category.{v₃, u₃} C₃<VAR>inst✝⁵ : Category.{v₄, u₄} D₁<VAR>inst✝⁴ : Category.{v₅, u₅} D₂<VAR>inst✝³ : Category.{v₆, u₆} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>G : D₁ ⥤ D₂<VAR>inst✝ : (Φ.functor ⋙ L₂).IsLocalization W₁<VAR>this : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)<GOAL>Φ.IsLocalizedEquivalence
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>a : G<VAR>b : k<GOAL>single a b ^ 0 = single (a ^ 0) (b ^ 0)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>a : G<VAR>b : k<GOAL>1 = single 1 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>a : G<VAR>b : k<VAR>n : ℕ<GOAL>single a b ^ (n + 1) = single (a ^ (n + 1)) (b ^ (n + 1))
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>W : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : AddCommMonoid W<VAR>inst✝⁶ : AddCommMonoid X<VAR>inst✝⁵ : AddCommMonoid Y<VAR>inst✝⁴ : AddCommMonoid Z<VAR>inst✝³ : Module R W<VAR>inst✝² : Module R X<VAR>inst✝¹ : Module R Y<VAR>inst✝ : Module R Z<GOAL>(LinearMap.lTensor W ↑(assoc R X Y Z) ∘ₗ ↑(assoc R W (X ⊗[R] Y) Z)) ∘ₗ LinearMap.rTensor Z ↑(assoc R W X Y) = ↑(assoc R W X (Y ⊗[R] Z)) ∘ₗ ↑(assoc R (W ⊗[R] X) Y Z)
<VAR>R : Type u<VAR>inst✝⁸ : CommRing R<VAR>W : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝⁷ : AddCommMonoid W<VAR>inst✝⁶ : AddCommMonoid X<VAR>inst✝⁵ : AddCommMonoid Y<VAR>inst✝⁴ : AddCommMonoid Z<VAR>inst✝³ : Module R W<VAR>inst✝² : Module R X<VAR>inst✝¹ : Module R Y<VAR>inst✝ : Module R Z<GOAL>∀ (w : W) (x : X) (y : Y) (z : Z), ((LinearMap.lTensor W ↑(assoc R X Y Z) ∘ₗ ↑(assoc R W (X ⊗[R] Y) Z)) ∘ₗ LinearMap.rTensor Z ↑(assoc R W X Y)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) = (↑(assoc R W X (Y ⊗[R] Z)) ∘ₗ ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>log (x * ↑r) = ↑(Real.log r) + log x
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>h : l ≠ []<GOAL>l.cyclicPermutations.length = l.length
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ p x✝ : P<GOAL>x✝ ∈ ↑⊤ → x✝ ∈ ↑(perpBisector p p)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : Fintype Ω<VAR>s : Set Ω<GOAL>(condCount Set.univ) s = Measure.count s / ↑(Fintype.card Ω)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : Fintype Ω<VAR>s : Set Ω<GOAL>Measure.count s / Measure.count Set.univ = Measure.count s / ↑(Fintype.card Ω)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : Fintype Ω<VAR>s : Set Ω<GOAL>Measure.count Set.univ = ↑(Fintype.card Ω)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : Fintype Ω<VAR>s : Set Ω<GOAL>∑ x : Ω, 1 = ↑(Fintype.card Ω)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : Fintype Ω<VAR>s : Set Ω<GOAL>MeasurableSet ↑Finset.univ
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : ContinuousConstSMul G α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<VAR>c : G<GOAL>(Continuous fun x => c • f x) ↔ Continuous f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ↥(Lp E p μ)<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C<VAR>hμ : ¬μ = 0<GOAL>‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ↥(Lp E p μ)<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C<VAR>hμ : ¬μ = 0<GOAL>eLpNorm (↑↑f) p μ ≤ ↑(measureUnivNNReal μ ^ p.toReal⁻¹ * C)