ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>r : β → β → Prop<VAR>hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z<VAR>c : β<GOAL>r c (Finset.fold op b f s) ↔ r c b ∨ ∃ x ∈ s, r c (f x)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.fold (fun x x_1 => x ∪ x_1) ∅ singleton s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.fold (fun x x_1 => x ⊔ x_1) ⊥ singleton s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>c ≤ Finset.fold min b f s ↔ c ≤ b ∧ ∀ x ∈ s, c ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>Finset.fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>c < Finset.fold min b f s ↔ c < b ∧ ∀ x ∈ s, c < f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>Finset.fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>Finset.fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>c ≤ Finset.fold max b f s ↔ c ≤ b ∨ ∃ x ∈ s, c ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>Finset.fold max b f s < c ↔ b < c ∧ ∀ x ∈ s, f x < c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>LinearOrder β<VAR>c : β<GOAL>c < Finset.fold max b f s ↔ c < b ∨ ∃ x ∈ s, c < f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>LinearOrder β<VAR>Add β<VAR>CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : WithBot β<VAR>s : Finset α<GOAL>Finset.fold max ⊥ (fun x => ↑(f x) + n) s = Finset.fold max ⊥ (WithBot.some ∘ f) s + n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>h : (↑s).PairwiseDisjoint t<GOAL>(s.disjiUnion t h).val = s.val.bind fun a => (t a).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Finset β<GOAL>∅.disjiUnion t ⋯ = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>b : β<VAR>h : (↑s).PairwiseDisjoint t<GOAL>b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>h : (↑s).PairwiseDisjoint t<GOAL>↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>f : α → Finset β<VAR>H : (↑(Finset.cons a s ha)).PairwiseDisjoint f<GOAL>(Finset.cons a s ha).disjiUnion f H = (f a).disjUnion (s.disjiUnion f ⋯) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Finset β<VAR>a : α<VAR>h : (↑{a}).PairwiseDisjoint t<GOAL>{a}.disjiUnion t h = t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<VAR>h1 : (↑s).PairwiseDisjoint f<VAR>h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g<GOAL>(s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun a => (f ↑a).disjiUnion g ⋯) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<GOAL>(↑t).PairwiseDisjoint fun a => Finset.filter (fun x => f x = a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<GOAL>t.disjiUnion (fun a => Finset.filter (fun x => f x = a) s) ⋯ = Finset.filter (fun c => f c ∈ t) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>h : ∀ x ∈ s, f x ∈ t<GOAL>t.disjiUnion (fun a => Finset.filter (fun x => f x = a) s) ⋯ = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : α → Finset β<GOAL>(s.biUnion t).val = (s.val.bind fun a => (t a).val).dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Finset β<VAR>DecidableEq β<GOAL>∅.biUnion t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>DecidableEq β<VAR>b : β<GOAL>b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>DecidableEq β<GOAL>↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>DecidableEq β<VAR>DecidableEq α<VAR>a : α<GOAL>(insert a s).biUnion t = t a ∪ s.biUnion t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : α → Finset β<VAR>DecidableEq β<VAR>hs : s₁ = s₂<VAR>ht : ∀ a ∈ s₁, t₁ a = t₂ a<GOAL>s₁.biUnion t₁ = s₂.biUnion t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>hf : (↑s).PairwiseDisjoint f<GOAL>s.disjiUnion f hf = s.biUnion f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>DecidableEq β<VAR>s' : Finset β<GOAL>s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : α → Finset β<VAR>DecidableEq β<VAR>a : α<GOAL>{a}.biUnion t = t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>t : Finset β<GOAL>s.biUnion f ∩ t = s.biUnion fun x => f x ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>t : Finset β<VAR>s : Finset α<VAR>f : α → Finset β<GOAL>t ∩ s.biUnion f = s.biUnion fun x => t ∩ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>s : Finset α<VAR>f : α → Finset β<VAR>g : β → Finset γ<GOAL>(s.biUnion f).biUnion g = s.biUnion fun a => (f a).biUnion g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>s : Multiset α<VAR>t : α → Multiset β<GOAL>(s.bind t).toFinset = s.toFinset.biUnion fun a => (t a).toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t₁ t₂ : α → Finset β<VAR>DecidableEq β<VAR>h : ∀ a ∈ s, t₁ a ⊆ t₂ a<GOAL>s.biUnion t₁ ⊆ s.biUnion t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s₁ s₂ : Finset α<VAR>DecidableEq β<VAR>t : α → Finset β<VAR>h : s₁ ⊆ s₂<GOAL>s₁.biUnion t ⊆ s₂.biUnion t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>DecidableEq β<VAR>u : α → Finset β<VAR>x : α<VAR>xs : x ∈ s<GOAL>u x ⊆ s.biUnion u
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → Finset β<GOAL>s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t
<VAR>α : Type u_1<VAR>s : Finset α<VAR>DecidableEq α<GOAL>s.biUnion singleton = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>p : β → Prop<VAR>DecidablePred p<GOAL>Finset.filter p (s.biUnion f) = s.biUnion fun a => Finset.filter p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>h : ∀ x ∈ s, f x ∈ t<GOAL>(t.biUnion fun a => Finset.filter (fun c => f c = a) s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → Finset β<VAR>s : Finset α<VAR>b : β<GOAL>(s.biUnion f).erase b = s.biUnion fun x => (f x).erase b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>DecidableEq β<GOAL>(s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : α → Finset β<VAR>DecidableEq β<VAR>hs : s.Nonempty<VAR>ht : ∀ x ∈ s, (t x).Nonempty<GOAL>(s.biUnion t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>t : Finset β<GOAL>Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>s : Finset β<VAR>t : Finset α<VAR>f : α → Finset β<GOAL>Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Finite ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>r : (i : ι) → α i → Finset (α i) → Prop<VAR>H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>f : (i : ι) → Finset (α i)<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (Function.update g i (insert x (g i)))<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Finite ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>f : (i : ι) → Finset (α i)<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι), ∀ x ∉ g i, p g → p (Function.update g i (insert x (g i)))<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Finite ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → LinearOrder (α i)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>f : (i : ι) → Finset (α i)<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), (∀ y ∈ g i, y < x) → p g → p (Function.update g i (insert x (g i)))<GOAL>p f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>Finite ι<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (α i)<VAR>(i : ι) → LinearOrder (α i)<VAR>p : ((i : ι) → Finset (α i)) → Prop<VAR>f : (i : ι) → Finset (α i)<VAR>h0 : p fun x => ∅<VAR>step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), (∀ y ∈ g i, x < y) → p g → p (Function.update g i (insert x (g i)))<GOAL>p f
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>x : (i : ι) → π i<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>y : (i : { x // x ∈ s }) → π ↑i<GOAL>Function.updateFinset x s y = fun i => if hi : i ∈ s then y ⟨i, hi⟩ else x i
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>x : (i : ι) → π i<VAR>DecidableEq ι<VAR>y : (i : { x // x ∈ ∅ }) → π ↑i<GOAL>Function.updateFinset x ∅ y = x
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>x : (i : ι) → π i<VAR>DecidableEq ι<VAR>i : ι<VAR>y : (i_1 : { x // x ∈ {i} }) → π ↑i_1<GOAL>Function.updateFinset x {i} y = Function.update x i (y ⟨i, ⋯⟩)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>x : (i : ι) → π i<VAR>DecidableEq ι<VAR>i : ι<VAR>y : π i<GOAL>Function.update x i y = Function.updateFinset x {i} (uniqueElim y)
<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>x : (i : ι) → π i<VAR>DecidableEq ι<VAR>s t : Finset ι<VAR>hst : Disjoint s t<VAR>y : (i : { x // x ∈ s }) → π ↑i<VAR>z : (i : { x // x ∈ t }) → π ↑i<GOAL>Function.updateFinset (Function.updateFinset x s y) t z = Function.updateFinset x (s ∪ t) ((Equiv.piFinsetUnion π hst) (y, z))
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<GOAL>(s.pi t).val = s.val.pi fun a => (t a).val
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>f : (a : α) → a ∈ s → β a<GOAL>f ∈ s.pi t ↔ ∀ (a : α) (h : a ∈ s), f a h ∈ t a
<VAR>α : Type u_1<VAR>δ : α → Sort v<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>b : δ a<VAR>f : (a : α) → a ∈ s → δ a<VAR>h : a ∈ insert a s<GOAL>Finset.Pi.cons s a b f a h = b
<VAR>α : Type u_1<VAR>δ : α → Sort v<VAR>DecidableEq α<VAR>s : Finset α<VAR>a a' : α<VAR>b : δ a<VAR>f : (a : α) → a ∈ s → δ a<VAR>h : a' ∈ insert a s<VAR>ha : a ≠ a'<GOAL>Finset.Pi.cons s a b f a' h = f a' ⋯
<VAR>α : Type u_1<VAR>δ : α → Sort v<VAR>DecidableEq α<VAR>a : α<VAR>b : δ a<VAR>s : Finset α<VAR>hs : a ∉ s<GOAL>Function.Injective (Finset.Pi.cons s a b)
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>DecidableEq α<VAR>t : (a : α) → Finset (β a)<GOAL>∅.pi t = {Finset.Pi.empty β}
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<GOAL>(s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>DecidableEq α<VAR>(a : α) → DecidableEq (β a)<VAR>s : Finset α<VAR>t : (a : α) → Finset (β a)<VAR>a : α<VAR>ha : a ∉ s<GOAL>(insert a s).pi t = (t a).biUnion fun b => Finset.image (Finset.Pi.cons s a b) (s.pi t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<GOAL>(s.pi fun a => {f a}) = {fun a x => f a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>β : Type u_2<VAR>s : Finset α<VAR>i : β<GOAL>(s.pi fun x => {i}) = {fun x x => i}
<VAR>α : Type u_1<VAR>β : α → Type u<VAR>DecidableEq α<VAR>s : Finset α<VAR>t₁ t₂ : (a : α) → Finset (β a)<VAR>h : ∀ a ∈ s, t₁ a ⊆ t₂ a<GOAL>s.pi t₁ ⊆ s.pi t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>δ : α → Type u_2<VAR>s : Finset α<VAR>t₁ t₂ : (a : α) → Finset (δ a)<VAR>a : α<VAR>ha : a ∈ s<VAR>h : Disjoint (t₁ a) (t₂ a)<GOAL>Disjoint (s.pi t₁) (s.pi t₂)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>DecidableEq (ι → α)<VAR>s : Finset α<VAR>f : ι → α<GOAL>f ∈ s.piDiag ι ↔ ∃ a ∈ s, Function.const ι a = f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>ι : Type u_3<VAR>DecidableEq (ι → α)<VAR>Nonempty ι<GOAL>(s.piDiag ι).card = s.card
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>HomogeneousLocalization.mk z ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat<GOAL>(AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x).IsPrime
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace<GOAL>(AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f x).asIdeal = AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f ⁻¹' ↑(PrimeSpectrum.basicOpen (HomogeneousLocalization.mk z)) = Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑z.num)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace<GOAL>((AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) x).asIdeal = AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>⇑(AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) ⁻¹' ↑(PrimeSpectrum.basicOpen (HomogeneousLocalization.mk z)) = Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑z.num)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>a : A<GOAL>a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ ∀ (i : ℕ), HomogeneousLocalization.mk { deg := m * i, num := ⟨(GradedAlgebra.proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>a : A<GOAL>a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ ∀ (i : ℕ), Localization.mk ((GradedAlgebra.proj 𝒜 i) a ^ m) ⟨f ^ i, ⋯⟩ ∈ ⇑(algebraMap (HomogeneousLocalization.Away 𝒜 f) (Localization.Away f)) '' {s | s ∈ q.asIdeal}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 n<GOAL>a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ HomogeneousLocalization.mk { deg := m * n, num := ⟨a ^ m, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>a : A<VAR>n : ℕ<VAR>hn : a ∈ 𝒜 (n * m)<GOAL>a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ HomogeneousLocalization.mk { deg := m * n, num := ⟨a, ⋯⟩, den := ⟨f ^ n, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>↑z.num ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>a b : A<VAR>ha : a ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q<VAR>hb : b ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q<GOAL>a + b ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>0 ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<VAR>c x : A<VAR>hx : x ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q<GOAL>c • x ∈ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>Ideal.IsHomogeneous 𝒜 (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>f ∉ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>¬HomogeneousIdeal.irrelevant 𝒜 ≤ AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asHomogeneousIdeal f_deg hm q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q ≠ ⊤
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>(AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal f_deg hm q).IsPrime
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace<GOAL>(AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) (AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace<GOAL>AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm ((AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>Function.Injective ⇑(AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>Function.Surjective ⇑(AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>Function.Bijective ⇑(AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>a : A<VAR>i : ℕ<GOAL>⇑(AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) '' (Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑(((DirectSum.decompose 𝒜) a) i))) = (PrimeSpectrum.basicOpen (HomogeneousLocalization.mk { deg := m * i, num := ⟨↑(((DirectSum.decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ })).carrier
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection 𝒜 f) ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ x) = CategoryTheory.CategoryStruct.comp (HomogeneousLocalization.mapId 𝒜 ⋯) (AlgebraicGeometry.Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f) (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.Γgerm x) = CategoryTheory.CategoryStruct.comp (HomogeneousLocalization.mapId 𝒜 ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrictStalkIso ⋯ x).inv)