ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>V : Set (β × β)<VAR>hV : SymmetricRel V<VAR>x y : β<GOAL>x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}
<VAR>ι : Type u_1<VAR>𝕜✝ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>𝕜 : Type u_6<VAR>inst✝ : RCLike 𝕜<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → ℝ<GOAL>∫ (x : ℝ) in a..b, ↑(f x) ∂μ = ↑(∫ (x : ℝ) in a..b, f x ∂μ)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H K : Subgroup G<VAR>hH : f.ker ≤ H<VAR>hK : f.ker ≤ K<VAR>hf : comap f (map f H) = comap f (map f K)<GOAL>H = K
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ i₁' : I₁<VAR>h₁ : ¬c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>(F.map (K₁.d i₁ i₁')).app (K₂.X i₂) = 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<VAR>h₂ : ¬c₂.Rel i₂ i₂'<GOAL>(F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') = 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ i₁' i₁'' : I₁<VAR>i₂ : I₂<GOAL>(F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.map (K₁.d i₁' i₁'')).app (K₂.X i₂) = 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ i₂' i₂'' : I₂<GOAL>(F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (K₁.X i₁)).map (K₂.d i₂' i₂'') = 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ i₁' : I₁<VAR>i₂ i₂' : I₂<GOAL>(F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂')
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ K₂' : HomologicalComplex C₂ c₂<VAR>φ : K₂ ⟶ K₂'<VAR>i₁✝ i₁'✝ : I₁<VAR>i₂✝ : I₂<VAR>a✝ : c₁.Rel i₁✝ i₁'✝<GOAL>(F.obj (K₁.X i₁✝)).map (φ.f i₂✝) ≫ (F.map (K₁.d i₁✝ i₁'✝)).app (K₂'.X i₂✝) = (F.map (K₁.d i₁✝ i₁'✝)).app (K₂.X i₂✝) ≫ (F.obj (K₁.X i₁'✝)).map (φ.f i₂✝)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ K₂' : HomologicalComplex C₂ c₂<VAR>φ : K₂ ⟶ K₂'<VAR>i₁✝ : I₁<VAR>i₂✝ i₂'✝ : I₂<VAR>a✝ : c₂.Rel i₂✝ i₂'✝<GOAL>(F.obj (K₁.X i₁✝)).map (φ.f i₂✝) ≫ (F.obj (K₁.X i₁✝)).map (K₂'.d i₂✝ i₂'✝) = (F.obj (K₁.X i₁✝)).map (K₂.d i₂✝ i₂'✝) ≫ (F.obj (K₁.X i₁✝)).map (φ.f i₂'✝)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i✝¹ : I₁<VAR>i✝ : I₂<GOAL>(F.obj (K₁.X i✝¹)).map (𝟙 (K₂.X i✝)) = 𝟙 ((F.obj (K₁.X i✝¹)).obj (K₂.X i✝))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{?u.836, u_1} C₁<VAR>inst✝⁶ : Category.{?u.840, u_2} C₂<VAR>inst✝⁵ : Category.{?u.844, u_3} D<VAR>inst✝⁴ : HasZeroMorphisms C₁<VAR>inst✝³ : HasZeroMorphisms C₂<VAR>inst✝² : HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>inst✝¹ : F.PreservesZeroMorphisms<VAR>inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>X✝ Y✝ Z✝ : HomologicalComplex C₂ c₂<VAR>f : X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Z✝<VAR>i✝¹ : I₁<VAR>i✝ : I₂<GOAL>(F.obj (K₁.X i✝¹)).map (f.f i✝ ≫ g.f i✝) = (F.obj (K₁.X i✝¹)).map (f.f i✝) ≫ (F.obj (K₁.X i✝¹)).map (g.f i✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>M₀ : Type u_7<VAR>inst✝ : CommMonoidWithZero M₀<VAR>f : α → M₀<VAR>x : α<VAR>hx : f x = 0<VAR>hf : (mulSupport f).Finite<VAR>a✝ : Nontrivial M₀<GOAL>∏ᶠ (x : α), f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>M₀ : Type u_7<VAR>inst✝ : CommMonoidWithZero M₀<VAR>f : α → M₀<VAR>x : α<VAR>hx : f x = 0<VAR>hf : (mulSupport f).Finite<VAR>a✝ : Nontrivial M₀<GOAL>∏ i ∈ hf.toFinset, f i = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>M₀ : Type u_7<VAR>inst✝ : CommMonoidWithZero M₀<VAR>f : α → M₀<VAR>x : α<VAR>hx : f x = 0<VAR>hf : (mulSupport f).Finite<VAR>a✝ : Nontrivial M₀<GOAL>x ∈ mulSupport f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<GOAL>x ∈ p₂.asIdeal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<VAR>h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<VAR>h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal<VAR>h₂ : a ⊗ₜ[R] t ∉ p₂.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<VAR>h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal<VAR>h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<VAR>h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal<VAR>h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal<VAR>h₃ : t ∉ Ideal.comap g p₂.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<VAR>h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal<VAR>h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal<VAR>h₃ : t ∉ Ideal.comap g p₂.asIdeal<VAR>h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₂.asIdeal<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>hRT : (algebraMap R T).SurjectiveOnStalks<VAR>p₁ p₂ : PrimeSpectrum (S ⊗[R] T)<VAR>h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂<VAR>g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom<VAR>x : S ⊗[R] T<VAR>hxp₁ : x ∈ p₁.asIdeal<VAR>hxp₂ : x ∉ p₂.asIdeal<VAR>t : T<VAR>r : R<VAR>a : S<VAR>ht : r • t ∉ Ideal.comap g p₂.asIdeal<VAR>e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t<VAR>h₁ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ p₁.asIdeal<VAR>h₂ : a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ p₂.asIdeal<VAR>h₃ : t ∉ Ideal.comap g p₁.asIdeal<VAR>h₄ : a ∉ Ideal.comap (algebraMap S (S ⊗[R] T)) p₁.asIdeal<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>f : OneHom M N<VAR>g : N → M<VAR>h₁ : LeftInverse g ⇑f<GOAL>g 1 = 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>f : P →ᵃ[R] P'<GOAL>Wbtw R (f x) (f y) (f z)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>f : P →ᵃ[R] P'<GOAL>f y ∈ ⇑f '' affineSegment R x z
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>H ≠ ⊥ ↔ ∃ a, a ≠ 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>(∃ x ∈ H, x ≠ 1) ↔ ∃ a, a ≠ 1
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>{x * y, x, y, 1} = univ
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>{x * y, x, y, 1}.card = Fintype.card G
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>{x * y, x, y, 1}.card = 4
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>{1}.card + 1 + 1 + 1 = 4
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>y ∉ {1}
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>x ∉ {y, 1}
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>inst✝² : IsKleinFour G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>x y : G<VAR>hx : x ≠ 1<VAR>hy : y ≠ 1<VAR>hxy : x ≠ y<GOAL>x * y ∉ {x, y, 1}
<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>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>h : DifferentiableAt 𝕜 (fun y => f y + c) x<GOAL>DifferentiableAt 𝕜 f x
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w u' : V<VAR>p : G.Walk u' u'<GOAL>(p.copy ⋯ ⋯).IsCircuit ↔ p.IsCircuit
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>h : ∀ t ∈ s, IsIntegralCurveAt γ v t<VAR>t : ℝ<VAR>ht : t ∈ s<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s✝ s' : Set ℝ<VAR>t₀ : ℝ<VAR>h✝ : ∀ t ∈ s✝, IsIntegralCurveAt γ v t<VAR>t : ℝ<VAR>ht : t ∈ s✝<VAR>s : Set ℝ<VAR>hs : s ∈ 𝓝 t<VAR>h : IsIntegralCurveOn γ v s<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖₊ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<GOAL>∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>μ : Measure β<VAR>inst✝ : SeparableSpace ↑(Set.range f ∪ {0})<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<GOAL>HasFiniteIntegral (fun x => f x - 0) μ
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<GOAL>ofHom 0 = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>μ.withDensity (f * fun x => (f x)⁻¹) = μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<GOAL>(f * fun x => (f x)⁻¹) =ᶠ[ae μ] 1
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>x : α<VAR>hf_ne_zero : f x ≠ 0<VAR>hf_ne_top : f x ≠ ⊤<GOAL>(f * fun x => (f x)⁻¹) x = 1 x
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0<VAR>hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>x : α<VAR>hf_ne_zero : f x ≠ 0<VAR>hf_ne_top : f x ≠ ⊤<GOAL>f x * (f x)⁻¹ = 1 x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>S : Set (Set α)<VAR>hc : S.Countable<GOAL>μ.restrict (⋃₀ S) = ν.restrict (⋃₀ S) ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp a (p + b) = toIcoDiv hp a b + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b : β<VAR>q✝ : ℚ<VAR>x✝ : ∃ q, b < ↑q ∧ ↑q < a<VAR>q : ℚ<VAR>hbq : b < ↑q<VAR>hqa : ↑q < a<GOAL>↑q < inducedMap α β a
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n < firstDiff x y<GOAL>x n = y n
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>n : ℕ<VAR>hn : n < if h : x ≠ y then Nat.find ⋯ else 0<GOAL>x n = y n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hs : s.Subsingleton<GOAL>∃ a, l = pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>a : α<VAR>hsl : {a} ∈ l<VAR>hs : {a}.Subsingleton<GOAL>∃ a, l = pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>a : α<VAR>hsl : {a} ∈ l<VAR>hs : {a}.Subsingleton<GOAL>l ≤ pure a
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : P1 →ᵃ[k] P2<VAR>p1 p2 : P1<GOAL>f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2