ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∑ j : κ, ∑ i : { i // g i = j }, f ↑i = ∑ i : ι, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∏ j : κ, ∏ i : { i // g i = j }, f ↑i = ∏ i : ι, f i
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>AddCommMonoid α<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∑ j : κ, ∑ _i : { i // g i = j }, f j = ∑ i : ι, f (g i)
<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>Fintype ι<VAR>Fintype κ<VAR>CommMonoid α<VAR>DecidableEq κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∏ j : κ, ∏ _i : { i // g i = j }, f j = ∏ i : ι, f (g i)
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>CommMonoid β<VAR>Unique α<VAR>Fintype α<VAR>f : α → β<GOAL>∏ x : α, f x = f default
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>AddCommMonoid β<VAR>Unique α<VAR>Fintype α<VAR>f : α → β<GOAL>∑ x : α, f x = f default
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>CommMonoid β<VAR>IsEmpty α<VAR>Fintype α<VAR>f : α → β<GOAL>∏ x : α, f x = 1
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>AddCommMonoid β<VAR>IsEmpty α<VAR>Fintype α<VAR>f : α → β<GOAL>∑ x : α, f x = 0
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>AddCommMonoid β<VAR>Subsingleton α<VAR>Fintype α<VAR>f : α → β<VAR>a : α<GOAL>∑ x : α, f x = f a
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>CommMonoid β<VAR>Subsingleton α<VAR>Fintype α<VAR>f : α → β<VAR>a : α<GOAL>∏ x : α, f x = f a
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>Fintype α<VAR>CommMonoid β<VAR>p : α → Prop<VAR>f : α → β<VAR>DecidablePred p<GOAL>(∏ i : { x // p x }, f ↑i) * ∏ i : { x // ¬p x }, f ↑i = ∏ i : α, f i
<VAR>α : Type u_9<VAR>β : Type u_10<VAR>Fintype α<VAR>AddCommMonoid β<VAR>p : α → Prop<VAR>f : α → β<VAR>DecidablePred p<GOAL>∑ i : { x // p x }, f ↑i + ∑ i : { x // ¬p x }, f ↑i = ∑ i : α, f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<VAR>h : ∀ (i : ι), f i ≠ 1 → i ∈ s<GOAL>∏ i ∈ s, f i = ∏ i : ι, f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<VAR>h : ∀ (i : ι), f i ≠ 0 → i ∈ s<GOAL>∑ i ∈ s, f i = ∑ i : ι, f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>h : ∀ (i j : ι), p i → p j → i = j<VAR>a : α<GOAL>(∏ i : ι, if p i then a else 1) = if ∃ i, p i then a else 1
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>h : ∀ (i j : ι), p i → p j → i = j<VAR>a : α<GOAL>(∑ i : ι, if p i then a else 0) = if ∃ i, p i then a else 0
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → i = j → α<GOAL>(∑ j : ι, if h : i = j then f j h else 0) = f i ⋯
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → i = j → α<GOAL>(∏ j : ι, if h : i = j then f j h else 1) = f i ⋯
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → j = i → α<GOAL>(∑ j : ι, if h : j = i then f j h else 0) = f i ⋯
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : (j : ι) → j = i → α<GOAL>(∏ j : ι, if h : j = i then f j h else 1) = f i ⋯
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : ι → α<GOAL>(∏ j : ι, if i = j then f j else 1) = f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : ι → α<GOAL>(∑ j : ι, if i = j then f j else 0) = f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : ι → α<GOAL>(∏ j : ι, if j = i then f j else 1) = f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>f : ι → α<GOAL>(∑ j : ι, if j = i then f j else 0) = f i
<VAR>ι : Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>α : ι → Type u_9<VAR>(i : ι) → CommMonoid (α i)<VAR>i : ι<VAR>f : (i : ι) → α i<GOAL>∏ j : ι, Pi.mulSingle j (f j) i = f i
<VAR>ι : Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>α : ι → Type u_9<VAR>(i : ι) → AddCommMonoid (α i)<VAR>i : ι<VAR>f : (i : ι) → α i<GOAL>∑ j : ι, Pi.single j (f j) i = f i
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>AddCommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>a : α<GOAL>∑ j : ι, Pi.single i a j = a
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommMonoid α<VAR>DecidableEq ι<VAR>i : ι<VAR>a : α<GOAL>∏ j : ι, Pi.mulSingle i a j = a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CommMonoid α<VAR>Fintype ι<VAR>f : { i // i ∈ Finset.univ } → α<GOAL>∏ i ∈ Finset.univ.attach, f i = ∏ i : ι, f ⟨i, ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>Fintype ι<VAR>f : { i // i ∈ Finset.univ } → α<GOAL>∑ i ∈ Finset.univ.attach, f i = ∑ i : ι, f ⟨i, ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CommMonoid α<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>i : { x // x ∈ s }<GOAL>∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>f : ι → α<VAR>i : { x // x ∈ s }<GOAL>∑ j ∈ s.attach.erase i, f ↑j = ∑ j ∈ s.erase ↑i, f j
<VAR>α : Type u_3<VAR>M : Type u_6<VAR>DecidableEq α<VAR>AddCommMonoid M<VAR>f : α → M<VAR>l : List α<VAR>_hl : l.Nodup<GOAL>l.toFinset.sum f = (List.map f l).sum
<VAR>α : Type u_3<VAR>M : Type u_6<VAR>DecidableEq α<VAR>CommMonoid M<VAR>f : α → M<VAR>l : List α<VAR>_hl : l.Nodup<GOAL>l.toFinset.prod f = (List.map f l).prod
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>l : List α<GOAL>∑ a ∈ l.toFinset, List.count a l = l.length
<VAR>α : Type u_3<VAR>a : Multiset α<VAR>l : List (Multiset α)<GOAL>l.sum.Disjoint a ↔ ∀ b ∈ l, b.Disjoint a
<VAR>α : Type u_3<VAR>a : Multiset α<VAR>l : List (Multiset α)<GOAL>a.Disjoint l.sum ↔ ∀ b ∈ l, a.Disjoint b
<VAR>α : Type u_3<VAR>a : Multiset α<VAR>i : Multiset (Multiset α)<GOAL>i.sum.Disjoint a ↔ ∀ b ∈ i, b.Disjoint a
<VAR>α : Type u_3<VAR>a : Multiset α<VAR>i : Multiset (Multiset α)<GOAL>a.Disjoint i.sum ↔ ∀ b ∈ i, a.Disjoint b
<VAR>α : Type u_3<VAR>β : Type u_6<VAR>i : Finset β<VAR>f : β → Multiset α<VAR>a : Multiset α<GOAL>(i.sum f).Disjoint a ↔ ∀ b ∈ i, (f b).Disjoint a
<VAR>α : Type u_3<VAR>β : Type u_6<VAR>i : Finset β<VAR>f : β → Multiset α<VAR>a : Multiset α<GOAL>a.Disjoint (i.sum f) ↔ ∀ b ∈ i, a.Disjoint (f b)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>a : α<VAR>s : Finset ι<VAR>m : ι → Multiset α<GOAL>a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>∑ a ∈ s.toFinset, Multiset.count a s = Multiset.card s
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>s : Finset α<VAR>m : Multiset α<VAR>hms : ∀ a ∈ m, a ∈ s<GOAL>∑ a ∈ s, Multiset.count a m = Multiset.card m
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>Fintype α<VAR>s : Multiset α<GOAL>∑ a : α, Multiset.count a s = Multiset.card s
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>DecidableEq α<VAR>s : Finset β<VAR>a : α<VAR>f : β → Multiset α<GOAL>Multiset.count a (∑ x ∈ s, f x) = ∑ x ∈ s, Multiset.count a (f x)
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>∑ a ∈ s.toFinset, Multiset.count a s • {a} = s
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>s : Multiset α<VAR>k : ℕ<VAR>h : ∀ a ∈ s, k ∣ Multiset.count a s<GOAL>∃ u, s = k • u
<VAR>α : Type u_3<VAR>DecidableEq α<VAR>CommMonoid α<VAR>S : Multiset α<GOAL>S.toFinset.prod id ∣ S.prod
<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>CommMonoid α<VAR>f : ι → Multiset α<VAR>s : Finset ι<GOAL>(∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod
<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>AddCommMonoid α<VAR>f : ι → Multiset α<VAR>s : Finset ι<GOAL>(∑ x ∈ s, f x).sum = ∑ x ∈ s, (f x).sum
<VAR>α : Type u_3<VAR>M : Type u_6<VAR>CommMonoid M<VAR>f : α → Mˣ<VAR>s : Finset α<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℤ<GOAL>(∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : List α<GOAL>Additive.ofMul s.prod = (List.map (⇑Additive.ofMul) s).sum
<VAR>α : Type u_3<VAR>Monoid α<VAR>s : List (Additive α)<GOAL>Additive.toMul s.sum = (List.map (⇑Additive.toMul) s).prod
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : List α<GOAL>Multiplicative.ofAdd s.sum = (List.map (⇑Multiplicative.ofAdd) s).prod
<VAR>α : Type u_3<VAR>AddMonoid α<VAR>s : List (Multiplicative α)<GOAL>Multiplicative.toAdd s.prod = (List.map (⇑Multiplicative.toAdd) s).sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<GOAL>Additive.ofMul s.prod = (Multiset.map (⇑Additive.ofMul) s).sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset (Additive α)<GOAL>Additive.toMul s.sum = (Multiset.map (⇑Additive.toMul) s).prod
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Finset ι<VAR>f : ι → Additive α<GOAL>Additive.toMul (∑ i ∈ s, f i) = ∏ i ∈ s, Additive.toMul (f i)
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<GOAL>Multiplicative.ofAdd s.sum = (Multiset.map (⇑Multiplicative.ofAdd) s).prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset (Multiplicative α)<GOAL>Multiplicative.toAdd s.prod = (Multiset.map (⇑Multiplicative.toAdd) s).sum
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>Multiplicative.ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, Multiplicative.ofAdd (f i)
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → Multiplicative α<GOAL>Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i)
<VAR>ι : Type u_6<VAR>α : Type u_7<VAR>LinearOrder ι<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>p : Sym2 ι → α<GOAL>∑ i ∈ Finset.filter (fun x => ¬x.IsDiag) s.sym2, p i = ∑ i ∈ Finset.filter (fun i => i.1 < i.2) s.offDiag, p s(i.1, i.2)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>IsOpen (Set.range ⇑f.val.base)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>OpenEmbedding ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>↑f.opensRange = Set.range ⇑f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : U ≤ V<GOAL>f.opensFunctor.obj U ≤ f.opensFunctor.obj V
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : U ≤ V<GOAL>f.opensFunctor.map (CategoryTheory.homOfLE e) = CategoryTheory.homOfLE ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>f.opensFunctor.obj ⊤ = f.opensRange
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<GOAL>(TopologicalSpace.Opens.map f.val.base).obj (f.opensFunctor.obj U) = U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<GOAL>f.opensFunctor.obj ((TopologicalSpace.Opens.map f.val.base).obj U) = f.opensRange ⊓ U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U V : X.Opens<VAR>i : Opposite.op U ⟶ Opposite.op V<GOAL>X.presheaf.map i ≫ (f.appIso V).inv = (f.appIso U).inv ≫ Y.presheaf.map (f.opensFunctor.op.map i)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<GOAL>(f.appIso U).hom = f.app (f.opensFunctor.obj U) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<GOAL>(f.appIso U).hom = f.appLE (f.opensFunctor.obj U) U ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<GOAL>f.app U ≫ (f.appIso ((TopologicalSpace.Opens.map f.val.base).obj U)).inv = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<VAR>hU : U ≤ f.opensRange<GOAL>f.app U ≫ (f.appIso ((TopologicalSpace.Opens.map f.val.base).obj U)).inv = Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<GOAL>(f.appIso U).inv ≫ f.app (f.opensFunctor.obj U) = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<VAR>V : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<GOAL>AlgebraicGeometry.Scheme.Hom.appLE f U V e ≫ (AlgebraicGeometry.Scheme.Hom.appIso f V).inv = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U V : X.Opens<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)<GOAL>(AlgebraicGeometry.Scheme.Hom.appIso f U).inv ≫ AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) V e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U : { U // U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }<GOAL>(AlgebraicGeometry.IsOpenImmersion.opensEquiv f).symm U = (TopologicalSpace.Opens.map f.val.base).obj ↑U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<GOAL>↑((AlgebraicGeometry.IsOpenImmersion.opensEquiv f) U) = (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U
<VAR>R S : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : R<VAR>IsLocalization.Away f S<GOAL>AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
<VAR>X : AlgebraicGeometry.Scheme<VAR>x : ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hxU : x ∈ U<GOAL>∃ R f, AlgebraicGeometry.IsOpenImmersion f ∧ x ∈ Set.range ⇑f.val.base ∧ Set.range ⇑f.val.base ⊆ ↑U
<VAR>X : AlgebraicGeometry.PresheafedSpace CommRingCat<VAR>Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f).toLocallyRingedSpace = AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y.toLocallyRingedSpace f
<VAR>X : AlgebraicGeometry.PresheafedSpace CommRingCat<VAR>Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y.toPresheafedSpace<VAR>H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f<GOAL>(AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toSchemeHom Y f).val = f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace<GOAL>X = Y
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<GOAL>AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toScheme Y f.val = X
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<GOAL>∀ (X_1 : (TopologicalSpace.Opens ↑U)ᵒᵖ), (X.restrict h).presheaf.obj X_1 = X.presheaf.obj (Opposite.op (⋯.functor.obj (Opposite.unop X_1)))
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<GOAL>↑(X.restrict h).toPresheafedSpace = U
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<GOAL>(X.restrict h).toPresheafedSpace = X.restrict h
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<GOAL>(X.ofRestrict h).val.base = f
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<GOAL>(X.ofRestrict h).val.c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V : X.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (X.ofRestrict h) V = X.presheaf.map (⋯.adjunction.counit.app V).op
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V : X.Opens<VAR>W : (X.restrict h).Opens<VAR>e : W ≤ (TopologicalSpace.Opens.map (X.ofRestrict h).val.base).obj V<GOAL>AlgebraicGeometry.Scheme.Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<GOAL>∀ (U_1 : (X.restrict h).Opens), AlgebraicGeometry.Scheme.Hom.appIso (X.ofRestrict h) U_1 = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (X.ofRestrict h)).obj U_1)))
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : U ⟶ TopCat.of ↑↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V W : (TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace)ᵒᵖ<VAR>i : V ⟶ W<GOAL>(X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>h : AlgebraicGeometry.IsOpenImmersion f<VAR>CategoryTheory.Epi f.val.base<GOAL>CategoryTheory.IsIso f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>hf : OpenEmbedding ⇑f.val.base<VAR>∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)<GOAL>AlgebraicGeometry.IsOpenImmersion f
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ AlgebraicGeometry.IsOpenImmersion f ∧ CategoryTheory.Epi f.val.base
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ CategoryTheory.IsIso f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.snd f g).val.base = ((TopologicalSpace.Opens.map g.val.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)).carrier
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.snd f g) = (TopologicalSpace.Opens.map g.val.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.fst g f).val.base = ((TopologicalSpace.Opens.map g.val.base).obj { carrier := Set.range ⇑f.val.base, is_open' := ⋯ }).carrier
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>AlgebraicGeometry.Scheme.Hom.opensRange (CategoryTheory.Limits.pullback.fst g f) = (TopologicalSpace.Opens.map g.val.base).obj (AlgebraicGeometry.Scheme.Hom.opensRange f)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.fst f g ≫ f).val.base = Set.range ⇑f.val.base ∩ Set.range ⇑g.val.base
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<GOAL>Set.range ⇑(CategoryTheory.Limits.pullback.fst g f ≫ g).val.base = Set.range ⇑g.val.base ∩ Set.range ⇑f.val.base
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>AlgebraicGeometry.IsOpenImmersion.lift f g H' ≫ f = g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>l : Y ⟶ X<VAR>hl : l ≫ f = g<GOAL>l = AlgebraicGeometry.IsOpenImmersion.lift f g H'
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>AlgebraicGeometry.IsOpenImmersion g<VAR>e : Set.range ⇑f.val.base = Set.range ⇑g.val.base<GOAL>(AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).hom ≫ g = f
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>AlgebraicGeometry.IsOpenImmersion g<VAR>e : Set.range ⇑f.val.base = Set.range ⇑g.val.base<GOAL>(AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).inv ≫ f = g
<VAR>X Y U : AlgebraicGeometry.Scheme<VAR>f : Y ⟶ U<VAR>g : U ⟶ X<VAR>fg : Y ⟶ X<VAR>H : fg = f ≫ g<VAR>h : AlgebraicGeometry.IsOpenImmersion g<VAR>V : U.Opens<GOAL>(TopologicalSpace.Opens.map f.val.base).obj V = (TopologicalSpace.Opens.map fg.val.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V)
<VAR>X Y U : AlgebraicGeometry.Scheme<VAR>f : Y ⟶ U<VAR>g : U ⟶ X<VAR>fg : Y ⟶ X<VAR>H : fg = f ≫ g<VAR>h : AlgebraicGeometry.IsOpenImmersion g<VAR>V : U.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app f V = (AlgebraicGeometry.Scheme.Hom.appIso g V).inv ≫ AlgebraicGeometry.Scheme.Hom.app fg ((AlgebraicGeometry.Scheme.Hom.opensFunctor g).obj V) ≫ Y.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y U : AlgebraicGeometry.Scheme<VAR>f : U ⟶ Y<VAR>g : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>H : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>V : U.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.IsOpenImmersion.lift f g H) V = (AlgebraicGeometry.Scheme.Hom.appIso f V).inv ≫ AlgebraicGeometry.Scheme.Hom.app g ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V) ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<GOAL>(AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv = AlgebraicGeometry.Scheme.Hom.appLE f (AlgebraicGeometry.Scheme.Hom.opensRange f ⊓ U) ((TopologicalSpace.Opens.map f.val.base).obj U) ⋯
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<GOAL>Y.presheaf.map (CategoryTheory.homOfLE ⋯).op ≫ (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv = AlgebraicGeometry.Scheme.Hom.app f U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>U : Y.Opens<GOAL>AlgebraicGeometry.Scheme.Hom.app f U ≫ (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).hom = Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<VAR>r : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (X.basicOpen r) = Y.basicOpen ((AlgebraicGeometry.Scheme.Hom.appIso f U).inv r)
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<GOAL>Function.Injective ⇑(X.presheaf.germ x)
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsIntegral X<VAR>U : X.Opens<VAR>Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>Function.Injective ⇑(X.germToFunctionField U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>hX : IrreducibleSpace ↑↑X.toPresheafedSpace<VAR>IrreducibleSpace ↑↑Y.toPresheafedSpace<GOAL>f.val.base (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace
<VAR>R : CommRingCat<VAR>IsDomain ↑R<GOAL>genericPoint ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace = ⊥
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsIntegral X<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>h : Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>hU.primeIdealOf ⟨genericPoint ↑↑X.toPresheafedSpace, ⋯⟩ = genericPoint ↑↑(AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsIntegral X<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>IsFractionRing ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField