mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ 𝟙 (r₁ ≫ g) ⊗≫ (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) β) ⊗≫ 𝟙 (h ≫ r₃) =
    (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)

Tactic:
]

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ 𝟙 (r₁ ≫ g) ⊗≫ (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) β) ⊗≫ 𝟙 (h ≫ r₃) =
    (mateEquiv adj₁ adj₃) (leftAdjointConjugateSquare.vcomp α β)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ f ∉ z.asHomogeneousIdeal ↔ ∃ u ∈ Set.range fun i ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f), z ∈ u
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedRing.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) f), ↑(((decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), (GradedRing.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) f), ↑(((decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
i : ℕ
hi : (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
⊢ (GradedRing.proj 𝒜 i) f ∉ z.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a ∈ s, a ∉ ↑p.asHomogeneousIdeal
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen 𝒜 r), p ∈ v ∧ v ⊆ U

Tactic:
]

Goal state after:
case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a ∈ s, a ∉ ↑p.asHomogeneousIdeal
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen 𝒜 r), p ∈ v ∧ v ⊆ U
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}

Tactic:
]

Goal state after:
case h_nhds
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ↑F ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
]

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
⊢ ↑F ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ ↑x.asHomogeneousIdeal ⊆ ↑y.asHomogeneousIdeal
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ ∑ i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) s), ↑(((DirectSum.decompose 𝒜) s) i) ∈
    ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))

Tactic:
]

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
F : Finset S
hF : Algebra.adjoin ↥(𝒜 0) ↑F = ⊤
ι₀ : Type (max u_1 u_3) := (x : ↥F) × ↥(DFinsupp.support ((DirectSum.decompose 𝒜) ↑x))
x : ι₀ → S := fun i ↦ ↑(((DirectSum.decompose 𝒜) ↑i.fst) ↑i.snd)
s : S
hs : s ∈ ↑F
⊢ ∑ i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) s), ↑(((DirectSum.decompose 𝒜) s) i) ∈
    ↑(Algebra.adjoin ↥(𝒜 0) ↑(Finset.image x Finset.univ))
Module: Mathlib.Data.FunLike.Graded

Goal state before:
pp: E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ ↑y ∈ ℬ i

Tactic:
]

Goal state after:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst✝³ : SetLike σ A
inst✝² : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝¹ : EquivLike E A B
inst✝ : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ ↑y ∈ ℬ i
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
σ : Type u_6
τ : Type u_7
ψ : Type u_8
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Semiring C
inst✝² : SetLike σ A
inst✝¹ : SetLike τ B
inst✝ : SetLike ψ C
𝒜 : ι → σ
ℬ : ι → τ
𝒞 : ι → ψ
g : ℬ →+*ᵍ 𝒞
f₁ f₂ : 𝒜 →+*ᵍ ℬ
hg : Function.Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : A
⊢ g (f₂ x) = g (f₂ x)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.FiniteType

Goal state before:
pp: S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ ↑s ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑({x ∈ s | n x ≠ 0}))

Tactic:
]

Goal state after:
S : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : CommRing S
inst✝³ : SetLike σ S
inst✝² : AddSubgroupClass σ S
𝒜 : ι → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) S
s : Finset S
h₁ : Algebra.adjoin ↥(𝒜 0) ↑s = ⊤
n : S → ι
hn : ∀ i ∈ s, i ∈ 𝒜 (n i)
⊢ ↑s ⊆ ↑(Algebra.adjoin ↥(𝒜 0) ↑({x ∈ s | n x ≠ 0}))
Module: Mathlib.RingTheory.GradedAlgebra.RingHom

Goal state before:
pp: ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : DecidableEq ι
inst✝⁷ : AddMonoid ι
inst✝⁶ : AddSubmonoidClass σ A
inst✝⁵ : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝⁴ : GradedRing 𝒜
inst✝³ : GradedRing ℬ
F : Type u_10
inst✝² : FunLike F A B
inst✝¹ : GradedFunLike F 𝒜 ℬ
inst✝ : RingHomClass F A B
f : F
x : A
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), (decompose ℬ) (f ↑(((decompose 𝒜) x) i)) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x), (map (↑f).gradedAddHom) ((decompose 𝒜) ↑(((decompose 𝒜) x) x_1))

Tactic:
]

Goal state after:
ι : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_6
τ : Type u_7
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : SetLike σ A
inst✝⁹ : SetLike τ B
inst✝⁸ : DecidableEq ι
inst✝⁷ : AddMonoid ι
inst✝⁶ : AddSubmonoidClass σ A
inst✝⁵ : AddSubmonoidClass τ B
𝒜 : ι → σ
ℬ : ι → τ
inst✝⁴ : GradedRing 𝒜
inst✝³ : GradedRing ℬ
F : Type u_10
inst✝² : FunLike F A B
inst✝¹ : GradedFunLike F 𝒜 ℬ
inst✝ : RingHomClass F A B
f : F
x : A
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), (decompose ℬ) (f ↑(((decompose 𝒜) x) i)) =
    ∑ x_1 ∈ DFinsupp.support ((decompose 𝒜) x), (map (↑f).gradedAddHom) ((decompose 𝒜) ↑(((decompose 𝒜) x) x_1))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ val (↑(sectionInBasicOpen 𝒜 x f) ((homOfLE ⋯ ≫ homOfLE ⋯).op.unop ⟨t, ⋯⟩)) =
    val (↑(sectionInBasicOpen 𝒜 x g) ((homOfLE ⋯ ≫ homOfLE ⋯).op.unop ⟨t, ⋯⟩))

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ val (↑(sectionInBasicOpen 𝒜 x f) ((homOfLE ⋯ ≫ homOfLE ⋯).op.unop ⟨t, ⋯⟩)) =
    val (↑(sectionInBasicOpen 𝒜 x g) ((homOfLE ⋯ ≫ homOfLE ⋯).op.unop ⟨t, ⋯⟩))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
c : A
hc : c ∈ x.asHomogeneousIdeal.toIdeal.primeCompl
hc' : ↑⟨c, hc⟩ * (↑g.den * ↑f.num) = ↑⟨c, hc⟩ * (↑f.den * ↑g.num)
t : ↑(ProjectiveSpectrum.top 𝒜)
ht' : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 c)
htf : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑f.den)
htg : t ∈ ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑g.den)
⊢ (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑⟨c, hc⟩ * (↑f.den * ↑g.num)) =
    (algebraMap A (Localization t.asHomogeneousIdeal.toIdeal.primeCompl)) (↑⟨c, ht'⟩ * (↑f.den * ↑g.num))

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ (ConcreteCategory.hom
        ((Proj.structureSheaf 𝒜).presheaf.germ
          (ProjectiveSpectrum.basicOpen 𝒜 ↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den) x ⋯))
      (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
⊢ (ConcreteCategory.hom
        ((Proj.structureSheaf 𝒜).presheaf.germ
          (ProjectiveSpectrum.basicOpen 𝒜 ↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den) x ⋯))
      (sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
t : ↑(ProjectiveSpectrum.top 𝒜)
ht : t ∈ unop (op V)
⊢ HomogeneousLocalization.val
      (↑(sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) ((homOfLE ⋯).op.unop ⟨t, ht⟩)) =
    HomogeneousLocalization.val (↑s (i.op.unop ⟨t, ht⟩))

Tactic:
]

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
V : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxV : ↑⟨x, hxU⟩ ∈ V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), ↑b ∉ (↑x).asHomogeneousIdeal
e :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a_1 ∈ V),
    ↑s ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
t : ↑(ProjectiveSpectrum.top 𝒜)
ht : t ∈ unop (op V)
⊢ HomogeneousLocalization.val
      (↑(sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) ((homOfLE ⋯).op.unop ⟨t, ht⟩)) =
    HomogeneousLocalization.val (↑s (i.op.unop ⟨t, ht⟩))
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑⟨fun y ↦ HomogeneousLocalization.mk { deg := z.deg, num := z.num, den := z.den, den_mem := ⋯ }, ⋯⟩ ⟨x, ⋯⟩ =
    Quotient.mk'' z

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
rid₁ : x✝ ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
x : A
hx : x ∉ I
⊢ ∃ a ∈ DFinsupp.support ((decompose 𝒜) x), (proj 𝒜 a) x ∉ I

Tactic:
]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
rid₁ : x✝ ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
x : A
hx : x ∉ I
⊢ ∃ a ∈ DFinsupp.support ((decompose 𝒜) x), (proj 𝒜 a) x ∉ I
Module: Mathlib.RingTheory.GradedAlgebra.Radical

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
rid₁ : x✝ ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
x : A
hx : ∀ a ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) a) ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ I

Tactic:
]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : LinearOrder ι
inst✝³ : IsOrderedCancelAddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
hI : IsHomogeneous 𝒜 I
I_ne_top : I ≠ ⊤
homogeneous_mem_or_mem : ∀ {x y : A}, IsHomogeneousElem 𝒜 x → IsHomogeneousElem 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
x✝ y : A
hxy : x✝ * y ∈ I
rid₁ : x✝ ∉ I
rid₂ : y ∉ I
set₁ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₁_eq : set₁ = {i ∈ DFinsupp.support ((decompose 𝒜) x✝) | (proj 𝒜 i) x✝ ∉ I}
set₂ : Finset ι := {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
set₂_eq : set₂ = {i ∈ DFinsupp.support ((decompose 𝒜) y) | (proj 𝒜 i) y ∉ I}
x : A
hx : ∀ a ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) a) ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ I