ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>a x : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<VAR>hx : x ≠ a<GOAL>Multiset.count x ↑(Sym.fill a i s) = Multiset.count x ↑s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym (Option α) n.succ<VAR>h : none ∈ s<GOAL>SymOptionSuccEquiv.encode s = Sum.inl (s.erase none h)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym (Option α) n.succ<VAR>h : none ∉ s<GOAL>SymOptionSuccEquiv.encode s = Sum.inr (Sym.map (fun o => (↑o).get ⋯) s.attach)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym (Option α) n<GOAL>SymOptionSuccEquiv.decode (Sum.inl s) = none ::ₛ s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Sym α n.succ<GOAL>SymOptionSuccEquiv.decode (Sum.inr s) = Sym.map (⇑Function.Embedding.some) s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym (Option α) n.succ<GOAL>SymOptionSuccEquiv.decode (SymOptionSuccEquiv.encode s) = s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>s : Sym (Option α) n ⊕ Sym α n.succ<GOAL>SymOptionSuccEquiv.encode (SymOptionSuccEquiv.decode s) = s
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.QuasiCompact f<VAR>U : Set ↑↑Y.toPresheafedSpace<GOAL>IsOpen U → IsCompact U → IsCompact (⇑f.val.base ⁻¹' U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑f.val.base ⁻¹' U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.QuasiCompact f ↔ IsSpectralMap ⇑f.val.base
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : Set ↑↑X.toPresheafedSpace<GOAL>IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑↑i
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>U : Set ↑↑X.toPresheafedSpace<GOAL>IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑(X.basicOpen i)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.QuasiCompact f ↔ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<GOAL>IsCompact ↑(X.basicOpen f)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<GOAL>AlgebraicGeometry.QuasiCompact f ↔ CompactSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<GOAL>CompactSpace ↑↑X.toPresheafedSpace ↔ AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.terminal.from X)
<GOAL>CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.QuasiCompact
<VAR>X : AlgebraicGeometry.Scheme<VAR>P : X.Opens → Prop<VAR>S : X.Opens<VAR>hS : IsCompact S.carrier<VAR>h₁ : P ⊥<VAR>h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)<GOAL>P S
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : IsCompact U.carrier<VAR>x f : ↑Γ(X, U)<VAR>H : (x |_ X.basicOpen f) ⋯ = 0<GOAL>∃ n, f ^ n * x = 0
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>f : ↑Γ(X, U)<GOAL>IsNilpotent f ↔ X.basicOpen f = ⊥
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>s : Set ↑Γ(X, U)<GOAL>X.zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical ↑Γ(X, U))
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y S : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>AlgebraicGeometry.IsAffine Y<VAR>AlgebraicGeometry.IsAffine S<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>H : P (AlgebraicGeometry.Scheme.Hom.app g ⊤)<GOAL>P (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.Limits.pullback.fst f g) ⊤)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>(AlgebraicGeometry.sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).toProperty.RespectsIso
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>(AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>AlgebraicGeometry.sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] => P) (f ∣_ U) ↔ ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (AlgebraicGeometry.Scheme.Hom.appLE f U (↑V) e)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.affineLocally (fun {R S} [CommRing R] [CommRing S] => P) f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U), P (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>h₂ : RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P<VAR>h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => P<GOAL>(AlgebraicGeometry.sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => P).IsLocal
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop)<VAR>self : AlgebraicGeometry.HasRingHomProperty P Q<GOAL>P = AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop)<VAR>self : AlgebraicGeometry.HasRingHomProperty P Q<GOAL>RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<GOAL>P = AlgebraicGeometry.affineLocally fun {R S} [CommRing R] [CommRing S] => Q
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<GOAL>AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.sourceAffineLocally fun {R S} [CommRing R] [CommRing S] => Q)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : P f<VAR>U : ↑Y.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ f ⁻¹ᵁ ↑U<GOAL>Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : P f<VAR>AlgebraicGeometry.IsAffine X<VAR>AlgebraicGeometry.IsAffine Y<GOAL>Q (AlgebraicGeometry.Scheme.Hom.app f ⊤)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>H : P g<GOAL>P (f ≫ g)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>P f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<VAR>𝒰 : X.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<VAR>H : ∀ (i : 𝒰.J), Q (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i ≫ f) ⊤)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<VAR>𝒰 : X.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<GOAL>P f ↔ ∀ (i : 𝒰.J), Q (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i ≫ f) ⊤)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine X<VAR>AlgebraicGeometry.IsAffine Y<GOAL>P f ↔ Q (AlgebraicGeometry.Scheme.Hom.app f ⊤)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>R S : CommRingCat<VAR>φ : R ⟶ S<GOAL>P (AlgebraicGeometry.Spec.map φ) ↔ Q φ
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<VAR>ι : Type u_1<VAR>U : ι → ↑X.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>H : ∀ (i : ι), Q (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<VAR>ι : Type u_1<VAR>U : ι → ↑X.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<GOAL>P f ↔ ∀ (i : ι), Q (AlgebraicGeometry.Scheme.Hom.appLE f ⊤ ↑(U i) ⋯)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>H : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T), Q (g.comp f) → Q g<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : P (f ≫ g)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>AlgebraicGeometry.HasRingHomProperty P Q<VAR>hP : RingHom.StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => Q<GOAL>P.StableUnderBaseChange
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α β : TypeVec.{u} n<VAR>g : α ⟹ β<VAR>a : P.A<VAR>f : P.B a ⟹ α<GOAL>g <$$> ⟨a, f⟩ = ⟨a, g ⊚ f⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α : TypeVec.{u} n<VAR>x : ↑P α<GOAL>TypeVec.id <$$> x = x
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α β γ : TypeVec.{u} n<VAR>f : α ⟹ β<VAR>g : β ⟹ γ<VAR>x : ↑P α<GOAL>(g ⊚ f) <$$> x = g <$$> f <$$> x
<VAR>n : ℕ<VAR>A : Type u<VAR>α β : TypeVec.{u} n<VAR>f : α ⟹ β<VAR>x : ↑(MvPFunctor.const n A) α<GOAL>MvPFunctor.const.get (f <$$> x) = MvPFunctor.const.get x
<VAR>n : ℕ<VAR>A : Type u<VAR>α : TypeVec.{u} n<VAR>x : A<GOAL>MvPFunctor.const.get (MvPFunctor.const.mk n x) = x
<VAR>n : ℕ<VAR>A : Type u<VAR>α : TypeVec.{u} n<VAR>x : ↑(MvPFunctor.const n A) α<GOAL>MvPFunctor.const.mk n (MvPFunctor.const.get x) = x
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α β : TypeVec.{u} m<VAR>f : α ⟹ β<VAR>x : ↑(P.comp Q) α<GOAL>MvPFunctor.comp.get (f <$$> x) = (fun i x => f <$$> x) <$$> MvPFunctor.comp.get x
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α : TypeVec.{u} m<VAR>x : ↑P fun i => ↑(Q i) α<GOAL>MvPFunctor.comp.get (MvPFunctor.comp.mk x) = x
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α : TypeVec.{u} m<VAR>x : ↑(P.comp Q) α<GOAL>MvPFunctor.comp.mk (MvPFunctor.comp.get x) = x
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : ↑P α<GOAL>MvFunctor.LiftP p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>a : P.A<VAR>f : P.B a ⟹ α<GOAL>MvFunctor.LiftP p ⟨a, f⟩ ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α : TypeVec.{u} n<VAR>r : ⦃i : Fin2 n⦄ → α i → α i → Prop<VAR>x y : ↑P α<GOAL>MvFunctor.LiftR r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), r (f₀ i j) (f₁ i j)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} n<VAR>α : TypeVec.{u} n<VAR>a : P.A<VAR>f : P.B a ⟹ α<VAR>i : Fin2 n<GOAL>MvFunctor.supp ⟨a, f⟩ i = f i '' Set.univ
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : X.OpenCover<VAR>x : self.J<GOAL>AlgebraicGeometry.IsOpenImmersion (self.map x)
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : X.OpenCover<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Set.range ⇑(self.map (self.f x)).val.base
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>⋃ i, Set.range ⇑(𝒰.map i).val.base = Set.univ
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>⨆ i, AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.map i) = ⊤
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : (i : 𝒰.J) × (f i).J<GOAL>(𝒰.bind f).obj x = (f x.fst).obj x.snd
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<GOAL>(𝒰.bind f).J = ((i : 𝒰.J) × (f i).J)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : (x : 𝒰.J) → (𝒰.obj x).OpenCover<VAR>x : (i : 𝒰.J) × (f i).J<GOAL>(𝒰.bind f).map x = (f x.fst).map x.snd ≫ 𝒰.map x.fst
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>(AlgebraicGeometry.Scheme.openCoverOfIsIso f).J = PUnit.{v + 1}
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>∀ (x : PUnit.{v + 1}), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).map x = f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>∀ (x : PUnit.{v + 1}), (AlgebraicGeometry.Scheme.openCoverOfIsIso f).obj x = X
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>J : Type u_1<VAR>obj : J → AlgebraicGeometry.Scheme<VAR>map : (i : J) → obj i ⟶ X<VAR>e₁ : J ≃ 𝒰.J<VAR>e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)<GOAL>∀ (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (e₁ i)) (i : J), (𝒰.copy J obj map e₁ e₂ e₂_1).map i = map i
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>J : Type u_1<VAR>obj : J → AlgebraicGeometry.Scheme<VAR>map : (i : J) → obj i ⟶ X<VAR>e₁ : J ≃ 𝒰.J<VAR>e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)<GOAL>∀ (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (e₁ i)), (𝒰.copy J obj map e₁ e₂ e₂_1).J = J
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>J : Type u_1<VAR>obj : J → AlgebraicGeometry.Scheme<VAR>map : (i : J) → obj i ⟶ X<VAR>e₁ : J ≃ 𝒰.J<VAR>e₂ : (i : J) → obj i ≅ 𝒰.obj (e₁ i)<GOAL>∀ (e₂_1 : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.map (e₁ i)) (a : J), (𝒰.copy J obj map e₁ e₂ e₂_1).obj a = obj a
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>∀ (x : 𝒰.J), (𝒰.pushforwardIso f).map x = 𝒰.map x ≫ f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>∀ (x : 𝒰.J), (𝒰.pushforwardIso f).obj x = 𝒰.obj x
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>(𝒰.pushforwardIso f).J = 𝒰.J
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : Y ⟶ X<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>i : Option 𝒰.J<GOAL>(𝒰.add f).obj i = Option.rec Y 𝒰.obj i
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : Y ⟶ X<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>(𝒰.add f).f x = some (𝒰.f x)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : Y ⟶ X<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>i : Option 𝒰.J<GOAL>(𝒰.add f).map i = Option.rec f 𝒰.map i
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : Y ⟶ X<VAR>AlgebraicGeometry.IsOpenImmersion f<GOAL>(𝒰.add f).J = Option 𝒰.J
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : 𝒰.J<GOAL>(𝒰.pullbackCover f).map x = CategoryTheory.Limits.pullback.fst f (𝒰.map x)
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>(𝒰.pullbackCover f).f x = 𝒰.f (f.val.base x)
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<GOAL>(𝒰.pullbackCover f).J = 𝒰.J
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : 𝒰.J<GOAL>(𝒰.pullbackCover f).obj x = CategoryTheory.Limits.pullback f (𝒰.map x)
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>i : (𝒰.pullbackCover f).J<GOAL>𝒰.pullbackHom f i ≫ 𝒰.map i = (𝒰.pullbackCover f).map i ≫ f
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : ↑↑W.toPresheafedSpace<GOAL>(𝒰.pullbackCover' f).f x = 𝒰.f (f.val.base x)
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<GOAL>(𝒰.pullbackCover' f).J = 𝒰.J
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : 𝒰.J<GOAL>(𝒰.pullbackCover' f).map x = CategoryTheory.Limits.pullback.snd (𝒰.map x) f
<VAR>X W : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : W ⟶ X<VAR>x : 𝒰.J<GOAL>(𝒰.pullbackCover' f).obj x = CategoryTheory.Limits.pullback (𝒰.map x) f
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>H : CompactSpace ↑↑X.toPresheafedSpace<VAR>x : { x // x ∈ ⋯.choose }<GOAL>𝒰.finiteSubcover.obj x = 𝒰.obj (𝒰.f ↑x)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>H : CompactSpace ↑↑X.toPresheafedSpace<VAR>x : { x // x ∈ ⋯.choose }<GOAL>𝒰.finiteSubcover.map x = 𝒰.map (𝒰.f ↑x)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>Finite 𝒰.J<VAR>H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<GOAL>CompactSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : X.AffineOpenCover<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ Set.range ⇑(self.map (self.f x)).val.base
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : X.AffineOpenCover<VAR>x : self.J<GOAL>AlgebraicGeometry.IsOpenImmersion (self.map x)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 : X.AffineOpenCover<VAR>j : 𝓤.J<GOAL>𝓤.openCover.obj j = AlgebraicGeometry.Spec (𝓤.obj j)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 : X.AffineOpenCover<VAR>j : 𝓤.J<GOAL>𝓤.openCover.map j = 𝓤.map j
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 : X.AffineOpenCover<GOAL>𝓤.openCover.J = 𝓤.J
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 : X.AffineOpenCover<GOAL>∀ (a : ↑↑X.toPresheafedSpace), 𝓤.openCover.f a = 𝓤.f a
<VAR>X : AlgebraicGeometry.Scheme<GOAL>X.affineOpenCover.openCover = X.affineCover
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.affineRefinement.openCover.pullbackCover f).J<GOAL>(AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫ (𝒰.affineRefinement.openCover.pullbackCover f).map i = ((𝒰.obj i.fst).affineCover.pullbackCover (𝒰.pullbackHom f i.fst)).map i.snd ≫ (𝒰.pullbackCover f).map i.fst
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>i : (𝒰.affineRefinement.openCover.pullbackCover f).J<GOAL>(AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv ≫ 𝒰.affineRefinement.openCover.pullbackHom f i = (𝒰.obj i.fst).affineCover.pullbackHom (𝒰.pullbackHom f i.fst) i.snd
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 𝓥 : X.OpenCover<VAR>self : 𝓤.Hom 𝓥<VAR>j : 𝓤.J<GOAL>self.app j ≫ 𝓥.map (self.idx j) = 𝓤.map j
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 𝓥 : X.OpenCover<VAR>self : 𝓤.Hom 𝓥<VAR>j : 𝓤.J<GOAL>AlgebraicGeometry.IsOpenImmersion (self.app j)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 : X.OpenCover<VAR>j : 𝓤.J<GOAL>(𝟙 𝓤).idx j = j
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 : X.OpenCover<VAR>j : 𝓤.J<GOAL>(𝟙 𝓤).app j = 𝟙 (𝓤.obj j)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 𝓥 𝓦 : X.OpenCover<VAR>f : 𝓤 ⟶ 𝓥<VAR>g : 𝓥 ⟶ 𝓦<VAR>j : 𝓤.J<GOAL>(f ≫ g).idx j = g.idx (f.idx j)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝓤 𝓥 𝓦 : X.OpenCover<VAR>f : 𝓤 ⟶ 𝓥<VAR>g : 𝓥 ⟶ 𝓦<VAR>j : 𝓤.J<GOAL>(f ≫ g).app j = f.app j ≫ g.app (f.idx j)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>f g : ↑(X.presheaf.obj (Opposite.op U))<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) f = (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) g<GOAL>f = g
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : ↑(X.presheaf.obj (Opposite.op U))<VAR>𝒰 : X.OpenCover<VAR>h : ∀ (i : 𝒰.J), (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) s = 0<GOAL>s = 0
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : ↑(X.presheaf.obj (Opposite.op U))<VAR>𝒰 : X.OpenCover<VAR>Finite 𝒰.J<VAR>h : ∀ (i : 𝒰.J), IsNilpotent ((AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) s)<GOAL>IsNilpotent s
<VAR>X : AlgebraicGeometry.Scheme<VAR>i : X.affineBasisCover.J<GOAL>X.affineBasisCover.obj i = AlgebraicGeometry.Spec (X.affineBasisCoverRing i)
<VAR>X : AlgebraicGeometry.Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>r : ↑⋯.choose<GOAL>Set.range ⇑(X.affineBasisCover.map ⟨x, r⟩).val.base = ⇑(X.affineCover.map x).val.base '' (PrimeSpectrum.basicOpen r).carrier
<VAR>X : AlgebraicGeometry.Scheme<GOAL>TopologicalSpace.IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.map a).val.base}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>x : α<GOAL>x ∈ f.Dom ↔ ∃ y, y ∈ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<GOAL>(PFun.Dom fun x => { Dom := p x, get := f x }) = {x | p x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<GOAL>f.Dom = {x | ∃ y, y ∈ f x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>a : α<GOAL>f.fn a = (f a).get
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α →. β<VAR>H1 : ∀ (a : α), a ∈ f.Dom ↔ a ∈ g.Dom<VAR>H2 : ∀ (a : α) (p : f.Dom a) (q : g.Dom a), f.fn a p = g.fn a q<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f g : α →. β<VAR>H : ∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>x : α<VAR>y : β<VAR>fxy : y ∈ f x<VAR>domx : x ∈ f.Dom<GOAL>f.asSubtype ⟨x, domx⟩ = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<GOAL>↑f a = Part.some (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>(↑f).Dom = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Injective PFun.lift
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>s : Set α<VAR>h : s ⊆ f.Dom<VAR>a : α<VAR>b : β<GOAL>b ∈ f.restrict h a ↔ a ∈ s ∧ b ∈ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>b ∈ PFun.res f s a ↔ a ∈ s ∧ f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>PFun.res f Set.univ = ↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α →. β<VAR>x : α<GOAL>x ∈ f.Dom ↔ ∃ y, (x, y) ∈ f.graph
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>(a, b) ∈ (↑f).graph ↔ f a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α →. β<VAR>g : β → α →. γ<VAR>a : α<GOAL>f.bind g a = (f a).bind fun b => g b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : Set α<VAR>x : β<GOAL>p ⊆ (PFun.pure x).Dom
<VAR>α : Type u_7<VAR>β γ : Type u_8<VAR>p : Set α<VAR>f : α →. β<VAR>g : β → α →. γ<VAR>H1 : p ⊆ f.Dom<VAR>H2 : ∀ (x : β), p ⊆ (g x).Dom<GOAL>p ⊆ (f >>= g).Dom