ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Gamma s * Gamma (s + 1 / 2) = Gamma s * Gamma (s + 1 / 2) * 2 ^ (2 * s - 1) / √π * (2 ^ (2 * s - 1))⁻¹ * √π
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Gamma s * Gamma ((s * 2 + 1) / 2) * (√π * 2 ^ (2 * s - 1)) = Gamma s * Gamma ((s * 2 + 1) / 2) * 2 ^ (2 * s - 1) * √π
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<GOAL>boundedBy 0 = 0
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<GOAL>boundedBy 0 ≤ ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N N₁ N₂ P P₁ P₂ : Submodule R M<VAR>I : Ideal R<VAR>x r : R<GOAL>r ∈ colon I (Ideal.span {x}) ↔ r * x ∈ I
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<GOAL>Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<GOAL>Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank E ↥(separableClosure E K)) = Cardinal.lift.{v, w} (Module.rank F ↥(restrictScalars F (separableClosure E K)))
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedSpace 𝕜 G<VAR>R : Type u_5<VAR>𝕜₂ : Type u_6<VAR>𝕜' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>M : Type u_8<VAR>inst✝⁷ : TopologicalSpace M<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>G' : Type u_9<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜₂ G'<VAR>inst✝⁴ : NormedSpace 𝕜' G'<VAR>inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>ρ₁₂ : R →+* 𝕜'<VAR>f : M →SL[ρ₁₂] F →SL[σ₁₂] G'<VAR>x : M<VAR>y : F<GOAL>(f (-x)) y = -(f x) y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : OrderedCommMonoid α<VAR>s t : Multiset α<VAR>a : α<VAR>l : List α<VAR>hl : ∀ x ∈ ⟦l⟧, 1 ≤ x<VAR>x : α<VAR>hx : x ∈ ⟦l⟧<GOAL>x ≤ prod ⟦l⟧
<VAR>𝕜 : Type v<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<VAR>p : Submodule 𝕜 E := span 𝕜 {x}<VAR>f : ↥(span 𝕜 {x}) →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h<GOAL>∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
<VAR>𝕜 : Type v<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<VAR>p : Submodule 𝕜 E := span 𝕜 {x}<VAR>f : ↥(span 𝕜 {x}) →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h<VAR>g : E →L[𝕜] 𝕜<VAR>hg : (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖<GOAL>∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
<VAR>d : ℤ<VAR>a : Solution₁ d<GOAL>a.x ^ 2 = 1 + d * a.y ^ 2
<VAR>d : ℤ<VAR>a : Solution₁ d<GOAL>a.x ^ 2 = a.x ^ 2 - d * a.y ^ 2 + d * a.y ^ 2
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>x : α<VAR>n : ℕ<GOAL>m < replicate (n + 1) x ↔ m ≤ replicate n x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>m : Multiset α<VAR>x : α<VAR>n : ℕ<GOAL>(∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₁ : ∀ (l : ι), ¬c.Rel l k₁<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>(dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i k₁ k₀ : ι<VAR>r₁₀ : c.Rel k₁ k₀<VAR>hk₁ : ∀ (l : ι), ¬c.Rel l k₁<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<GOAL>¬c.Rel (c.prev k₁) k₁
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom = (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv = ((Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X)) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>((evaluation C D).obj X).map (cokernel.π α) ≫ 𝟙 (((evaluation C D).obj X).obj (cokernel α)) = (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(cokernel.π α).app X ≫ 𝟙 ((cokernel α).obj X) = 𝟙 (G.obj X) ≫ cokernel.π (α.app X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type w<VAR>inst✝¹ : Category.{z, w} D<VAR>inst✝ : Abelian D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(cokernel.π α).app X = cokernel.π (α.app X) ≫ cokernelComparison α ((evaluation C D).obj X)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.17195, u_1} C₁<VAR>inst✝⁴ : Category.{?u.17199, u_2} C₂<VAR>inst✝³ : Category.{?u.17203, u_3} C₃<VAR>inst✝² : Category.{?u.17207, u_4} C₄<VAR>inst✝¹ : Category.{?u.17211, u_5} C₁₂<VAR>inst✝ : Category.{?u.17215, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>ψ : X₂ ⟶ Y₂<VAR>X₃ : GradedObject I₃ C₃<VAR>x : I₁ × I₂ × I₃<GOAL>((F.obj (X₁ x.1)).map (ψ x.2.1)).app (X₃ x.2.2) ≫ ((F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2) = ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2) ≫ ((F.obj (Y₁ x.1)).map (ψ x.2.1)).app (X₃ x.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.17195, u_1} C₁<VAR>inst✝⁴ : Category.{?u.17199, u_2} C₂<VAR>inst✝³ : Category.{?u.17203, u_3} C₃<VAR>inst✝² : Category.{?u.17207, u_4} C₄<VAR>inst✝¹ : Category.{?u.17211, u_5} C₁₂<VAR>inst✝ : Category.{?u.17215, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>ψ : X₂ ⟶ Y₂<VAR>X₃ : GradedObject I₃ C₃<VAR>x : I₁ × I₂ × I₃<GOAL>((F.obj (X₁ x.1)).map (ψ x.2.1) ≫ (F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2) = ((F.map (φ x.1)).app (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1)).app (X₃ x.2.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.17195, u_1} C₁<VAR>inst✝⁴ : Category.{?u.17199, u_2} C₂<VAR>inst✝³ : Category.{?u.17203, u_3} C₃<VAR>inst✝² : Category.{?u.17207, u_4} C₄<VAR>inst✝¹ : Category.{?u.17211, u_5} C₁₂<VAR>inst✝ : Category.{?u.17215, u_6} C₂₃<VAR>F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>X₁ Y₁ : GradedObject I₁ C₁<VAR>φ : X₁ ⟶ Y₁<VAR>X₂ Y₂ : GradedObject I₂ C₂<VAR>ψ : X₂ ⟶ Y₂<VAR>X₃ : GradedObject I₃ C₃<VAR>x : I₁ × I₂ × I₃<GOAL>(F.obj (X₁ x.1)).map (ψ x.2.1) ≫ (F.map (φ x.1)).app (Y₂ x.2.1) = (F.map (φ x.1)).app (X₂ x.2.1) ≫ (F.obj (Y₁ x.1)).map (ψ x.2.1)
<VAR>n : ℕ<GOAL>antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map succ id) (antidiagonal n)
<VAR>n : ℕ<GOAL>(0, n + 1) :: (succ 0, n) :: map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) = (0, n + 1) :: (succ 0, n) :: map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)
<VAR>n : ℕ<GOAL>map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) = map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>(locallyRingedSpaceMap (f ≫ g)).val = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).val
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>sheafedSpaceMap g ≫ sheafedSpaceMap f = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n i : ℕ<VAR>x : α<VAR>l : List α<GOAL>(n + i, x) ∈ enumFrom n l ↔ l.get? i = some x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>z : ℂ<GOAL>Complex.orientation.rightAngleRotation z = I * z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>z : ℂ<GOAL>∀ (v : ℂ), ⟪Complex.orientation.rightAngleRotation z, v⟫_ℝ = ⟪I * z, v⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>z w : ℂ<GOAL>⟪Complex.orientation.rightAngleRotation z, w⟫_ℝ = ⟪I * z, w⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>z w : ℂ<GOAL>(Complex.orientation.areaForm z) w = ⟪I * z, w⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>z w : ℂ<GOAL>z.re * w.im + -z.im * w.re = (-0 * z.re - -1 * -z.im) * w.re - (-0 * -z.im + -1 * z.re) * w.im
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>((quotient C (ComplexShape.up ℤ)).map ((CochainComplex.mappingCone.triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f)) ≫ ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (CochainComplex.mappingCone f)) ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map (𝟙 ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone f))) = (quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom ≫ (quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃ ≫ ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (CochainComplex.mappingCone f)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(quotient C (ComplexShape.up ℤ)).map ((CochainComplex.mappingCone.triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f)) ≫ ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (CochainComplex.mappingCone f) = (quotient C (ComplexShape.up ℤ)).map ((CochainComplex.mappingConeCompHomotopyEquiv f g).hom ≫ (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃) ≫ ((quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app (CochainComplex.mappingCone f)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(CochainComplex.mappingCone.triangle g).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f) = (CochainComplex.mappingConeCompHomotopyEquiv f g).hom ≫ (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>f : ℕ → G<GOAL>(CauchySeq fun s => ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>f : ℕ → G<VAR>vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : UniformSpace G<VAR>inst✝ : UniformGroup G<VAR>f : ℕ → G<VAR>vanish : ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
<VAR>u v : ℤ<GOAL>IsUnit u ↔ u.natAbs = 1
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i✝ : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>i : δ<VAR>hi : i ∉ s<VAR>x : (i : δ) → π i<GOAL>(∫⋯∫⁻_insert i s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s, f ∂μ) (update x i xᵢ) ∂μ i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a : α<GOAL>op '' s⁻¹ = (op '' s)⁻¹
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>(∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a) ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : StrictOrderedRing α<VAR>inst✝ : Archimedean α<VAR>x : α<VAR>n : ℕ<VAR>h : x < ↑n<GOAL>x < ↑↑n
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>S : Set β<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : UniformEquicontinuousOn F S<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>U ∈ map (fun x => (f x.1, f x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>S : Set β<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : UniformEquicontinuousOn F S<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>(fun x => (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>S : Set β<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : UniformEquicontinuousOn F S<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<GOAL>(fun x => (f x.1, f x.2)) ⁻¹' U ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>S : Set β<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : UniformEquicontinuousOn F S<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<GOAL>∀ (a : β × β), (∀ (i : ι), (F i a.1, F i a.2) ∈ V) → a ∈ S ×ˢ S → a ∈ (fun x => (f x.1, f x.2)) ⁻¹' U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>S : Set β<VAR>h₁ : ∀ x ∈ S, Tendsto (fun x_1 => F x_1 x) l (𝓝 (f x))<VAR>h₂ : UniformEquicontinuousOn F S<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVclosed : IsClosed V<VAR>hVU : V ⊆ U<VAR>x y : β<VAR>hxy : ∀ (i : ι), (F i (x, y).1, F i (x, y).2) ∈ V<VAR>hxS : (x, y).1 ∈ S<VAR>hyS : (x, y).2 ∈ S<GOAL>(x, y) ∈ (fun x => (f x.1, f x.2)) ⁻¹' U
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>φ' : S' ⟶ R<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ↑(R.obj X)<GOAL>((relativeDifferentials' φ').map f) (CommRingCat.KaehlerDifferential.d x) = CommRingCat.KaehlerDifferential.d ((R.map f) x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s s₁ s₂ t t₁ t₂ u : Finset α<VAR>a b c : α<GOAL>(s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K✝ : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing A'<VAR>inst✝⁷ : CommRing A''<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R A''<VAR>a b : R<VAR>K : Type u_9<VAR>inst✝³ : CommRing K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra K A<VAR>inst✝ : IsScalarTower R K A<VAR>hinj : Injective ⇑(algebraMap R K)<VAR>ai : AlgebraicIndependent K x<GOAL>AlgebraicIndependent R x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K✝ : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing A'<VAR>inst✝⁷ : CommRing A''<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R A''<VAR>a b : R<VAR>K : Type u_9<VAR>inst✝³ : CommRing K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra K A<VAR>inst✝ : IsScalarTower R K A<VAR>hinj : Injective ⇑(algebraMap R K)<VAR>ai : AlgebraicIndependent K x<VAR>this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom<GOAL>AlgebraicIndependent R x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K✝ : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing A'<VAR>inst✝⁷ : CommRing A''<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R A''<VAR>a b : R<VAR>K : Type u_9<VAR>inst✝³ : CommRing K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra K A<VAR>inst✝ : IsScalarTower R K A<VAR>hinj : Injective ⇑(algebraMap R K)<VAR>ai : AlgebraicIndependent K x<VAR>this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom<GOAL>Injective ⇑(aeval x).toRingHom
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K✝ : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing A'<VAR>inst✝⁷ : CommRing A''<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R A'<VAR>inst✝⁴ : Algebra R A''<VAR>a b : R<VAR>K : Type u_9<VAR>inst✝³ : CommRing K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : Algebra K A<VAR>inst✝ : IsScalarTower R K A<VAR>hinj : Injective ⇑(algebraMap R K)<VAR>ai : AlgebraicIndependent K x<VAR>this : (aeval x).comp (MvPolynomial.map (algebraMap R K)) = (aeval x).toRingHom<GOAL>Injective (⇑(aeval x).toRingHom ∘ ⇑(MvPolynomial.map (algebraMap R K)))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>f : R →+* S<VAR>t : Subsemiring S<VAR>h : t ≤ f.rangeS<GOAL>map f (comap f t) = t
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedRing 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>x y : E<VAR>hs : StrictConvex 𝕜 s<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>hx₀ : x ≠ 0<VAR>t : 𝕜<VAR>ht₀ : 0 < t<VAR>ht₁ : t < 1<GOAL>t • x ∈ interior s
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>p : ℝ<GOAL>LiouvilleWith p x
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>p : ℝ<GOAL>LiouvilleWith (↑⌈p⌉₊) x
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>p : ℝ<GOAL>∀ (x_1 : ℕ), (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) → ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊
<VAR>x : ℝ<VAR>hx : Liouville x<VAR>p : ℝ<VAR>b : ℕ<VAR>_hb : 1 < b<VAR>a : ℤ<VAR>hne : x ≠ ↑a / ↑b<VAR>hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊<GOAL>|x - ↑a / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>(𝓝 0).HasBasis (fun x => True) fun γ => {x | v x < ↑γ}
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>pa : p a = true<VAR>x : α<VAR>xs l₂ : List α<VAR>h : a ∈ x :: xs<VAR>h' : ¬p x = true<GOAL>eraseP p (xs ++ l₂) = eraseP p xs ++ l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>pa : p a = true<VAR>x : α<VAR>xs l₂ : List α<VAR>h : a ∈ x :: xs<VAR>h' : ¬p x = true<GOAL>a = x → p x = true
<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>f✝ g✝ : α → ℝ≥0∞<VAR>f : α → β<VAR>hf : Surjective f<VAR>g : β → ℝ≥0∞<GOAL>∑' (y : β), g y = ∑' (y : β), g (f (surjInv hf y))
<VAR>R✝ : Type u<VAR>I : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>x y z : R✝<VAR>s : I → R✝<VAR>t : Finset I<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : ℕ<VAR>h : a.Coprime b<GOAL>IsCoprime ↑a ↑b
<VAR>R✝ : Type u<VAR>I : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>x y z : R✝<VAR>s : I → R✝<VAR>t : Finset I<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : ℕ<VAR>h : IsCoprime ↑a ↑b<GOAL>IsCoprime ↑a ↑b
<VAR>R✝ : Type u<VAR>I : Type v<VAR>inst✝¹ : CommSemiring R✝<VAR>x y z : R✝<VAR>s : I → R✝<VAR>t : Finset I<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : ℕ<VAR>h : IsCoprime ↑a ↑b<GOAL>IsCoprime ↑↑a ↑↑b
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : Filter α<VAR>t : TopologicalSpace α<GOAL>nhdsAdjoint a f ≤ t ↔ f ≤ (fun t => 𝓝 a) t
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>f : Filter α<VAR>t : TopologicalSpace α<GOAL>nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Nontrivial R<VAR>i j : σ<GOAL>X i ∣ X j ↔ i = j