ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>f g₁ g₂ : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R g₁ g₂ U hu₂ * AlgebraicGeometry.StructureSheaf.const R f g₁ U hu₁ = AlgebraicGeometry.StructureSheaf.const R f g₂ U hu₂
<VAR>R : Type u<VAR>CommRing R<VAR>U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>i : V ⟶ U<GOAL>AlgebraicGeometry.StructureSheaf.toOpen R U ≫ (AlgebraicGeometry.Spec.structureSheaf R).val.map i.op = AlgebraicGeometry.StructureSheaf.toOpen R V
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : R<VAR>x : ↥U<GOAL>↑((AlgebraicGeometry.StructureSheaf.toOpen R U) f) x = (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ↑x)) f
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : R<GOAL>(AlgebraicGeometry.StructureSheaf.toOpen R U) f = AlgebraicGeometry.StructureSheaf.const R f 1 U ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↥U<GOAL>AlgebraicGeometry.StructureSheaf.toOpen R U ≫ (AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ x = AlgebraicGeometry.StructureSheaf.toStalk R ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↥U<VAR>f : R<GOAL>((AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ x) ((AlgebraicGeometry.StructureSheaf.toOpen R U) f) = (AlgebraicGeometry.StructureSheaf.toStalk R ↑x) f
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : R<GOAL>((AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ ⟨x, trivial⟩) ((AlgebraicGeometry.StructureSheaf.toOpen R ⊤) f) = (AlgebraicGeometry.StructureSheaf.toStalk R x) f
<VAR>R : Type u<VAR>CommRing R<VAR>f : R<GOAL>IsUnit ((AlgebraicGeometry.StructureSheaf.toOpen R (PrimeSpectrum.basicOpen f)) f)
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : ↥x.asIdeal.primeCompl<GOAL>IsUnit ((AlgebraicGeometry.StructureSheaf.toStalk R x) ↑f)
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : R<GOAL>(AlgebraicGeometry.StructureSheaf.localizationToStalk R x) ((algebraMap R (Localization x.asIdeal.primeCompl)) f) = (AlgebraicGeometry.StructureSheaf.toStalk R x) f
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : R<VAR>s : ↥x.asIdeal.primeCompl<GOAL>(AlgebraicGeometry.StructureSheaf.localizationToStalk R x) (IsLocalization.mk' (Localization.AtPrime x.asIdeal) f s) = ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ ⟨x, ⋯⟩) (AlgebraicGeometry.StructureSheaf.const R f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hx : x ∈ U<GOAL>⇑(AlgebraicGeometry.StructureSheaf.openToLocalization R U x hx) = fun s => ↑s ⟨x, hx⟩
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hx : x ∈ U<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.StructureSheaf.openToLocalization R U x hx) s = ↑s ⟨x, hx⟩
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↥U<GOAL>(AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ x ≫ AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R ↑x = AlgebraicGeometry.StructureSheaf.openToLocalization R U ↑x ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hx : x ∈ U<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x) (((AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ ⟨x, hx⟩) s) = ↑s ⟨x, hx⟩
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>x : ↥U<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R ↑x) (((AlgebraicGeometry.Spec.structureSheaf R).presheaf.germ x) s) = ↑s x
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>AlgebraicGeometry.StructureSheaf.toStalk R x ≫ AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x = algebraMap R (Localization.AtPrime x.asIdeal)
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : R<GOAL>(AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x) ((AlgebraicGeometry.StructureSheaf.toStalk R x) f) = (algebraMap R (Localization.AtPrime x.asIdeal)) f
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>(AlgebraicGeometry.StructureSheaf.stalkIso R x).hom = AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>(AlgebraicGeometry.StructureSheaf.stalkIso R x).inv = AlgebraicGeometry.StructureSheaf.localizationToStalk R x
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x ≫ AlgebraicGeometry.StructureSheaf.localizationToStalk R x = 𝟙 ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk x)
<VAR>R : Type u<VAR>CommRing R<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>AlgebraicGeometry.StructureSheaf.localizationToStalk R x ≫ AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x = 𝟙 (CommRingCat.of (Localization.AtPrime x.asIdeal))
<VAR>R : Type u<VAR>CommRing R<VAR>s f : R<VAR>g : ↥(Submonoid.powers s)<GOAL>(AlgebraicGeometry.StructureSheaf.toBasicOpen R s) (IsLocalization.mk' (Localization.Away s) f g) = AlgebraicGeometry.StructureSheaf.const R f (↑g) (PrimeSpectrum.basicOpen s) ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>f : R<GOAL>(AlgebraicGeometry.StructureSheaf.toBasicOpen R f).comp (algebraMap R (Localization.Away f)) = AlgebraicGeometry.StructureSheaf.toOpen R (PrimeSpectrum.basicOpen f)
<VAR>R : Type u<VAR>CommRing R<VAR>s f : R<GOAL>(AlgebraicGeometry.StructureSheaf.toBasicOpen R s) ((algebraMap R (Localization.Away s)) f) = AlgebraicGeometry.StructureSheaf.const R f 1 (PrimeSpectrum.basicOpen s) ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>f : R<GOAL>Function.Injective ⇑(AlgebraicGeometry.StructureSheaf.toBasicOpen R f)
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<VAR>x : ↥U<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ AlgebraicGeometry.StructureSheaf.const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((AlgebraicGeometry.Spec.structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>a h : ι → R<VAR>iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U<VAR>h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)<VAR>hs : ∀ (i : ι), AlgebraicGeometry.StructureSheaf.const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ = ((AlgebraicGeometry.Spec.structureSheaf R).val.map (iDh i).op) s<GOAL>∃ a' h' iDh', U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧ (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧ ∀ i ∈ t, ((AlgebraicGeometry.Spec.structureSheaf R).val.map (iDh' i).op) s = AlgebraicGeometry.StructureSheaf.const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>f : R<GOAL>Function.Surjective ⇑(AlgebraicGeometry.StructureSheaf.toBasicOpen R f)
<VAR>R : Type u<VAR>CommRing R<VAR>p : PrimeSpectrum R<VAR>r : R<GOAL>(algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk p)) r = (AlgebraicGeometry.StructureSheaf.toStalk R p) r
<VAR>R : Type u<VAR>CommRing R<VAR>U : (TopologicalSpace.Opens (PrimeSpectrum R))ᵒᵖ<VAR>r : R<GOAL>(algebraMap R ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)) r = (AlgebraicGeometry.StructureSheaf.toOpen R (Opposite.unop U)) r
<VAR>R : Type u<VAR>CommRing R<GOAL>AlgebraicGeometry.StructureSheaf.toOpen R ⊤ = CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ AlgebraicGeometry.StructureSheaf.toBasicOpen R 1 ≫ (AlgebraicGeometry.Spec.structureSheaf R).val.map (CategoryTheory.eqToHom ⋯).op
<VAR>R : Type u<VAR>CommRing R<GOAL>(AlgebraicGeometry.StructureSheaf.globalSectionsIso R).inv = CategoryTheory.inv (AlgebraicGeometry.StructureSheaf.toOpen R ⊤)
<VAR>R : Type u<VAR>CommRing R<VAR>f : ↑(CommRingCat.of R)<VAR>x : ↥(Opposite.unop (Opposite.op ⊤))<GOAL>↑((AlgebraicGeometry.StructureSheaf.globalSectionsIso R).hom f) x = (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ↑x)) f
<VAR>R : CommRingCat<GOAL>(AlgebraicGeometry.StructureSheaf.globalSectionsIso ↑R).hom = AlgebraicGeometry.StructureSheaf.toOpen ↑R ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>AlgebraicGeometry.StructureSheaf.toStalk R y ≫ (AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h = AlgebraicGeometry.StructureSheaf.toStalk R x
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>AlgebraicGeometry.StructureSheaf.localizationToStalk R y ≫ (AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h = CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ AlgebraicGeometry.StructureSheaf.localizationToStalk R x
<VAR>R : Type u_1<VAR>CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>(AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h ≫ AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R x = AlgebraicGeometry.StructureSheaf.stalkToFiberRingHom R y ≫ let_fun this := PrimeSpectrum.localizationMapOfSpecializes h; this
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<VAR>CommRing S<VAR>f : R →+* S<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>s : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations R ↑x<VAR>hs : (AlgebraicGeometry.StructureSheaf.isLocallyFraction R).pred s<GOAL>(AlgebraicGeometry.StructureSheaf.isLocallyFraction S).pred (AlgebraicGeometry.StructureSheaf.comapFun f U V hUV s)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<VAR>CommRing S<VAR>f : R →+* S<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<VAR>p : ↥V<GOAL>↑((AlgebraicGeometry.StructureSheaf.comap f U V hUV) s) p = (Localization.localRingHom ((PrimeSpectrum.comap f) ↑p).asIdeal (↑p).asIdeal f ⋯) (↑s ⟨(PrimeSpectrum.comap f) ↑p, ⋯⟩)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<VAR>CommRing S<VAR>f : R →+* S<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)<VAR>hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier<VAR>a b : R<VAR>hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl<GOAL>(AlgebraicGeometry.StructureSheaf.comap f U V hUV) (AlgebraicGeometry.StructureSheaf.const R a b U hb) = AlgebraicGeometry.StructureSheaf.const S (f a) (f b) V ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>iVU : V ⟶ U<GOAL>AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ = (AlgebraicGeometry.Spec.structureSheaf R).val.map iVU.op
<VAR>R : Type u<VAR>CommRing R<VAR>U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hUV : U = V<GOAL>AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U V ⋯ = CategoryTheory.eqToHom ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>AlgebraicGeometry.StructureSheaf.comap (RingHom.id R) U U ⋯ = RingHom.id ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<VAR>CommRing S<VAR>P : Type u<VAR>CommRing P<VAR>f : R →+* S<VAR>g : S →+* P<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)<VAR>W : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top P)<VAR>hUV : ∀ p ∈ V, (PrimeSpectrum.comap f) p ∈ U<VAR>hVW : ∀ p ∈ W, (PrimeSpectrum.comap g) p ∈ V<GOAL>AlgebraicGeometry.StructureSheaf.comap (g.comp f) U W ⋯ = (AlgebraicGeometry.StructureSheaf.comap g V W hVW).comp (AlgebraicGeometry.StructureSheaf.comap f U V hUV)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<VAR>CommRing S<VAR>f : R →+* S<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>AlgebraicGeometry.StructureSheaf.toOpen R U ≫ AlgebraicGeometry.StructureSheaf.comap f U ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) U) ⋯ = CommRingCat.ofHom f ≫ AlgebraicGeometry.StructureSheaf.toOpen S ((TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) U)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<VAR>CommRing S<VAR>f : R →+* S<VAR>x : R<GOAL>AlgebraicGeometry.StructureSheaf.comap f (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen (f x)) ⋯ = IsLocalization.map (↑((AlgebraicGeometry.Spec.structureSheaf S).val.obj (Opposite.op (PrimeSpectrum.basicOpen (f x))))) f ⋯
<VAR>α : Type u_2<VAR>Zero α<GOAL>Set.Finite 0
<VAR>α : Type u_2<VAR>One α<GOAL>Set.Finite 1
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s⁻¹.Finite
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(-s).Finite
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>s.Finite → t.Finite → (s + t).Finite
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>s.Finite → t.Finite → (s * t).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>s.Finite → t.Finite → (s +ᵥ t).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>s.Finite → t.Finite → (s • t).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set β<VAR>a : α<GOAL>s.Finite → (a • s).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set β<VAR>a : α<GOAL>s.Finite → (a +ᵥ s).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set β<VAR>a : α<GOAL>(a +ᵥ s).Infinite → s.Infinite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set β<VAR>a : α<GOAL>(a • s).Infinite → s.Infinite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(s -ᵥ t).Finite
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>IsRightCancelMul α<VAR>s t : Set α<GOAL>(s * t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>IsRightCancelAdd α<VAR>s t : Set α<GOAL>(s + t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>IsRightCancelAdd α<VAR>s t : Set α<GOAL>(s + t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>IsRightCancelMul α<VAR>s t : Set α<GOAL>(s * t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>s : Set β<GOAL>(a +ᵥ s).Finite ↔ s.Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>s : Set β<GOAL>(a • s).Finite ↔ s.Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>s : Set β<GOAL>(a • s).Infinite ↔ s.Infinite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>s : Set β<GOAL>(a +ᵥ s).Infinite ↔ s.Infinite
<VAR>G : Type u_5<VAR>AddGroup G<VAR>Fintype G<VAR>S : Set G<VAR>(k : ℕ) → DecidablePred fun x => x ∈ k • S<VAR>k : ℕ<GOAL>Fintype.card G ≤ k → Fintype.card ↑(k • S) = Fintype.card ↑(Fintype.card G • S)
<VAR>G : Type u_5<VAR>Group G<VAR>Fintype G<VAR>S : Set G<VAR>(k : ℕ) → DecidablePred fun x => x ∈ S ^ k<VAR>k : ℕ<GOAL>Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.QuasiSeparated f<GOAL>AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.QuasiSeparated f ↔ autoParam (AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)) _auto✝
<VAR>X : AlgebraicGeometry.Scheme<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine Y<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.AffineTargetMorphismProperty.diagonal (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<GOAL>@AlgebraicGeometry.QuasiSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.QuasiCompact
<GOAL>CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.QuasiSeparated
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<GOAL>AlgebraicGeometry.QuasiSeparated f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace ↔ AlgebraicGeometry.QuasiSeparated (CategoryTheory.Limits.terminal.from X)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>hY : QuasiSeparatedSpace ↑↑Y.toPresheafedSpace<VAR>AlgebraicGeometry.QuasiSeparated f<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>IsQuasiSeparated ↑U
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.QuasiSeparated (f ≫ g)<GOAL>AlgebraicGeometry.QuasiSeparated f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<GOAL>∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
<VAR>X : TopCat<VAR>F : TopCat.Presheaf CommRingCat X<VAR>U₁ U₂ U₃ U₄ U₅ U₆ U₇ : TopologicalSpace.Opens ↑X<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑(F.obj (Opposite.op U₁))<VAR>y₂ : ↑(F.obj (Opposite.op U₂))<VAR>f : ↑(F.obj (Opposite.op (U₁ ⊔ U₂)))<VAR>x : ↑(F.obj (Opposite.op U₃))<VAR>h₄₁ : U₄ ≤ U₁<VAR>h₄₂ : U₄ ≤ U₂<VAR>h₅₁ : U₅ ≤ U₁<VAR>h₅₃ : U₅ ≤ U₃<VAR>h₆₂ : U₆ ≤ U₂<VAR>h₆₃ : U₆ ≤ U₃<VAR>h₇₄ : U₇ ≤ U₄<VAR>h₇₅ : U₇ ≤ U₅<VAR>h₇₆ : U₇ ≤ U₆<VAR>e₁ : (y₁ |_ U₅) h₅₁ = ((f |_ U₁) ⋯ |_ U₅) h₅₁ ^ n₁ * (x |_ U₅) h₅₃<VAR>e₂ : (y₂ |_ U₆) h₆₂ = ((f |_ U₂) ⋯ |_ U₆) h₆₂ ^ n₂ * (x |_ U₆) h₆₃<GOAL>((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ U₄) h₄₁ |_ U₇) h₇₄ = ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ U₄) h₄₂ |_ U₇) h₇₄
<VAR>X : AlgebraicGeometry.Scheme<VAR>S : ↑X.affineOpens<VAR>U₁ U₂ : X.Opens<VAR>n₁ n₂ : ℕ<VAR>y₁ : ↑Γ(X, U₁)<VAR>y₂ : ↑Γ(X, U₂)<VAR>f : ↑Γ(X, U₁ ⊔ U₂)<VAR>x : ↑Γ(X, X.basicOpen f)<VAR>h₁ : ↑S ≤ U₁<VAR>h₂ : ↑S ≤ U₂<VAR>e₁ : (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ = ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯<VAR>e₂ : (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ = ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → (((f |_ U₁) ⋯ ^ (m + n₂) * y₁) |_ ↑S) h₁ = (((f |_ U₂) ⋯ ^ (m + n₁) * y₂) |_ ↑S) h₂
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>hU' : IsQuasiSeparated U.carrier<VAR>f : ↑Γ(X, U)<VAR>x : ↑Γ(X, X.basicOpen f)<GOAL>∃ n y, (y |_ X.basicOpen f) ⋯ = (f |_ X.basicOpen f) ⋯ ^ n * x
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>hU' : IsQuasiSeparated U.carrier<VAR>f : ↑Γ(X, U)<GOAL>IsLocalization.Away f ↑Γ(X, X.basicOpen f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>CompactSpace ↑↑X.toPresheafedSpace<VAR>QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>CategoryTheory.IsIso ((AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.c.app (Opposite.op (PrimeSpectrum.basicOpen f)))
<VAR>α : Type u_1<VAR>Add α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x ∈ s.addAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a
<VAR>α : Type u_1<VAR>Mul α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x ∈ s.mulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a
<VAR>α : Type u_1<VAR>Add α<VAR>s₁ s₂ t : Set α<VAR>a : α<VAR>h : s₁ ⊆ s₂<GOAL>s₁.addAntidiagonal t a ⊆ s₂.addAntidiagonal t a
<VAR>α : Type u_1<VAR>Mul α<VAR>s₁ s₂ t : Set α<VAR>a : α<VAR>h : s₁ ⊆ s₂<GOAL>s₁.mulAntidiagonal t a ⊆ s₂.mulAntidiagonal t a
<VAR>α : Type u_1<VAR>Mul α<VAR>s t₁ t₂ : Set α<VAR>a : α<VAR>h : t₁ ⊆ t₂<GOAL>s.mulAntidiagonal t₁ a ⊆ s.mulAntidiagonal t₂ a
<VAR>α : Type u_1<VAR>Add α<VAR>s t₁ t₂ : Set α<VAR>a : α<VAR>h : t₁ ⊆ t₂<GOAL>s.addAntidiagonal t₁ a ⊆ s.addAntidiagonal t₂ a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x.swap ∈ s.addAntidiagonal t a ↔ x ∈ t.addAntidiagonal s a
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x.swap ∈ s.mulAntidiagonal t a ↔ x ∈ t.mulAntidiagonal s a
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 * x.1 = a ↔ x ∈ t.mulAntidiagonal s a
<VAR>α : Type u_1<VAR>AddCommSemigroup α<VAR>s t : Set α<VAR>a : α<VAR>x : α × α<GOAL>x.2 ∈ s ∧ x.1 ∈ t ∧ x.2 + x.1 = a ↔ x ∈ t.addAntidiagonal s a
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.mulAntidiagonal t a)<GOAL>(↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.addAntidiagonal t a)<GOAL>(↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.addAntidiagonal t a)<VAR>h : (↑x).1 = (↑y).1<GOAL>x = y
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.mulAntidiagonal t a)<VAR>h : (↑x).1 = (↑y).1<GOAL>x = y
<VAR>α : Type u_1<VAR>CancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.mulAntidiagonal t a)<VAR>h : (↑x).2 = (↑y).2<GOAL>x = y
<VAR>α : Type u_1<VAR>AddCancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.addAntidiagonal t a)<VAR>h : (↑x).2 = (↑y).2<GOAL>x = y
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.mulAntidiagonal t a)<VAR>h₁ : (↑x).1 ≤ (↑y).1<VAR>h₂ : (↑x).2 ≤ (↑y).2<GOAL>x = y
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>a : α<VAR>x y : ↑(s.addAntidiagonal t a)<VAR>h₁ : (↑x).1 ≤ (↑y).1<VAR>h₂ : (↑x).2 ≤ (↑y).2<GOAL>x = y
<VAR>α : Type u_1<VAR>OrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<GOAL>(s.mulAntidiagonal t a).Finite
<VAR>α : Type u_1<VAR>OrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<VAR>a : α<GOAL>(s.addAntidiagonal t a).Finite
<VAR>α : Type u_1<VAR>LinearOrderedCancelCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>a : α<GOAL>(s.mulAntidiagonal t a).Finite
<VAR>α : Type u_1<VAR>LinearOrderedCancelAddCommMonoid α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>a : α<GOAL>(s.addAntidiagonal t a).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Set.range (List.map f) = {l | ∀ x ∈ l, x ∈ Set.range f}
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.range (List.map Subtype.val) = {l | ∀ x ∈ l, x ∈ s}
<VAR>α : Type u_1<VAR>l : List α<GOAL>Set.range l.get = {x | x ∈ l}
<VAR>α : Type u_1<VAR>l : List α<GOAL>Set.range l.get? = insert none (some '' {x | x ∈ l})
<VAR>α : Type u_1<VAR>l : List α<VAR>d : α<GOAL>(Set.range fun n => l[n]?.getD d) = insert d {x | x ∈ l}
<VAR>α : Type u_1<VAR>Inhabited α<VAR>l : List α<GOAL>Set.range l.getI = insert default {x | x ∈ l}
<VAR>α : Type u<VAR>x : α<VAR>p : α → Prop<GOAL>(x ∈ {y | p y}) = p x
<VAR>α : Type u<VAR>x : α<GOAL>x ∈ Set.univ
<VAR>α : Type u<VAR>s : Set α<VAR>x : α<GOAL>x ∈ sᶜ ↔ ¬x ∈ s
<VAR>α : Type u<VAR>s t : Set α<GOAL>s \ t = s ∩ tᶜ
<VAR>α : Type u<VAR>s t : Set α<VAR>x : α<GOAL>x ∈ s \ t ↔ x ∈ s ∧ ¬x ∈ t