ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g✝ : S →+* T<VAR>f : R →+* S<VAR>hf : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>J : Ideal (S ⊗[R] T)<VAR>hJ : J.IsPrime<VAR>x : S ⊗[R] T<GOAL>∃ x_1 r, ∃ c ∉ J, (algebraMap S (S ⊗[R] T)) r ∉ J ∧ c * (algebraMap S (S ⊗[R] T)) r * x = c * (algebraMap S (S ⊗[R] T)) x_1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g✝ : S →+* T<VAR>f : R →+* S<VAR>hf : (algebraMap R T).SurjectiveOnStalks<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>J : Ideal (S ⊗[R] T)<VAR>hJ : J.IsPrime<VAR>x : S ⊗[R] T<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g J<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<GOAL>∃ x_1 r, ∃ c ∉ J, (algebraMap S (S ⊗[R] T)) r ∉ J ∧ c * (algebraMap S (S ⊗[R] T)) r * x = c * (algebraMap S (S ⊗[R] T)) x_1
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<GOAL>IsOpen (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>yfs : y ∈ ⇑f '' s<GOAL>∃ ε > 0, ball y ε ⊆ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<GOAL>∃ ε > 0, ball y ε ⊆ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ball x ε ⊆ s<GOAL>∃ ε > 0, ball y ε ⊆ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ball x ε ⊆ s<VAR>z : F<VAR>hz : z ∈ ball y (ε / C)<GOAL>z ∈ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ball x ε ⊆ s<VAR>z : F<VAR>hz : z ∈ ball y (ε / C)<VAR>w : E<VAR>wim : f w = z - y<VAR>wnorm : ‖w‖ ≤ C * ‖z - y‖<GOAL>z ∈ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ball x ε ⊆ s<VAR>z : F<VAR>hz : z ∈ ball y (ε / C)<VAR>w : E<VAR>wim : f w = z - y<VAR>wnorm : ‖w‖ ≤ C * ‖z - y‖<VAR>this : f (x + w) = z<GOAL>z ∈ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ball x ε ⊆ s<VAR>z : F<VAR>hz : z ∈ ball y (ε / C)<VAR>w : E<VAR>wim : f w = z - y<VAR>wnorm : ‖w‖ ≤ C * ‖z - y‖<VAR>this : f (x + w) = z<GOAL>f (x + w) ∈ ⇑f '' s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>s : Set E<VAR>hs : IsOpen s<VAR>C : ℝ<VAR>Cpos : C > 0<VAR>hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖<VAR>y : F<VAR>x : E<VAR>xs : x ∈ s<VAR>fxy : f x = y<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>hε : ball x ε ⊆ s<VAR>z : F<VAR>hz : z ∈ ball y (ε / C)<VAR>w : E<VAR>wim : f w = z - y<VAR>wnorm : ‖w‖ ≤ C * ‖z - y‖<VAR>this✝ : f (x + w) = z<VAR>this : x + w ∈ ball x ε<GOAL>f (x + w) ∈ ⇑f '' s
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Finite ι<VAR>inst✝ : HasSolidNorm K<GOAL>IsBounded (fundamentalDomain b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Finite ι<VAR>inst✝ : HasSolidNorm K<VAR>val✝ : Fintype ι<GOAL>IsBounded (fundamentalDomain b)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Finite ι<VAR>inst✝ : HasSolidNorm K<VAR>val✝ : Fintype ι<VAR>x : E<VAR>hx : x ∈ fundamentalDomain b<GOAL>‖x‖ ≤ ∑ j : ι, ‖b j‖
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : NormedLinearOrderedField K<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝² : FloorRing K<VAR>inst✝¹ : Finite ι<VAR>inst✝ : HasSolidNorm K<VAR>val✝ : Fintype ι<VAR>x : E<VAR>hx : x ∈ fundamentalDomain b<GOAL>‖fract b x‖ ≤ ∑ j : ι, ‖b j‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f✝ : α →. β<VAR>g : β → γ<VAR>f : α → β<VAR>x✝¹ : α<VAR>x✝ : γ<GOAL>x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ (↑g).comp (↑f) x✝¹
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ toArray l ↔ a ∈ l
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<GOAL>(α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv = (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X Y Z : C<GOAL>((α_ W X (Y ⊗ Z)).inv ≫ (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv) ≫ (α_ W X Y).inv ▷ Z = ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) ≫ (α_ W X Y).inv ▷ Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>s✝ : Set α<VAR>s : Set β<VAR>f : α → β<VAR>hf : Surjective f<VAR>x : α<VAR>hx : f x ∈ s<VAR>y : α<VAR>hy : f y ∈ s<VAR>hxy : f x ≠ f y<GOAL>(f ⁻¹' s).Nontrivial
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>inst✝ : ProperSpace E<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>a b : E<GOAL>Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x✝ y : M<VAR>u : Rˣ<VAR>x : M<GOAL>-u • x = -(u • x)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.76625, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>p : ℤ<GOAL>((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) p).hom ≫ ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj S.X₂).d p (p + 1) = (mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫ ((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) (p + 1)).hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.76625, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>p : ℤ<VAR>r_f : (σ (p + 1 + 1)).r ≫ (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).f = 𝟙 (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).X₂ - (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).g ≫ (σ (p + 1 + 1)).s<GOAL>((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) p).hom ≫ ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj S.X₂).d p (p + 1) = (mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫ ((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) (p + 1)).hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.76625, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>p : ℤ<VAR>r_f : (σ (p + 1 + 1)).r ≫ (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).f = 𝟙 (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).X₂ - (S.map (eval C (ComplexShape.up ℤ) (p + 1 + 1))).g ≫ (σ (p + 1 + 1)).s<VAR>s_g : (σ (p + 1)).s ≫ (S.map (eval C (ComplexShape.up ℤ) (p + 1))).g = 𝟙 (S.map (eval C (ComplexShape.up ℤ) (p + 1))).X₃<GOAL>((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) p).hom ≫ ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj S.X₂).d p (p + 1) = (mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫ ((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) (p + 1)).hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.76625, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>inst✝ : HasBinaryBiproducts C<VAR>p : ℤ<VAR>r_f : (σ (p + 1 + 1)).r ≫ S.f.f (p + 1 + 1) = 𝟙 (S.X₂.X (p + 1 + 1)) - S.g.f (p + 1 + 1) ≫ (σ (p + 1 + 1)).s<VAR>s_g : (σ (p + 1)).s ≫ S.g.f (p + 1) = 𝟙 (S.X₃.X (p + 1))<GOAL>((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) p).hom ≫ ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj S.X₂).d p (p + 1) = (mappingCone (homOfDegreewiseSplit S σ)).d p (p + 1) ≫ ((fun p => mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) (p + 1)).hom
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : 1 < A.card * B.card<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<VAR>a : G<VAR>ha : a ∈ A<VAR>b : G<VAR>hb : b ∈ B<VAR>hu : UniqueMul A B a b<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<VAR>a : G<VAR>ha : a ∈ A<VAR>b : G<VAR>hb : b ∈ B<VAR>hu : UniqueMul A B a b<VAR>C : Finset G := map { toFun := fun x => a⁻¹ * x, inj' := ⋯ } A<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<VAR>a : G<VAR>ha : a ∈ A<VAR>b : G<VAR>hb : b ∈ B<VAR>hu : UniqueMul A B a b<VAR>C : Finset G := map { toFun := fun x => a⁻¹ * x, inj' := ⋯ } A<VAR>D : Finset G := map { toFun := fun x => x * b⁻¹, inj' := ⋯ } B<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<VAR>a : G<VAR>ha : a ∈ A<VAR>b : G<VAR>hb : b ∈ B<VAR>hu : UniqueMul A B a b<VAR>C : Finset G := map { toFun := fun x => a⁻¹ * x, inj' := ⋯ } A<VAR>D : Finset G := map { toFun := fun x => x * b⁻¹, inj' := ⋯ } B<VAR>hcard : 1 < C.card ∨ 1 < D.card<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<VAR>a : G<VAR>ha : a ∈ A<VAR>b : G<VAR>hb : b ∈ B<VAR>hu : UniqueMul A B a b<VAR>C : Finset G := map { toFun := fun x => a⁻¹ * x, inj' := ⋯ } A<VAR>D : Finset G := map { toFun := fun x => x * b⁻¹, inj' := ⋯ } B<VAR>hcard : 1 < C.card ∨ 1 < D.card<VAR>hC : 1 ∈ C<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>G✝ : Type u<VAR>H : Type v<VAR>inst✝³ : Mul G✝<VAR>inst✝² : Mul H<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : UniqueProds G<VAR>A B : Finset G<VAR>hc : A.Nonempty ∧ B.Nonempty ∧ (1 < A.card ∨ 1 < B.card)<VAR>a : G<VAR>ha : a ∈ A<VAR>b : G<VAR>hb : b ∈ B<VAR>hu : UniqueMul A B a b<VAR>C : Finset G := map { toFun := fun x => a⁻¹ * x, inj' := ⋯ } A<VAR>D : Finset G := map { toFun := fun x => x * b⁻¹, inj' := ⋯ } B<VAR>hcard : 1 < C.card ∨ 1 < D.card<VAR>hC : 1 ∈ C<VAR>hD : 1 ∈ D<GOAL>∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : A<VAR>p : R[X]<VAR>h : Function.Injective ⇑(algebraMap A B)<GOAL>(aeval ((algebraMap A B) x)) p = 0 ↔ (aeval x) p = 0
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<GOAL>1 - ε ^ 5 / 50 ≤ (↑m / (↑m + 1)) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)<GOAL>1 - ε ^ 5 / 50 ≤ (↑m / (↑m + 1)) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)<GOAL>1 - ε ^ 5 / 50 ≤ 1 - 2 * (1 / (↑m + 1)) + (1 / (↑m + 1)) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)<GOAL>1 - ε ^ 5 / 50 ≤ 1 - 2 * (1 / (↑m + 1))
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)<GOAL>50 * 2 / ε ^ 5 ≤ ↑m + 1
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)<GOAL>0 < ε ^ 5 / (50 * 2)
<VAR>a : ℝ<GOAL>frontier {z | z.re < a} = {z | z.re = a}
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<VAR>h : I ≤ J<GOAL>(π.restrict J).boxes = π.boxes
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<VAR>h : I ≤ J<GOAL>(Finset.image (fun J' => ↑J ⊓ ↑J') π.boxes).biUnion Option.toFinset = π.boxes
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<VAR>h : I ≤ J<GOAL>(π.boxes.biUnion fun a => Option.toFinset (↑J ⊓ ↑a)) = π.boxes
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<VAR>h : I ≤ J<GOAL>∀ a ∈ π.boxes, Option.toFinset (↑J ⊓ ↑a) = {a}
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<VAR>h : I ≤ J<VAR>J' : Box ι<VAR>hJ' : J' ∈ π.boxes<GOAL>Option.toFinset (↑J ⊓ ↑J') = {J'}
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<VAR>h : I ≤ J<VAR>J' : Box ι<VAR>hJ' : J' ∈ π.boxes<GOAL>↑J' ≤ ↑J
<VAR>n : Nat<GOAL>range (n + 1) = 0 :: map succ (range n)
<VAR>n : Nat<GOAL>0 :: map (fun x => 1 + x) (range' 0 n) = 0 :: map succ (range' 0 n)
<VAR>n : Nat<GOAL>(fun x => 1 + x) = succ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.133956, u_1} C<VAR>inst✝³ : Category.{?u.133960, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain F K m<VAR>β : Cocycle G K n<VAR>h : m + 1 = n<VAR>eq : δ m n α = n.negOnePow • (Cochain.ofHom φ).comp ↑β ⋯<GOAL>δ n (n + 1) (descCochain φ α (↑β) h) = 0