mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x✝ : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x✝ ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x✝ ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := ⋯
this✝² : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝¹ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := ⋯
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := ⋯
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this✝ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
e : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↑Γ(X, f ⁻¹ᵁ U) ≃ₐ[↑Γ(Y, V)] ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) := ⋯
ψ : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)) →ₐ[↑Γ(Y, V)]
  ↥(integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) := ⋯
hψ : Function.Bijective ⇑ψ
φ : pushout (app (fromNormalization f) U) (appLE g U V hVU) ⟶
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W) := ⋯
this : Mono (CommRingCat.ofHom (integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)).val.toRingHom)
H : pullback.snd f g ⁻¹ᵁ V ≤ pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U
x : ↑(CommRingCat.of ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)))
⊢ (ConcreteCategory.hom (CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ e₀.hom)) ↑x =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          ((integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)).val.comp
            ((↑(RingEquiv.ofBijective (↑ψ) hψ)).comp ↑Algebra.TensorProduct.includeRight))))
      x

Tactic:
simp [ψ, toIntegralClosure, e]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ IsIso (toNormalization (pullback.snd f fT) ∣_ e.hom ⁻¹ᵁ opensRange ι)

Tactic:
rw [← isIso_comp_right_iff _ (e.hom ∣_ ι.opensRange),
      ← morphismRestrict_comp, ← isIso_comp_right_iff _ ι.isoOpensRange.inv]

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
hVW' : ↑W = (↑V)ᶜ
this✝ : IsClosedImmersion V.ι
this : IsClosedImmersion W.ι
H : IsColimit (BinaryCofan.mk V.ι W.ι)
e : normalization (pullback.snd f fT) ≅ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) :=
  (normalizationCoprodIso (pullback.snd f fT) H).symm ≪≫
    coprod.mapIso (asIso (toNormalization (V.ι ≫ pullback.snd f fT))).symm
      (Iso.refl (normalization (W.ι ≫ pullback.snd f fT)))
ι : ↑V ⟶ ↑V ⨿ normalization (W.ι ≫ pullback.snd f fT) := coprod.inl
⊢ IsIso ((toNormalization (pullback.snd f fT) ≫ e.hom) ∣_ opensRange ι ≫ (isoOpensRange ι).inv)
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
x : ↥X
hx : QuasiFiniteAt f x
T : Scheme
fT : T ⟶ Y
left✝¹ : Etale fT
u : ↥T
hu : fT u = f x
V W : (pullback f fT).Opens
v : ↥V
hVW : IsCompl V W
left✝ : IsFinite (V.ι ≫ pullback.snd f fT)
hv₂ : (pullback.fst f fT) ↑v = x
U : (normalization (pullback.snd f fT)).Opens
hU : (toNormalization (pullback.snd f fT)) ↑v ∈ U
right✝ : IsIso (toNormalization (pullback.snd f fT) ∣_ U)
fTn : normalization (pullback.snd f fT) ⟶ normalization f :=
  normalizationPullback f fT ≫ pullback.fst (fromNormalization f) fT
U' : (normalization f).Opens := { carrier := ⇑fTn '' U.carrier, is_open' := ⋯ }
fTnU : ↑U ⟶ ↑U' := resLE fTn U' U ⋯
this : Surjective fTnU
H : toNormalization (pullback.snd f fT) ⁻¹ᵁ U ≤ pullback.fst f fT ⁻¹ᵁ toNormalization f ⁻¹ᵁ U'
⊢ toNormalization (pullback.snd f fT) ∣_ U ≫ fTnU =
    resLE (pullback.fst f fT) (toNormalization f ⁻¹ᵁ U') (toNormalization (pullback.snd f fT) ⁻¹ᵁ U) H ≫
      toNormalization f ∣_ U'

Tactic:
simp [← cancel_mono U'.ι, fTnU, fTn]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsSeparated f
inst✝ : QuasiCompact f
V : { x // QuasiFiniteAt f x } → (normalization f).Opens
hxV : ∀ (x : { x // QuasiFiniteAt f x }), (toNormalization f) ↑x ∈ V x
hV : ∀ (x : { x // QuasiFiniteAt f x }), IsIso (toNormalization f ∣_ V x)
𝒰 : (↑(⨆ i, V i)).OpenCover := Opens.iSupOpenCover V
x : 𝒰.toPreZeroHypercover.1
⊢ (⨆ i, V i).ι ''ᵁ opensRange (𝒰.f x) = V x

Tactic:
simp only [Opens.iSupOpenCover, 𝒰, ← opensRange_comp, homOfLE_ι, Opens.opensRange_ι]

Goal state after:
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: case zero
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
⊢ ∃ b m,
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom b =
      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ m * 0

Tactic:
use 0

Goal state after:
case h
R : Type u_2
S : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : FiniteType R S
inst✝⁷ : CommRing R'
inst✝⁶ : Algebra R R'
inst✝⁵ : CommRing R''
inst✝⁴ : Algebra R R''
inst✝³ : Algebra R'' S
inst✝² : Algebra.IsIntegral R R''
inst✝¹ : IsScalarTower R R'' S
q : Ideal S
P : Ideal R'
inst✝ : P.IsPrime
e : R' ⊗[R] S
e₀ : R' ⊗[R] R''
he₀ : IsIdempotentElem e₀
he₀e : (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)) e₀ = e
P' : Ideal (R' ⊗[R] S)
hP'q : Ideal.comap TensorProduct.includeRight.toRingHom P' = q
H :
  ∀ (P'' : Ideal (R' ⊗[R] R'')),
    P''.IsPrime →
      P''.LiesOver P →
        e₀ ∉ P'' → P'' = Ideal.comap (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom P'
g : R''
hgq : (algebraMap R'' S) g ∉ q
hg : Function.Surjective ⇑(Localization.awayMap (algebraMap R'' S) g)
this : Algebra.IsIntegral R' (Localization.Away e₀)
⊢ ∃ m,
    (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom 0 =
      (TensorProduct.map (AlgHom.id R' R') (IsScalarTower.toAlgHom R R'' S)).toRingHom (e₀ * 1 ⊗ₜ[R] g) ^ m * 0
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).FinitePresentation
⊢ (algebraMap R T).FinitePresentation

Tactic:
finitePresentation_algebraMap

Goal state after:
R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.FinitePresentation S (S ⊗[R] T)
⊢ Algebra.FinitePresentation R T
Module: Mathlib.AlgebraicGeometry.Group.Affine

Goal state before:
pp: R✝¹ R✝ A : CommRingCat
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Bialgebra R S
inst✝ : Algebra R T
f :
  (Spec (CommRingCat.of T)).asOver (Spec (CommRingCat.of R)) ⟶
    (Spec (CommRingCat.of S)).asOver (Spec (CommRingCat.of R))
⊢ ∀ (r : R), (↑↑(CommRingCat.Hom.hom (preimage (Over.Hom.left f)))).toFun ((algebraMap R S) r) = (algebraMap R T) r

Tactic:
suffices CommRingCat.ofHom (algebraMap R S) ≫ Spec.preimage f.left =
      CommRingCat.ofHom (algebraMap R T) from fun r ↦ congr($this r)
    apply Spec.map_injective
    simpa [-comp_over] using! f.w

Goal state after:
Module: Mathlib.Topology.Sheaves.Over

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
x : X
⊢ x ∈ ↑V.left ↔ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑V.left

Tactic:
simp only [SetLike.mem_coe, Set.mem_image, Set.mem_preimage,
      Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right, iff_self_and]

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
U : Opens X
A : Type u_1
inst✝ : Category.{v_1, u_1} A
V : Over U
x : X
⊢ x ∈ V.left → x ∈ U
Module: Mathlib.RingTheory.Etale.QuasiFinite

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsPrime
⊢ ∃ R' x x_1,
    ∃ (_ : Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (R' ⊗[R] S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i

Tactic:
have ⟨R', _, _, _, P, _, _, n, e, he, P', _, _, hP, hP', H⟩ :=
    exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq' (S := ULift.{u} S) p
  let e₁ : R' ⊗[R] S ≃ₐ[R'] R' ⊗[R] ULift.{u} S :=
    Algebra.TensorProduct.congr .refl ULift.algEquiv.symm
  refine ⟨R', _, _, ‹_›, P, ‹_›, ‹_›, n, e₁.symm ∘ e, he.map _,
    fun i ↦ (P' i).comap e₁.toAlgHom, inferInstance, inferInstance, hP, by simpa,
    fun P'' _ _ ↦ ?_⟩
  have := H (P''.comap e₁.symm.toAlgHom) inferInstance inferInstance
  refine ⟨by simpa using this.1, fun i hi ↦ ?_⟩
  simp [← this.2 i (by simpa), Ideal.comap_comapₐ]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.ModuleFinitePresentation

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
this : Submodule.span R ↑s ≤ f.toLinearMap.range
⊢ Function.Surjective ⇑f

Tactic:
hs,

Goal state after:
R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.Finite R S
s : Finset S
hs : Submodule.span R ↑s = ⊤
S' : Type u
w✝⁴ : CommRing S'
w✝³ : Algebra R S'
w✝² : Module.Finite R S'
w✝¹ : Free R S'
w✝ : Algebra.FinitePresentation R S'
f : S' →ₐ[R] S
hsf : ↑s ⊆ ↑f.range
this : ⊤ ≤ f.toLinearMap.range
⊢ Function.Surjective ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ finrank (Spec.map (𝟙 R)) y = 1 (g y)

Tactic:
finrank_SpecMap_eq_finrank,

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).finrank y = 1 (g y)

case hf₁
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

case hf₂
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w✝ : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial ↑R
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ ord R ϖ = 1

Tactic:
rw [Ring.ord, Module.length_eq_one_iff]
  have : (Ideal.span {ϖ}).IsMaximal :=
    PrincipalIdealRing.isMaximal_of_irreducible hϖ
  rw [isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective (S := R ⧸ Ideal.span {ϖ})
    Ideal.Quotient.mk_surjective]
  let := Ideal.Quotient.field (Ideal.span {ϖ})
  exact instIsSimpleModule _

Goal state after:
Module: Mathlib.RingTheory.OrderOfVanishing.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ IsNoetherian R (R ⧸ span {x}) ∧ IsArtinian R (R ⧸ span {x})

Tactic:
suffices IsArtinianRing (R ⧸ Ideal.span {x}) from
    ⟨isNoetherian_quotient (Ideal.span {x}),
      isArtinian_of_surjective_algebraMap (Ideal.Quotient.mk_surjective (I := .span {x}))⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : KrullDimLE 1 R
x : R
hx : x ∈ nonZeroDivisors R
⊢ IsArtinianRing (R ⧸ span {x})
Module: Mathlib.RingTheory.OrderOfVanishing.Noetherian

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : IsNoetherianRing R
inst✝⁷ : KrullDimLE 1 R
K : Type u_2
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : Algebra S K
inst✝ : IsScalarTower S R K
a : S
ha : (algebraMap S R) a ≠ 0
f : K
j : ¬f = 0
this : (ordFrac R) f ≤ (ordFrac R) ((algebraMap S K) a • f)
⊢ (ordFrac R) f ≤ (ordFrac R) (a • f)

Tactic:
by simp_all only [ne_eq,
    algebraMap_smul]

Goal state after:
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 𝒜
s : Set (Set A)
⊢ zeroLocus 𝒜 (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus 𝒜 s'

Tactic:
simp only [zeroLocus_iUnion]

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

Goal state before:
pp: case inr
ι : 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
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}
nonempty : ∀ x ∉ I, {i ∈ DFinsupp.support ((decompose 𝒜) x) | (proj 𝒜 i) x ∉ I}.Nonempty
max₁ : ι := set₁.max' ⋯
max₂ : ι := set₂.max' ⋯
mem_max₁ : max₁ ∈ set₁
mem_max₂ : max₂ ∈ set₂
hxy : (proj 𝒜 (max₁ + max₂)) (x * y) ∈ I
antidiag : Finset (ι × ι) :=
  {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
ha : antidiag = {z ∈ DFinsupp.support ((decompose 𝒜) x) ×ˢ DFinsupp.support ((decompose 𝒜) y) | z.1 + z.2 = max₁ + max₂}
mem_antidiag : (max₁, max₂) ∈ antidiag
eq_add_sum :
  (proj 𝒜 (max₁ + max₂)) (x * y) =
    (proj 𝒜 max₁) x * (proj 𝒜 max₂) y + ∑ ij ∈ antidiag.erase (max₁, max₂), (proj 𝒜 ij.1) x * (proj 𝒜 ij.2) y
i j : ι
H₁ : ¬(i = max₁ ∧ j = max₂)
H₄ : i + j = max₁ + max₂
H₂ : i ∈ DFinsupp.support ((decompose 𝒜) x)
H₃ : j ∈ DFinsupp.support ((decompose 𝒜) y)
max_lt : max₂ < j
notMem : j ∈ DFinsupp.support ((decompose 𝒜) y) → (proj 𝒜 j) y ∈ I
⊢ (proj 𝒜 (i, j).1) x * (proj 𝒜 (i, j).2) y ∈ I

Tactic:
exact Ideal.mul_mem_left I _ (notMem H₃)

Goal state after:
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✝ : NegMemClass σ A
𝒜 : ι → σ
x : Submonoid A
c1 c2 : NumDenSameDeg 𝒜 x
h : Localization.mk ↑c1.num ⟨↑c1.den, ⋯⟩ = Localization.mk ↑c2.num ⟨↑c2.den, ⋯⟩
⊢ (Setoid.ker (embedding 𝒜 x)) (-c1) (-c2)

Tactic:
change Localization.mk _ _ = Localization.mk _ _
    simp only [num_neg, den_neg, ← Localization.neg_mk]
    exact congr_arg Neg.neg h

Goal state after:
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 𝒜
⊢ TopologicalSpace.Opens.IsBasis (Set.range (basicOpen 𝒜))

Tactic:
delta TopologicalSpace.Opens.IsBasis

Goal state after:
σ : Type u_1
A : Type u
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range (basicOpen 𝒜))
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
⊢ mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x ↦ f ^ x) j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
have : DirectSum.decompose 𝒜 a n = ⟨a, ha⟩ := Subtype.ext (DirectSum.decompose_of_mem_same 𝒜 ha)

Goal state after:
case neg
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
this : ((decompose 𝒜) a) n = ⟨a, ha⟩
⊢ mk { deg := n, num := ⟨a, ha⟩, den := ⟨(fun x ↦ f ^ x) j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = 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
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ¬∑ i, ai i • dv i = n
⊢ ↑(((decompose 𝒜) (∏ i, v i ^ ai i)) n) = 0

Tactic:
refine DirectSum.decompose_of_mem_ne _ ?_ H

Goal state after:
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
ai : ι' → ℕ
H : ¬∑ i, ai i • dv i = n
⊢ ∏ i, v i ^ ai i ∈ 𝒜 (∑ i, ai i • dv i)
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case neg.mem
ι : Type u_1
A : Type u_2
σ : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubgroupClass σ A
inst✝³ : AddCommMonoid ι
inst✝² : DecidableEq ι
𝒜 : ι → σ
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)
HH : ¬Subsingleton (Away 𝒜 f)
n : ι
a✝ : A
j : ℕ
hb' : (fun x ↦ f ^ x) j ∈ 𝒜 n
hfj : ¬f ^ j = 0
a : A
ha' : a ∈ ↑(Submonoid.closure (Set.range v))
⊢ mk { deg := n, num := ((decompose 𝒜) a) n, den := ⟨f ^ j, hb'⟩, den_mem := ⋯ } ∈
    Submodule.span ↥(𝒜 0) {x | ∃ a ai, ∃ (hai : ∑ i, ai i • dv i = a • d), Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x}

Tactic:
obtain ⟨ai, rfl⟩ := Submonoid.exists_of_mem_closure_range _ _ ha'
    clear ha'
    by_cases H : ∑ i, ai i • dv i = n
    · apply Submodule.subset_span
      refine ⟨j, ai, H.trans ?_, ?_⟩
      · exact DirectSum.degree_eq_of_mem_mem 𝒜 hb'
          (SetLike.pow_mem_graded j hf) hfj
      · ext
        simp only [val_mk, Away.val_mk]
        congr
        refine (DirectSum.decompose_of_mem_same _ ?_).symm
        exact H ▸ SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
    · convert! zero_mem (Submodule.span (𝒜 0) _)
      ext
      have : (DirectSum.decompose 𝒜 (∏ i : ι', v i ^ ai i) n).1 = 0 := by
        refine DirectSum.decompose_of_mem_ne _ ?_ H
        exact SetLike.prod_pow_mem_graded _ _ _ _ fun i _ ↦ hxd i
      simp [this, Localization.mk_zero]

Goal state after:
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
⊢ Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (X.basicOpen (f r)) ⋯ =
    (X.isoOfEq ⋯).inv ≫ fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r

Tactic:
← Scheme.Hom.resLE_eq_morphismRestrict

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
⊢ Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (X.basicOpen (f r)) ⋯ =
    (X.isoOfEq ⋯).inv ≫
      Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (fromOfGlobalSections 𝒜 f hf ⁻¹ᵁ basicOpen 𝒜 r) ⋯