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

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ (fun x ↦ x.ideal ⟨⊤, ⋯⟩) (ofIdealTop I) = I

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
inst✝ : IsAffine X
⊢ ∀ (x y : X.IdealSheafData), (x * y).ideal ⟨⊤, ⋯⟩ = x.ideal ⟨⊤, ⋯⟩ * y.ideal ⟨⊤, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
inst✝ : IsAffine X
⊢ ∀ (x y : X.IdealSheafData), (x + y).ideal ⟨⊤, ⋯⟩ = x.ideal ⟨⊤, ⋯⟩ + y.ideal ⟨⊤, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsIso (Spec.map f) ↔ Function.Bijective ⇑(CommRingCat.Hom.hom f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hx : x ∈ ↑U
⊢ x ∈ I.supportSet ↔ x ∈ X.zeroLocus ↑(I.ideal U).radical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I ⊓ J).radical = I.radical ⊓ J.radical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueDataObjι U) = ⇑(IsAffineOpen.isoSpec ⋯).inv '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueDataObjι U ≫ (↑U).ι) = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
F : Γ(X, ↑U) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x : ↑Γ(X, ↑U)
hx : x ∈ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)
this :
  ∀ (p : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))), (IsAffineOpen.fromSpec ⋯) p ∈ Z → (CommRingCat.Hom.hom F) x ∈ p.asIdeal
⊢ x ∈
    Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
⊢ IsLocalization.Away f ↑Γ(X, ↑U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
⊢ IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f) (↑Γ(X, ↑U) ⧸ I.ideal U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
U✝ V : X✝.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
⊢ IsPreimmersion (hU.fromSpecStalk hx)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hxU : x ∈ U
⊢ (hU.fromSpecStalk hxU) (closedPoint ↑(X.presheaf.stalk x)) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
⊢ I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f ≤ Hom.opensRange (I.glueDataObjMap ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Hom.app (X.fromSpecStalk x) U =
    X.presheaf.germ U x hxU ≫
      (ΓSpecIso (X.presheaf.stalk x)).inv ≫ (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x y : ↥X
h : x ⤳ y
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this✝ :
  ∀ {X Y : Scheme} {f : X ⟶ Y},
    P f →
      ∀ (x : ↥X),
        IsAffine X → IsAffine Y → (∃ R S, Y = Spec R ∧ X = Spec S) → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ R S, Y = Spec R ∧ X = Spec S
this : Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x))))
⊢ X.isoSpec.inv (X.isoSpec.hom x) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
p : ↥(I.glueDataObj U)
hp : p ∈ Opposite.unop (Opposite.op (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V))
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hf : ↑((I.glueDataObjι U) p) ∈ X.basicOpen f
this : IsIso (Hom.app (I.glueDataObjMap ⋯) (I.glueDataObjι U ⁻¹ᵁ (↑U).ι ⁻¹ᵁ X.basicOpen f))
⊢ (X.homOfLE ⋯ ≫ (↑U).ι) ⁻¹ᵁ ↑V = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) =
    PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ ↑Z ↔ x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ Z ≤ I.support ↔ I ≤ vanishingIdeal Z

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ vanishingIdeal I.support = I.radical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ vanishingIdeal ⊤ = X.nilradical

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
⊢ X.nilradical = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
I : X.IdealSheafData
⊢ I.support = ⊤ ↔ I = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f → ∀ (J : Ideal S) (x : J.IsPrime), Q' (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n✝ : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n✝, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
n : ℕ
hn : (ConcreteCategory.hom (f.app ↑U)) s ^ n * (ConcreteCategory.hom (f.app ↑U)) x = 0
⊢ (fun x ↦ s ^ x) n * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Set.range ⇑(X.fromSpecStalk x) = {y | y ⤳ x}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this✝ : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
this :
  ∃ V, ∃ (hV : V = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)), ((CommRingCat.Hom.hom (f.app ↑U)) x |_ V) ⋯ = 0
⊢ ∃ s_1 ∈ Submonoid.powers s, s_1 * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ f ⁻¹ᵁ Y.basicOpen s = X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ P = P'

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.ideal V ≤ RingHom.ker (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
⊢ X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
x : ↥U
f : ↑(X.presheaf.obj (op U))
⊢ (ConcreteCategory.hom (X.evaluation x)) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑X.toTopCat
f : ↑(X.presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : ↥U), (ConcreteCategory.hom (X.evaluation x)) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Y.residue ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x = Hom.stalkMap f x ≫ X.residue x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : ↑X.toTopCat
⊢ residueFieldMap (f ≫ g) x = residueFieldMap g ((ConcreteCategory.hom f.base) x) ≫ residueFieldMap f x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
⊢ Y.evaluation ⟨(ConcreteCategory.hom f.base) ↑x, ⋯⟩ ≫ residueFieldMap f ↑x = f.c.app (op V) ≫ X.evaluation x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial =
    X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U) ⟨x, hxU⟩ hxU

Tactic:
← Functor.map_comp_assoc

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ (↑U).presheaf.germ ⊤ ⟨x, hxU⟩ trivial =
    X.presheaf.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U) ⟨x, hxU⟩ hxU
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (ConcreteCategory.hom (residueFieldMap f ↑x))
      ((ConcreteCategory.hom (Y.evaluation ⟨(ConcreteCategory.hom f.base) ↑x, ⋯⟩)) a) =
    (ConcreteCategory.hom (X.evaluation x)) ((ConcreteCategory.hom (f.c.app (op V))) a)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ (Opens.map f.base).obj ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ (Opens.map f.base).obj ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
⊢ (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x✝¹ : ↑Γ(X, ↑V)
hx : x✝¹ ∈ I.ideal V
x : ↥(pullback (I.glueDataObjι U) (X.homOfLE ⋯))
x✝ : x ∈ ⊤
⊢ x ∈ (F ≫ (↑U ⊓ ↑V).ι) ⁻¹ᵁ ↑V

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯) ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (stalkClosedPointIso R).inv = StructureSheaf.toStalk (↑R) (closedPoint ↑R)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
⊢ RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s))) ≤
    Ideal.map (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) (RingHom.ker (CommRingCat.Hom.hom (f.app ↑U)))

Tactic:
intro x hx
    have := U.2.isLocalization_basicOpen s
    obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x
    refine (IsLocalization.mk'_mem_map_algebraMap_iff _ _ _ _ _).mpr ?_
    suffices ∃ (V : X.Opens) (hV : V = X.basicOpen ((f.app U).hom s)),
        letI := hV.trans_le (X.basicOpen_le _); ((f.app U).hom x |_ V) = 0 by
      obtain ⟨_, rfl, H⟩ := this
      obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
        X (U := f ⁻¹ᵁ U) (QuasiCompact.isCompact_preimage (f := f) _ U.1.2 U.2.isCompact)
        (f.app U x) (f.app U s) H
      exact ⟨_, ⟨n, rfl⟩, by simpa using hn⟩
    refine ⟨f ⁻¹ᵁ Y.basicOpen s, by simp, ?_⟩
    replace hx : (Y.presheaf.map (homOfLE (Y.basicOpen_le s)).op ≫ f.app _).hom x = 0 := by
      trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)
      · simp [-NatTrans.naturality, RingHom.algebraMap_toAlgebra]
      · simp only [Scheme.affineBasicOpen_coe, RingHom.mem_ker] at hx
        rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]
    rwa [f.naturality] at hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]

Goal state after:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ StructureSheaf.toStalk (↑R) (closedPoint ↑R) =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint ↑R)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ stalkClosedPointTo (f ≫ g) = Hom.stalkMap g (f (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x✝¹ : ↑Γ(X, ↑V)
hx : x✝¹ ∈ I.ideal V
x : ↥↑(↑U ⊓ ↑V)
x✝ : x ∈ ⊤
⊢ x ∈ (↑U ⊓ ↑V).ι ⁻¹ᵁ ↑V

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : ↑Y.affineOpens
⊢ f.ker.ideal U = RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
by

Goal state after: