mathlib-initiative/mathlib-tactics huggingface dataset:
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 𝒜
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s ↦ zeroLocus 𝒜 s) fun t ↦ ↑(vanishingIdeal t)

Tactic:
simpa using

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s ↦ zeroLocus 𝒜 s) fun t ↦ ↑(vanishingIdeal t)
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 g : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f * g} ↔ x ∈ zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}

Tactic:
simpa using

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f g : A
x : ProjectiveSpectrum 𝒜
⊢ f * g ∈ x.asHomogeneousIdeal ↔ f ∈ x.asHomogeneousIdeal ∨ g ∈ x.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
n : ℕ
hn : 0 < n
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 {f ^ n} ↔ x ∈ zeroLocus 𝒜 {f}

Tactic:
simpa using

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
n : ℕ
hn : 0 < n
x : ProjectiveSpectrum 𝒜
⊢ f ^ n ∈ x.asHomogeneousIdeal ↔ f ∈ x.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
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen 𝒜 (f ^ n)) = ↑(basicOpen 𝒜 f)

Tactic:
simpa using

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
n : ℕ
hn : 0 < n
⊢ zeroLocus 𝒜 {f ^ n} = 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)
⊢ ∀ i ∈ Finset.image x Finset.univ, SetLike.IsHomogeneousElem 𝒜 i

Tactic:
simpa using

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)
⊢ ∀ (a : ι₀), SetLike.IsHomogeneousElem 𝒜 (x a)
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
n : ι
hn : n ∈ DFinsupp.support ((DirectSum.decompose 𝒜) s)
⊢ ↑(((DirectSum.decompose 𝒜) s) n) ∈ ↑(Finset.image x Finset.univ)

Tactic:
simpa using

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
n : ι
hn : n ∈ DFinsupp.support ((DirectSum.decompose 𝒜) s)
⊢ ∃ y, x y = ↑(((DirectSum.decompose 𝒜) s) n)
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)
⊢ ∀ i ∈ {x ∈ s | n x ≠ 0}, ∃ n, n ≠ 0 ∧ i ∈ 𝒜 n

Tactic:
simpa using

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)
⊢ ∀ i ∈ s, ¬n i = 0 → ∃ n, ¬n = 0 ∧ i ∈ 𝒜 n
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)
i : S
hi : i ∈ ↑s
hi0 : ¬n i = 0
⊢ i ∈ ↑({x ∈ s | n x ≠ 0})

Tactic:
simpa using

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)
i : S
hi : i ∈ ↑s
hi0 : ¬n i = 0
⊢ i ∈ s
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case succ
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
ih : ↑(GradedMonoid.GMonoid.gnpow n c.den) ∈ x
⊢ ↑(GradedMonoid.GMonoid.gnpow (n + 1) c.den) ∈ x

Tactic:
simpa using

Goal state after:
case succ
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
c : NumDenSameDeg 𝒜 x
n : ℕ
ih : ↑(GradedMonoid.GMonoid.gnpow n c.den) ∈ x
⊢ ↑c.den ^ n * ↑c.den ∈ x
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
a : AtPrime 𝒜 𝔭
⊢ IsUnit a ∨ IsUnit (1 - a)

Tactic:
simpa using

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
𝒜 : ι → σ
x : Submonoid A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
inst✝¹ : GradedRing 𝒜
𝔭 : Ideal A
inst✝ : 𝔭.IsPrime
a : AtPrime 𝒜 𝔭
⊢ IsUnit (val a) ∨ IsUnit (1 - val a)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
c : ℕ
hc : c = 0
⊢ c ∉ DFinsupp.support ((DirectSum.decompose 𝒜) x)

Tactic:
simpa using

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x : A
hx : x ∈ (HomogeneousIdeal.irrelevant 𝒜).toIdeal
c : ℕ
hc : c = 0
⊢ ((DirectSum.decompose 𝒜) x) 0 = 0
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
  ↑(X.basicOpen (f (x.snd.fst * y.snd.fst))) := ⋯
⊢ e.inv ≫
      pullback.fst ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
        toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 x.snd.fst).ι =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 (x.snd.fst * y.snd.fst)).ι

Tactic:
simpa using

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
  ↑(X.basicOpen (f (x.snd.fst * y.snd.fst))) :=
  ⋯.isoPullback.symm ≪≫ X.isoOfEq ⋯
⊢ X.homOfLE ⋯ ≫ toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 x.snd.fst).ι =
    toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 (x.snd.fst * y.snd.fst)).ι
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
  ↑(X.basicOpen (f (x.snd.fst * y.snd.fst))) := ⋯
⊢ toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 (x.snd.fst * y.snd.fst)).ι =
    e.inv ≫
      pullback.snd ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≫
        toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 y.snd.fst).ι

Tactic:
simpa using

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f✝ : A →+* ↑Γ(X, ⊤)
x✝ x' : ↑Γ(X, ⊤)
t t' : A
d d' : ℕ
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
x y : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
e : pullback ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x) ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f y) ≅
  ↑(X.basicOpen (f (x.snd.fst * y.snd.fst))) :=
  ⋯.isoPullback.symm ≪≫ X.isoOfEq ⋯
⊢ toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 (x.snd.fst * y.snd.fst)).ι =
    X.homOfLE ⋯ ≫ toBasicOpenOfGlobalSections 𝒜 f ⋯ ⋯ ⋯ ≫ (basicOpen 𝒜 y.snd.fst).ι
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (TopCat.Hom.hom
        (Spec.map
            (CommRingCat.ofHom
              ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base)
      ((TopCat.Hom.hom (basicOpenIsoSpecAway (f i.snd.fst)).hom.base)
        ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
          ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x))) ∈
    ⇑(TopCat.Hom.hom (awayι 𝒜 i.snd.fst ⋯ ⋯).base) ⁻¹' ↑(basicOpen 𝒜 r)
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
← TopologicalSpace.Opens.map_coe,

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (TopCat.Hom.hom
        (Spec.map
            (CommRingCat.ofHom
              ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base)
      ((TopCat.Hom.hom (basicOpenIsoSpecAway (f i.snd.fst)).hom.base)
        ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
          ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x))) ∈
    ↑((TopologicalSpace.Opens.map (awayι 𝒜 i.snd.fst ⋯ ⋯).base).obj (basicOpen 𝒜 r))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (TopCat.Hom.hom (basicOpenIsoSpecAway (f i.snd.fst)).hom.base)
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ⇑(TopCat.Hom.hom
          (Spec.map
              (CommRingCat.ofHom
                ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                  (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base) ⁻¹'
      ↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)

Tactic:
← TopologicalSpace.Opens.map_coe,

Goal state after:
case a
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
i : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀
x : ↥((openCoverOfMapIrrelevantEqTop 𝒜 f hf).X i)
hx :
  (TopCat.Hom.hom (basicOpenIsoSpecAway (f i.snd.fst)).hom.base)
      ((↑(PrimeSpectrum.basicOpen (f i.snd.fst))).restrictPreimage (⇑X.toSpecΓ)
        ((TopCat.Hom.hom ((TopologicalSpace.Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE ⋯))) x)) ∈
    ↑((TopologicalSpace.Opens.map
            (Spec.map
                (CommRingCat.ofHom
                  ((IsLocalization.map (Localization.Away (f i.snd.fst)) f ⋯).comp
                    (algebraMap (Away 𝒜 i.snd.fst) (Localization.Away i.snd.fst))))).base).obj
        (PrimeSpectrum.basicOpen (Away.isLocalizationElem ⋯ hr)))
⊢ ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f i) x ∈ X.basicOpen (f r)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
x : ↥X
hx : x ∈ X.basicOpen (f r)
I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, ⟨r, ⋯⟩⟩
⊢ x ∈ Scheme.Hom.opensRange ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f I)

Tactic:
simpa using

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
r : A
n : ℕ
hn : 0 < n
hr : r ∈ 𝒜 n
x : ↥X
hx : x ∈ X.basicOpen (f r)
I : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀ := ⟨n, ⟨r, ⋯⟩⟩
⊢ x ∈ X.basicOpen (f I.snd.fst)
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Goal state before:
pp: σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
X : Scheme
f : A →+* ↑Γ(X, ⊤)
hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤
⊢ fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜 = X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A)))

Tactic:
by
  refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).hom_ext _ _ fun x ↦ ?_
  simp only [fromOfGlobalSections, toBasicOpenOfGlobalSections, CommRingCat.ofHom_comp,
    Category.assoc, Scheme.Cover.ι_glueMorphisms_assoc, basicOpenIsoSpec_inv_ι_assoc,
    awayι_toSpecZero, Iso.inv_comp_eq]
  simp only [openCoverOfMapIrrelevantEqTop,
    Scheme.openCoverOfIsOpenCover_f, Scheme.isoOfEq_hom_ι_assoc, ← morphismRestrict_ι_assoc]
  congr 1
  simp only [basicOpenIsoSpecAway, ← CommRingCat.ofHom_comp, ← Spec.map_comp, ← Iso.eq_inv_comp,
    IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, ← HomogeneousLocalization.algebraMap_eq]
  congr 2
  rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ A,
    ← RingHom.comp_assoc, IsLocalization.map_comp, RingHom.comp_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ ∃ n, unop f ∣ unop g ^ n

Tactic:
simpa using

Goal state after:
R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec (CommRingCat.of ↑R)).Modules
f g : (↑R)ᵒᵖ
i : f ⟶ g
N : ModuleCat ↑(CommRingCat.of ↑R) := (modulesSpecToSheaf.obj M).presheaf.obj (op ⊤)
⊢ ∃ n, unop f ∣ unop g ^ n
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
hd : d = 0
⊢ ∀ (x : ι'), ai x = 0

Tactic:
simpa using

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
hxd' : ∀ (i : ι'), 0 < dv i
a : ℕ
ai : ι' → ℕ
hai : ∑ i, ai i • dv i = a • d
H₀ : (a - ∑ i, dv i * (ai i / d)) • d = ∑ k, (ai k % d) • dv k
H :
  Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ =
    Away.mk 𝒜 hf (a - ∑ i, dv i * (ai i / d)) (∏ i, v i ^ (ai i % d)) ⋯ * ∏ i, isLocalizationElem hf ⋯ ^ (ai i / d)
hd : d = 0
⊢ ∀ (x : ι'), ai x = 0
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : ModuleCat ↑R
s : Set ↑M
hs : Submodule.span (↑R) s = ⊤
t : Set (↑s →₀ ↑R)
ht : Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker
H₁ :
  Function.Exact ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
    ⇑(ConcreteCategory.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))
⊢ Function.Surjective ⇑(ModuleCat.Hom.hom (ModuleCat.ofHom (Finsupp.linearCombination (↑R) Subtype.val)))

Tactic:
by simp [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hs]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.LocalSubring

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
⊢ ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) x s) =
    (IsLocalization.liftAlgHom ⋯) (IsLocalization.mk' (Localization.AtPrime P) y t)
H : ∀ (x : ↥P.primeCompl), ↑x ≠ 0
⊢ ↑x = ↑y * (↑↑t)⁻¹ * ↑↑s
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
s : Finset ι' := {x | 0 < dv x}
i : ι'
hi : dv i > 0
⊢ i ∈ s

Tactic:
simpa using

Goal state after:
A : Type u_2
σ : Type u_3
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
f : A
d : ℕ
hf : f ∈ 𝒜 d
ι' : Type u_4
inst✝ : Fintype ι'
v : ι' → A
hx : Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤
dv : ι' → ℕ
hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)
s : Finset ι' := {x | 0 < dv x}
i : ι'
hi : dv i > 0
⊢ 0 < dv i
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: case refine_2
R : CommRingCat
M : (Spec R).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsIso ((modulesSpecToSheaf.obj M).obj.map (homOfLE ⋯).op)

Tactic:
simpa using

Goal state after:
case refine_2
R : CommRingCat
M : (Spec R).Modules
h : IsLocalizing (modulesSpecToSheaf.obj M)
⊢ IsIso (𝟙 ((modulesSpecToSheaf.obj M).obj.obj (op ⊤)))