ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0<GOAL>0 ≤ᶠ[ae (volume.restrict (Ioi 0))] fun x => rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>this : (Function.support fun x => rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0<GOAL>IntegrableOn (fun x => rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : SeminormedAddCommGroup F<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : NormedSpace 𝕜 G<VAR>x✝ : E × F<VAR>e : E<VAR>f : F<GOAL>‖(fst 𝕜 E F) (e, f)‖ ≤ 1 * ‖(e, f)‖
<VAR>b : Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ left b<GOAL>Finset.card (moveLeft b m) / 2 < Finset.card b / 2
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<VAR>n : ℕ<VAR>h1 : n ≠ 1<VAR>h2 : Odd n<VAR>h0 : n ≠ 0<GOAL>reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj ((J.plusObj P).obj (op X))<GOAL>∃ S y, x = mk y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj ((J.plusObj P).obj (op X))<VAR>S : (J.Cover X)ᵒᵖ<VAR>y : (forget D).obj ((J.diagram P X).obj S)<VAR>h : (colimit.ι (J.diagram P X) S) y = x<GOAL>∃ S y, x = mk y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>x : (forget D).obj ((J.plusObj P).obj (op X))<VAR>S : (J.Cover X)ᵒᵖ<VAR>y : (forget D).obj ((J.diagram P X).obj S)<VAR>h : (colimit.ι (J.diagram P X) S) y = x<GOAL>x = mk ((Meq.equiv P (unop S)) y)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>count a [b] = if a = b then 1 else 0
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J✝ K L : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, I ⊔ J i = ⊤<GOAL>(fun J => I ⊔ J = ⊤) 1
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<GOAL>x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>x✝ : Box ι<GOAL>x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ ↑x✝
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>(fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : NeZero μ<VAR>t : Set β<VAR>h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)<GOAL>NullMeasurableSet (?m.120828 ×ˢ t) (?m.120825.prod ν)
<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✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>htwo : p ^ (k - s + 1) ≠ 2<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<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✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>htwo : p ^ (k - s + 1) ≠ 2<VAR>this : NumberField K<GOAL>(Algebra.norm ℤ) (hζ.toInteger ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s
<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✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>s : ℕ<VAR>hs : s ≤ k<VAR>htwo : p ^ (k - s + 1) ≠ 2<VAR>this : NumberField K<GOAL>(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger ^ ↑p ^ s - 1)) = (algebraMap ℤ ℚ) (↑↑p ^ ↑p ^ s)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>inst✝ : TopologicalSpace Y<VAR>α : Type<VAR>X : α → TopCat<GOAL>(piComparison (yonedaPresheaf' Y) fun x => op (X x)) = (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫ (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv ≫ (Types.productIso fun i => C(↑(X i), Y)).inv
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>inst✝ : TopologicalSpace Y<VAR>α : Type<VAR>X : α → TopCat<GOAL>(piComparison (yonedaPresheaf' Y) fun x => op (X x)) ≫ (Types.productIso fun i => C(↑(X i), Y)).hom = (yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫ (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>inst✝ : TopologicalSpace Y<VAR>α : Type<VAR>X : α → TopCat<VAR>a✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x => op (X x))<VAR>x✝ : α<VAR>a✝ : ↑(X x✝)<GOAL>(((piComparison (yonedaPresheaf' Y) fun x => op (X x)) ≫ (Types.productIso fun i => C(↑(X i), Y)).hom) a✝¹ x✝) a✝ = (((yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫ (equivEquivIso (sigmaEquiv Y fun x => ↑(X x))).inv) a✝¹ x✝) a✝
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>inst✝ : TopologicalSpace Y<VAR>α : Type<VAR>X : α → TopCat<VAR>a✝¹ : (yonedaPresheaf' Y).obj (∏ᶜ fun x => op (X x))<VAR>x✝ : α<VAR>a✝ : ↑(X x✝)<GOAL>a✝¹ ((Sigma.ι X x✝ ≫ (opCoproductIsoProduct X).inv.unop) a✝) = a✝¹ (((TopCat.sigmaIsoSigma X).inv ≫ (opCoproductIsoProduct X).inv.unop) ⟨x✝, a✝⟩)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>toFinsupp✝ : AddMonoidAlgebra R ℕ<GOAL>((opRingEquiv R) (op { toFinsupp := toFinsupp✝ })).support = (unop (op { toFinsupp := toFinsupp✝ })).support
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>y : M<GOAL>polar (⇑Q) 0 y = 0
<VAR>X : Scheme<VAR>inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : IsNilpotent s<GOAL>s = 0
<VAR>X : Scheme<VAR>inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : IsNilpotent s<GOAL>∀ (x : ↥U), (X.sheaf.presheaf.germ x) s = (X.sheaf.presheaf.germ x) 0
<VAR>X : Scheme<VAR>inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : IsNilpotent s<VAR>x : ↥U<GOAL>(X.sheaf.presheaf.germ x) s = (X.sheaf.presheaf.germ x) 0
<VAR>X : Scheme<VAR>inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : IsNilpotent s<VAR>x : ↥U<GOAL>(X.sheaf.presheaf.germ x) s = 0
<VAR>X : Scheme<VAR>inst✝ : ∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : IsNilpotent s<VAR>x : ↥U<GOAL>(X.presheaf.germ x) s = 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>h : 𝟙 X = 0<VAR>Y : C<VAR>f : X ⟶ Y<GOAL>f = default
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>h : 𝟙 X = 0<VAR>Y : C<VAR>f : X ⟶ Y<GOAL>0 = default
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>h : 𝟙 X = 0<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>f = default
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : HasZeroMorphisms C<VAR>X : C<VAR>h : 𝟙 X = 0<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>0 = default
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>q : ι' → Prop<VAR>hp : ∃ i, p i<VAR>hq : ∃ j, q j<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ (i : ι), p i → ∀ (j : ι'), q j → f i + g j ≤ a<GOAL>(⨆ i, ⨆ (_ : p i), f i) + ⨆ j, ⨆ (_ : q j), g j ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>p : ι → Prop<VAR>q : ι' → Prop<VAR>hp : ∃ i, p i<VAR>hq : ∃ j, q j<VAR>f : ι → ℝ≥0∞<VAR>g : ι' → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>h : ∀ (i : ι), p i → ∀ (j : ι'), q j → f i + g j ≤ a<GOAL>⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<GOAL>LinearMap.range (Finsupp.totalOn α M R v s) = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>s : Set α<GOAL>span R (v '' s) ≤ map (Finsupp.total α M R v) (supported R R s)
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hp : 0 ≤ p<GOAL>ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : Simple Y<VAR>i : X ≅ Y<VAR>Y✝ : C<VAR>f : Y✝ ⟶ X<VAR>m : Mono f<GOAL>IsIso f ↔ f ≠ 0
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>inst✝ : Simple Y<VAR>i : X ≅ Y<VAR>Y✝ : C<VAR>f : Y✝ ⟶ X<VAR>m : Mono f<VAR>this : Mono (f ≫ i.hom)<GOAL>IsIso f ↔ f ≠ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>o.card = 0 ↔ o = 0
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : CommRing C<VAR>inst✝³ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι'<VAR>b : Basis ι A B<VAR>f : ι ≃ ι'<GOAL>discr A (⇑b ∘ ⇑f.symm) = discr A ⇑b
<VAR>n a : ℕ<VAR>h : a < n<GOAL>(↑a).val = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : NeZero 1<VAR>n : ℕ<GOAL>0 < ↑n ↔ 0 < n
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : K_hat R K<VAR>hx : x.IsFiniteAdele<VAR>hy : y.IsFiniteAdele<GOAL>(x + y).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : K_hat R K<VAR>hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite<VAR>hy : {x | y x ∉ adicCompletionIntegers K x}.Finite<GOAL>{x_1 | (x + y) x_1 ∉ adicCompletionIntegers K x_1}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : K_hat R K<VAR>hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite<VAR>hy : {x | y x ∉ adicCompletionIntegers K x}.Finite<VAR>h_subset : {v | (x + y) v ∉ adicCompletionIntegers K v} ⊆ {v | x v ∉ adicCompletionIntegers K v} ∪ {v | y v ∉ adicCompletionIntegers K v}<GOAL>{x_1 | (x + y) x_1 ∉ adicCompletionIntegers K x_1}.Finite
<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>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤<GOAL>Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))
<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>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤<VAR>A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))<GOAL>Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))
<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>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤<VAR>A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))<VAR>B : Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))<GOAL>Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ (closure s)))
<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>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤<VAR>A : Tendsto (fun r => μ (cthickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))<VAR>B : Tendsto (fun r => μ (cthickening r s)) (𝓝[≤] 0) (𝓝 (μ (closure s)))<GOAL>𝓝 0 = 𝓝[≤] 0 ⊔ 𝓝[>] 0
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>a ⨳ b ⨳ c = a ⨳ (b ⨳ c)
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>a ⨳ b ⨳ c ≤ a ⨳ (b ⨳ c)
<VAR>a✝ b✝ c✝ d : Ordinal.{u}<VAR>a b c : Ordinal.{u_1}<GOAL>a ⨳ (b ⨳ c) ≤ a ⨳ b ⨳ c
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>m : ℤ<GOAL>((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>m : ℤ<VAR>hn : 0 < n<GOAL>((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn✝ : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>m : ℤ<VAR>hn : 0 < n<GOAL>(autEquivRootsOfUnity ⋯ hn H L) ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) • α = ζ ^ m • α
<VAR>α✝ : Type u_1<VAR>β✝ : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α✝<VAR>s t : Multiset α✝<VAR>f✝ g : α✝ → Multiset β✝<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : α → Multiset β<VAR>S : Multiset α<VAR>x : α<VAR>hx : x ∈ S<GOAL>f x ≤ S.bind f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>(∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set R), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap f ↑r)) → P f) ↔ ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap f ↑r)) → P f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b), (∀ (s : Set a), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e ↑r)) → P e) ↔ ∀ (s : Finset a), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e ↑r)) → P e
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>C : Set α<GOAL>Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S✝ : Sieve X<VAR>R✝ : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>R S : Sieve X<VAR>hR : Presieve.IsSheafFor P R.arrows<VAR>hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows<VAR>hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows<VAR>this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows<GOAL>Presieve.IsSheafFor P S.arrows
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S✝ : Sieve X<VAR>R✝ : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>R S : Sieve X<VAR>hR : Presieve.IsSheafFor P R.arrows<VAR>hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows<VAR>hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows<VAR>this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows<GOAL>Presieve.IsSheafFor P (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P✝ : Cᵒᵖ ⥤ Type v<VAR>X Y : C<VAR>S✝ : Sieve X<VAR>R✝ : Presieve X<VAR>J J₂ : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>R S : Sieve X<VAR>hR : Presieve.IsSheafFor P R.arrows<VAR>hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows<VAR>hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Presieve.IsSheafFor P (Sieve.pullback f S).arrows<VAR>this : (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S).arrows ≤ S.arrows<GOAL>∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.bind R.arrows fun Y f x => Sieve.pullback f S)).arrows
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<GOAL>∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<GOAL>∀ j ≥ n, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>padicNorm p (↑(nthHom f (r * s) j) - ↑(nthHom f r j) * ↑(nthHom f s j)) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>padicNorm p (↑(nthHom f (r * s) j) - ↑(nthHom f r j) * ↑(nthHom f s j)) ≤ ↑p ^ (-↑n)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(nthHom f (r * s) j - nthHom f r j * nthHom f s j) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(↑((f j) (r * s)).val - ↑((f j) r).val * ↑((f j) s).val) = 0
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>r s : R<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : ↑p ^ (-↑n) < ε<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>((f j) r * (f j) s).cast - ((f j) r).cast * ((f j) s).cast = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>diam {x, y} = edist x y
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Groupoid D<VAR>inst✝² : Category.{?u.4103, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>G.map f ≫ (ihom.coev (F.obj Y)).app (G.obj Y) = (ihom.coev (F.obj X)).app (G.obj X) ≫ (F.closedIhom.obj (F ⊗ G)).map f