ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>r : R<VAR>x : ↑X<VAR>this✝ : Module R S := Module.compHom S f<VAR>this : Module R ↑Y := Module.compHom (↑Y) f<GOAL>g ((algebraMap R R) r • 1 ⊗ₜ[R] (RestrictScalars.addEquiv R R ↑X) x) = g (f r • 1 ⊗ₜ[R] x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : AddCommMonoid M<VAR>f : α → α<VAR>g : α → M<VAR>m n : ℕ<VAR>x : α<GOAL>birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>m : M<GOAL>torsionOf R M m = ⊥ ↔ m ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>m : M<VAR>h : torsionOf R M m = ⊥<VAR>contra : m = 0<GOAL>False
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>m : M<VAR>h : m ≠ 0<VAR>r : R<VAR>hr : r ∈ torsionOf R M m<GOAL>r = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>t : Set β<VAR>ht : (Measure.map f ν) t = 0<GOAL>(Measure.map f μ) t = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ ν : Measure α<VAR>hf : MeasurableEmbedding f<VAR>hμν : μ ≪ ν<VAR>t : Set β<VAR>ht : ν (f ⁻¹' t) = 0<GOAL>μ (f ⁻¹' t) = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Surjective f<VAR>s : Set Y<VAR>hs : MeasurableSet s<GOAL>(Measure.map f μH[d]) s = (μH[d].restrict (range f)) s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<VAR>H : x = y<GOAL>hammingDist y y = 0
<VAR>𝕜 : Type v<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>↑(closedBall 0 1) ≃ₜ ↑(closedBall y r)
<VAR>𝕜 : Type v<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>closedBall 0 1 = ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r
<VAR>𝕜 : Type v<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : E<GOAL>x ∈ closedBall 0 1 ↔ x ∈ ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r
<VAR>𝕜 : Type v<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : E<GOAL>‖x‖ ≤ 1 ↔ r * ‖x‖ ≤ r
<VAR>m n : ℕ<VAR>u : ℕˣ<GOAL>↑u = 1
<VAR>m n : ℕ<GOAL>↑1 = 1
<VAR>α β : Type u<VAR>a : Cardinal.{u}<GOAL>lift.{v, u} a ≤ 1 ↔ a ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>inst✝ : Std.IdempotentOp gb<VAR>h : Semiconj₂ f ga gb<VAR>h_inj : Injective f<VAR>x : α<GOAL>f (ga x x) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice β<VAR>t : ι → Set β<GOAL>sSup (⋃ i, t i) = ⨆ i, sSup (t i)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : o<GOAL>(M * 0) i✝ j✝ = 0 i✝ j✝
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<GOAL>∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<GOAL>∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<GOAL>∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<VAR>x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S<GOAL>∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<VAR>x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S<VAR>this : Algebra.IsIntegral Rₚ Sₚ<GOAL>∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<VAR>x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S<VAR>this : Algebra.IsIntegral Rₚ Sₚ<VAR>Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal<GOAL>∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<VAR>x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S<VAR>this : Algebra.IsIntegral Rₚ Sₚ<VAR>Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal<GOAL>comap (algebraMap R S) (comap (algebraMap S Sₚ) Qₚ) = P
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<VAR>x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S<VAR>this : Algebra.IsIntegral Rₚ Sₚ<VAR>Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal<GOAL>comap (algebraMap R S) (comap (algebraMap S Sₚ) Qₚ) = comap (algebraMap R (Localization.AtPrime P)) (LocalRing.maximalIdeal (Localization P.primeCompl))
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>inst✝ : P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<VAR>hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl<VAR>Rₚ : Type u_1 := Localization P.primeCompl<VAR>Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)<VAR>this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) := IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)<VAR>Qₚ : Ideal Sₚ<VAR>Qₚ_maximal : Qₚ.IsMaximal<VAR>x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S<VAR>this : Algebra.IsIntegral Rₚ Sₚ<VAR>Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal<GOAL>comap ((IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)) Qₚ = comap (algebraMap R (Localization.AtPrime P)) (comap (algebraMap Rₚ Sₚ) Qₚ)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫ Y₁ ◁ (α_ Y₂ V₁ V₂).inv ≫ Y₁ ◁ (β_ Y₂ V₁).hom ▷ V₂ ≫ Y₁ ◁ (α_ V₁ Y₂ V₂).hom ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ X₁ ◁ (α_ X₂ U₁ U₂).inv ≫ X₁ ◁ (β_ X₂ U₁).hom ▷ U₂ ≫ X₁ ◁ (α_ U₁ X₂ U₂).hom ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>((f₁ ⊗ f₂) ⊗ g₁ ⊗ g₂) ≫ (α_ Y₁ Y₂ (V₁ ⊗ V₂)).hom ≫ (𝟙 Y₁ ⊗ (α_ Y₂ V₁ V₂).inv) ≫ (𝟙 Y₁ ⊗ (β_ Y₂ V₁).hom ⊗ 𝟙 V₂) ≫ (𝟙 Y₁ ⊗ (α_ V₁ Y₂ V₂).hom) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>(((((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (f₁ ⊗ f₂ ⊗ g₁ ⊗ g₂)) ≫ (𝟙 Y₁ ⊗ (α_ Y₂ V₁ V₂).inv)) ≫ (𝟙 Y₁ ⊗ (β_ Y₂ V₁).hom ⊗ 𝟙 V₂)) ≫ (𝟙 Y₁ ⊗ (α_ V₁ Y₂ V₂).hom)) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>(α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ ((((𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (f₁ ⊗ (f₂ ⊗ g₁) ⊗ g₂)) ≫ (𝟙 Y₁ ⊗ (β_ Y₂ V₁).hom ⊗ 𝟙 V₂)) ≫ (𝟙 Y₁ ⊗ (α_ V₁ Y₂ V₂).hom)) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>(α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (((𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (f₁ ⊗ (g₁ ⊗ f₂) ⊗ g₂)) ≫ (𝟙 Y₁ ⊗ (α_ V₁ Y₂ V₂).hom)) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>(α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ ((𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (f₁ ⊗ g₁ ⊗ f₂ ⊗ g₂)) ≫ (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<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₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : U₁ ⟶ V₁<VAR>g₂ : U₂ ⟶ V₂<GOAL>(α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂) = ((α_ X₁ X₂ (U₁ ⊗ U₂)).hom ≫ (𝟙 X₁ ⊗ (α_ X₂ U₁ U₂).inv) ≫ (𝟙 X₁ ⊗ (β_ X₂ U₁).hom ⊗ 𝟙 U₂) ≫ (𝟙 X₁ ⊗ (α_ U₁ X₂ U₂).hom) ≫ (α_ X₁ U₁ (X₂ ⊗ U₂)).inv) ≫ ((f₁ ⊗ g₁) ⊗ f₂ ⊗ g₂)
<VAR>α : Type u_1<VAR>l l' : List α<GOAL>l <+ l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
<VAR>α : Type u_1<VAR>l l' : List α<GOAL>(∃ f, ∀ (ix : ℕ), l.get? ix = l'.get? (f ix)) ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
<VAR>α : Type u<VAR>a : α<VAR>s✝ t s : Set α<GOAL>s.Subsingleton ∨ s.Nontrivial
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.IsCommutative<VAR>inst✝¹ : H.FiniteIndex<VAR>α✝¹ β✝¹ : ↑(leftTransversals ↑H)<VAR>inst✝ : H.Normal<VAR>hH : (Nat.card ↥H).Coprime H.index<VAR>α✝ β✝ : H.QuotientDiff<VAR>β α : ↑(leftTransversals ↑H)<GOAL>diff (MonoidHom.id ↥H) β α * ((powCoprime hH).symm (diff (MonoidHom.id ↥H) β α))⁻¹ ^ H.index = 1
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{?u.55275, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Epi S.g<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<GOAL>opcyclesMap S.f i ≫ opcyclesMap S.g i = 0
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Epi S.g<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<VAR>this : Epi (S.map (eval C c i)).g<GOAL>(ShortComplex.mk (opcyclesMap S.f i) (opcyclesMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Epi S.g<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<VAR>this : Epi (S.map (eval C c i)).g<VAR>hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)<GOAL>(ShortComplex.mk (opcyclesMap S.f i) (opcyclesMap S.g i) ⋯).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Abelian C<VAR>c : ComplexShape ι<VAR>S : ShortComplex (HomologicalComplex C c)<VAR>hS : S.Exact<VAR>inst✝³ : Epi S.g<VAR>i : ι<VAR>inst✝² : S.X₁.HasHomology i<VAR>inst✝¹ : S.X₂.HasHomology i<VAR>inst✝ : S.X₃.HasHomology i<VAR>this : Epi (S.map (eval C c i)).g<VAR>hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)<GOAL>IsColimit (CokernelCofork.ofπ (ShortComplex.mk (opcyclesMap S.f i) (opcyclesMap S.g i) ⋯).g ⋯)
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<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>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>s : Set E<VAR>x : E<VAR>hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)<VAR>hs : Convex ℝ s<VAR>K : ℝ≥0<VAR>hK : ‖p x 1‖₊ < K<VAR>f' : E → E →L[ℝ] F := fun y => (continuousMultilinearCurryFin1 ℝ E F) (p y 1)<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<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>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>s : Set E<VAR>x : E<VAR>hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)<VAR>hs : Convex ℝ s<VAR>K : ℝ≥0<VAR>hK : ‖p x 1‖₊ < K<VAR>f' : E → E →L[ℝ] F := fun y => (continuousMultilinearCurryFin1 ℝ E F) (p y 1)<VAR>hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<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>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>s : Set E<VAR>x : E<VAR>hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)<VAR>hs : Convex ℝ s<VAR>K : ℝ≥0<VAR>hK : ‖p x 1‖₊ < K<VAR>f' : E → E →L[ℝ] F := fun y => (continuousMultilinearCurryFin1 ℝ E F) (p y 1)<VAR>hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<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>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>s : Set E<VAR>x : E<VAR>hf : HasFTaylorSeriesUpToOn 1 f p (insert x s)<VAR>hs : Convex ℝ s<VAR>K : ℝ≥0<VAR>f' : E → E →L[ℝ] F := fun y => (continuousMultilinearCurryFin1 ℝ E F) (p y 1)<VAR>hder : ∀ y ∈ s, HasFDerivWithinAt f (f' y) s y<VAR>hcont : ContinuousWithinAt f' s x<VAR>hK : ‖f' x‖₊ < K<GOAL>∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ<VAR>inst✝¹ : NeZero n<VAR>inst✝ : Fintype (ZMod n)ˣ<GOAL>Fintype.card { x // x.val.Coprime n } = φ n
<VAR>m : ℕ<VAR>inst✝¹ : NeZero (m + 1)<VAR>inst✝ : Fintype (ZMod (m + 1))ˣ<GOAL>Fintype.card { x // x.val.Coprime (m + 1) } = φ (m + 1)
<VAR>m : ℕ<VAR>inst✝¹ : NeZero (m + 1)<VAR>inst✝ : Fintype (ZMod (m + 1))ˣ<GOAL>(∑ a : ZMod (m + 1), if a.val.Coprime (m + 1) then 1 else 0) = ∑ i : Fin (m + 1), if (↑i).Coprime (m + 1) then 1 else 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>inst✝ : Fintype ι<VAR>f : α → ι → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f✝ : α → β<VAR>inst✝ : Fintype ι<VAR>f : α → ι → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<VAR>this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s<GOAL>∃ g, LipschitzWith K g ∧ EqOn f g s
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M<GOAL>x ∈ map (fst R M M₂) (p.prod q) ↔ x ∈ p
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime}