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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x').asIdeal (↑x').asIdeal
        (CommRingCat.Hom.hom f.op.unop) ⋯)
      (↑((toSpecΓ R).hom' x✝) ⟨PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x', ⋯⟩) =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'

Tactic:
]

Goal state after:
R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x').asIdeal (↑x').asIdeal
        (CommRingCat.Hom.hom f.op.unop) ⋯)
      (↑((toSpecΓ R).hom' x✝) ⟨PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x', ⋯⟩) =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        (CommRingCat.ofHom
            (stalkIso (↑(CommRingCat.of ↑R))
                    (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                      x)).symm.toRingEquiv.toRingHom ≫
          CommRingCat.ofHom
              (Localization.localRingHom
                (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                    x).asIdeal
                x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
            CommRingCat.ofHom (stalkIso (↑(CommRingCat.of (Localization M))) x).toRingEquiv.toRingHom))

Tactic:
]

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        (CommRingCat.ofHom
            (stalkIso (↑(CommRingCat.of ↑R))
                    (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                      x)).symm.toRingEquiv.toRingHom ≫
          CommRingCat.ofHom
              (Localization.localRingHom
                (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                    x).asIdeal
                x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
            CommRingCat.ofHom (stalkIso (↑(CommRingCat.of (Localization M))) x).toRingEquiv.toRingHom))
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
this :
  Function.Bijective
    ⇑(ConcreteCategory.hom
        (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom)
⊢ Function.Bijective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
        (algebraMap (↑R) (Localization M)) ⋯)

Tactic:
]

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
this :
  Function.Bijective
    ⇑(ConcreteCategory.hom
        (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom)
⊢ Function.Bijective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
        (algebraMap (↑R) (Localization M)) ⋯)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        ((TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).hom.base).obj
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p trivial

Tactic:
]

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        ((TopCat.Presheaf.pushforward CommRingCat (Spec.sheafedSpaceMap f).hom.base).obj
              (Spec.sheafedSpaceObj S).presheaf).germ
          ⊤ p trivial
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ↑{ carrier := carrier✝, is_open' := is_open'✝ } = carrier✝

Tactic:
]

Goal state after:
case app.op.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
carrier✝ : Set ↑↑(Y.restrict ⋯)
is_open'✝ : IsOpen carrier✝
⊢ ↑{ carrier := carrier✝, is_open' := is_open'✝ } = carrier✝
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ f.c.app (op (⋯.functor.obj (unop U))) ≫
      X.presheaf.map (((Opens.map f.base).map (⋯.functor.map i.unop)).op ≫ eqToHom ⋯) =
    f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map (𝟙 ↑X)).map i.unop).op)

Tactic:
]

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ f.c.app (op (⋯.functor.obj (unop U))) ≫
      X.presheaf.map (((Opens.map f.base).map (⋯.functor.map i.unop)).op ≫ eqToHom ⋯) =
    f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯ ≫ ((Opens.map (𝟙 ↑X)).map i.unop).op)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
x : (Opens ↑↑Y)ᵒᵖ
⊢ f.c.app x ≫ X.presheaf.map ((Opens.map f.base).op.map (⋯.adjunction.counit.app (unop x)).op ≫ (eqToIso ⋯).hom) =
    f.c.app x
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ app f U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = appLE f U V' ⋯

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op V ⟶ op V'
⊢ app f U ≫ X.presheaf.map ((homOfLE e).op ≫ i) = appLE f U V' ⋯
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ app f U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = appLE f U' V ⋯

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ app f U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = appLE f U' V ⋯
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono ((isoRestrict f).hom ≫ Y.ofRestrict ⋯)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono ((isoRestrict f).hom ≫ Y.ofRestrict ⋯)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case x
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ ⇑(ConcreteCategory.hom f.base) '' ↑U = ⇑(ConcreteCategory.hom f.base) '' ↑U

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ X.presheaf.map (eqToHom ⋯) =
    ((X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj (unop U))))) ≫
        Y.presheaf.map ((opensFunctor f).op.map i)) ≫
      f.c.app (op ((opensFunctor f).obj (unop V)))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op U)) = invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op U)) = invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ appLE (f ≫ g) U V e = appLE (f ≫ g) U V ⋯

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (homOfLE ⋯).op

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ X.presheaf.map (eqToHom ⋯) =
    f.c.app (op U) ≫ ((TopCat.Presheaf.pushforward C f.base).obj X.presheaf).map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ X.presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (eqToHom ⋯).op

Tactic:
simp only [app_invApp, Opens.carrier_eq_coe,
    homOfLE_leOfHom, eqToHom_op]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ : Y.presheaf ⟶ (Presheaf.pushforward CommRingCat { hom' := { toFun := f₁, continuous_toFun := f₂ } }).obj X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
⊢ { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }.copyBase
      ⇑{ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ } ⋯ =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }

Tactic:
simp only [Hom.copyBase]

Goal state after:
X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ : Y.presheaf ⟶ (Presheaf.pushforward CommRingCat { hom' := { toFun := f₁, continuous_toFun := f₂ } }).obj X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
⊢ {
      base :=
        ofHom
          { toFun := ⇑(ConcreteCategory.hom { hom' := { toFun := f₁, continuous_toFun := f₂ } }),
            continuous_toFun := ⋯ },
      c := f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ } =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ Scheme.Spec.map (inv f.op) = Scheme.Spec.map (inv f.op)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ U ⊓ X.basicOpen ((ConcreteCategory.hom (Hom.app f V)) s) = U ⊓ X.basicOpen ((ConcreteCategory.hom (Hom.app f V)) s)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_5.e_8.e_5
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ (⋯.functor.obj U ⟶ hf.functor.obj U) = (unop (op (hf.functor.obj U)) ⟶ unop (op (hf.functor.obj U)))

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ (X.restrict h).presheaf.map (eqToHom ⋯) = (X.ofRestrict h).c.app (op ((opensFunctor (X.ofRestrict h)).obj U))
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus ↑(Ideal.span ↑I * Ideal.span ↑J)

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus ↑(Ideal.span ↑I * Ideal.span ↑J)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ X.zeroLocus t ⊆ X.zeroLocus s

Tactic:
by
  simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]
  exact fun x H f hf hxf ↦ H f (h hf) hxf

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso
    (Hom.stalkMap (Y.ofRestrict ⋯) ((ConcreteCategory.hom (isoRestrict f).hom.base) x) ≫
      Hom.stalkMap (isoRestrict f).hom x)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso
    (Hom.stalkMap (Y.ofRestrict ⋯) ((ConcreteCategory.hom (isoRestrict f).hom.base) x) ≫
      Hom.stalkMap (isoRestrict f).hom x)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
x✝ : x ∈ U
⊢ x ∈ U

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
x✝ : x ∈ U
⊢ x ∈ U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ f ∉ x.asIdeal

Tactic:
]

Goal state after:
R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ f ∉ x.asIdeal
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit
    ((CommRingCat.Hom.hom
        (toStalk (↑R) p ≫
          (TopCat.Presheaf.stalkFunctor CommRingCat p).map
            (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c))
      x)

Tactic:
]

Goal state after:
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ p.asIdeal.primeCompl
⊢ IsUnit
    ((CommRingCat.Hom.hom
        (toStalk (↑R) p ≫
          (TopCat.Presheaf.stalkFunctor CommRingCat p).map
            (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap ↑R ↑S))).hom.c))
      x)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ 𝟙 (Scheme.Spec.obj (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap (↑(CommRingCat.of ↑S))
              ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj (op ⊤)))) ≫
          ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
            ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0

Tactic:
]

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (algebraMap (↑(CommRingCat.of ↑S))
              ((structureSheafInType ↑(CommRingCat.of ↑S) ↑(CommRingCat.of ↑S)).obj.obj
                ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj (op ⊤)))) ≫
          ((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
            ⊤ p trivial))
      0
⊢ ∃ m, m • x = 0
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
]

Goal state after:
X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ (pullbackConeOfLeftFst f g ≫ f).base = (Y.ofRestrict ⋯ ≫ g).base

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens ↑↑Z)ᵒᵖ
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ Functor.whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U =
    (Y.ofRestrict ⋯ ≫ g).c.app U

Tactic:
· simpa using! pullback.condition

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens ↑↑Z)ᵒᵖ
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ Functor.whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U =
    (Y.ofRestrict ⋯ ≫ g).c.app U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s ^ n)

Tactic:
]

Goal state after:
X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s ^ n)