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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Goal state after:
X : Scheme
I : X.IdealSheafData
ideal : (U : ↑X.affineOpens) → Ideal ↑Γ(X, ↑U)
map_ideal_basicOpen :
  ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)
supportSet : Set ↥X
supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a
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)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
⊢ (IsAffineOpen.fromSpec ⋯) x ∈ Z → (CommRingCat.Hom.hom F) x✝ ∈ x.asIdeal

Tactic:
hxZ

Goal state after:
case a
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)
x : ↥(Spec Γ(X, ↑(X.affineBasicOpen f)))
hxZ : (IsAffineOpen.fromSpec ⋯) x ∈ Z
⊢ (CommRingCat.Hom.hom F) x✝ ∈ x.asIdeal
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
simp only [le_def, vanishingIdeal_ideal, ← PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal]

Goal state after:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ Z ≤ I.support ↔ ∀ (U : ↑X.affineOpens), ⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
H : ∀ (U : ↑X.affineOpens), ↑Z ∩ ↑↑U ⊆ ↑I.support ∩ ↑↑U
x : ↥X
hx : x ∈ Z
⊢ x ∈ I.support

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Goal state after:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
H : ∀ (U : ↑X.affineOpens), ↑Z ∩ ↑↑U ⊆ ↑I.support ∩ ↑↑U
x : ↥X
hx : x ∈ Z
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ I.support
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) r)

Tactic:
rw [X.basicOpen_res]

Goal state after:
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = U ⊓ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V =
    IsOpenImmersion.lift (↑V ⊓ ↑U₀).ι
        (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U).ι)
        ⋯ ≫
      X.homOfLE ⋯

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]
      simp [pullback.condition_assoc]

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

Goal state before:
pp: case h₁
X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ (pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
          (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
        pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯))) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯) =
    (pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
        I.glueDataT i j) ≫
      pullback.snd (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]
      simp [pullback.condition_assoc]

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

Goal state before:
pp: case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))

Tactic:
simp_rw [Scheme.preimage_basicOpen] at hf

Goal state after:
case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
hf :
  ∀ (r : ↥s),
    IsAffine ↑(X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) ↑r)) ∧
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
⊢ IsAffineHom f ↔ targetAffineLocally (fun X x x_1 x_2 ↦ IsAffine X) f

Tactic:
simp only [targetAffineLocally, Scheme.affineOpens, Set.coe_ofPred, Set.mem_ofPred_eq,
      Subtype.forall, isAffineHom_iff]

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ↔ ∀ (a : Y.Opens), IsAffineOpen a → IsAffine ↑(f ⁻¹ᵁ a)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_2
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ ↑I.support
⊢ x ∈ Set.range ⇑I.gluedTo

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ ↑I.support
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ Set.range ⇑I.gluedTo
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf✝ : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine ↑(f ⁻¹ᵁ ↑⟨U, hU⟩)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
have hf : Q (Scheme.Hom.app f (((⟨U, hU⟩ : Y.affineOpens) : Y.Opens).ι ''ᵁ ⊤)).hom := hf

Goal state after:
case right
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
hf✝¹ : ∀ (U : ↑Y.affineOpens), IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))
U : Y.Opens
hU : IsAffineOpen U
hfU : IsAffine ↑(f ⁻¹ᵁ ↑⟨U, hU⟩)
hf✝ : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑⟨U, hU⟩).ι ''ᵁ ⊤)))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ ↑(Hom.ker f).support ⊆ closure (⇑(Hom.imageι f) '' Set.range ⇑(Hom.toImage f))

Tactic:
Hom.support_ker,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
inst✝ : QuasiCompact f
⊢ closure (Set.range ⇑f) ⊆ closure (⇑(Hom.imageι f) '' Set.range ⇑(Hom.toImage f))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
h f

Goal state after:
case refine_2
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ {X Y : Scheme} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ ((∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f ((pullback.fst f f) x)
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
H : (pullback.fst f f) x = (pullback.snd f f) x
i : 𝒰.I₀ := Cover.idx 𝒰 (f ((pullback.fst f f) x))
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f ((pullback.fst f f) x)
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = (pullback.fst f f) x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = x
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f x
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = (pullback.diagonal f) x

Tactic:
obtain ⟨z, hz₁, hz₂⟩ := exists_preimage_pullback _ _ hy.symm

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
x : ↥X
i : 𝒰.I₀ := Cover.idx 𝒰 (f x)
y : ↥(𝒰.X i)
hy : (𝒰.f i) y = f x
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
⊢ ∃ a b y, ((diagonalCover f 𝒰 𝒱).f ⟨a, (b, b)⟩) y = (pullback.diagonal f) x
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: case union
R : Type u_1
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
ht : IsConstructible t
Ht : ∃ S, S.toSet = t
S : ConstructibleSetData R
hs : IsConstructible S.toSet
⊢ ∃ S_1, S_1.toSet = S.toSet ∪ t

Tactic:
obtain ⟨T, rfl⟩ := Ht

Goal state after:
case union
R : Type u_1
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
S : ConstructibleSetData R
hs : IsConstructible S.toSet
T : ConstructibleSetData R
ht : IsConstructible T.toSet
⊢ ∃ S_1, S_1.toSet = S.toSet ∪ T.toSet
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ Disjoint (Set.range ⇑g) (Set.range ⇑(X.affineCover.f i))

Tactic:
rw [← Set.subset_compl_iff_disjoint_left]

Goal state after:
X Y : Scheme
inst✝ : Subsingleton ↥Y
f : X ⟶ Y
g : Y ⟶ X
hg : g ≫ f = 𝟙 Y
this : ∀ {X Y : Scheme} [Subsingleton ↥Y] (f : X ⟶ Y) (g : Y ⟶ X), g ≫ f = 𝟙 Y → (∃ R, X = Spec R) → IsClosedImmersion g
hX : ¬∃ R, X = Spec R
i : X.affineCover.toPreZeroHypercover.1
hxU : ¬Set.range ⇑g ⊆ ↑(Scheme.Hom.opensRange (X.affineCover.f i))
⊢ Set.range ⇑(X.affineCover.f i) ⊆ (Set.range ⇑g)ᶜ
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
⊢ LocallyOfFiniteType f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation] at hf

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ LocallyOfFiniteType f
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ map (algebraMap R x.asIdeal.ResidueField) f ≠ 0

Tactic:
refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0

Tactic:
refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ IsNilpotent ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
⊢ DiscreteTopology ↥X

Tactic:
apply discreteTopology_iff_isOpen_singleton.mpr
  intro x
  obtain ⟨W, hW1, hW2, _⟩ := exists_isAffineOpen_mem_and_subset (TopologicalSpace.Opens.mem_top x)
  have : IsArtinianRing Γ(X, W) := IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hW1⟩
  have : DiscreteTopology (Spec Γ(X, W)) := inferInstanceAs (DiscreteTopology (PrimeSpectrum _))
  have : DiscreteTopology W := hW1.isoSpec.hom.homeomorph.symm.discreteTopology
  simpa using (isOpen_discrete ({⟨x, hW2⟩} : Set W)).trans W.2

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
apply IsLocallyNoetherian.component_noetherian

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := ⋯
i : 𝒰.I₀
this : IsAffine (𝒰.X i)
U : ↑X.affineOpens := ⋯
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
apply IsLocallyNoetherian.component_noetherian

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
⊢ IsReduced X

Tactic:
let pt (Z : irreducibleComponents Y) := Y.presheaf.stalk Z.property.1.genericPoint
  have hpt (Z : _) : IsField (pt Z) :=
    isField_stalk_of_closure_mem_irreducibleComponents _ _ (by
      rw [Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)]
      exact Z.property)
  let (Z : _) := (hpt Z).toField
  let Z := ∐ fun Z ↦ Spec (pt Z)
  let g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk _
  have : Finite Z := (sigmaMk _).finite_iff.mp inferInstance
  have : QuasiCompact g := ⟨fun _ _ _ ↦ (Set.toFinite _).isCompact⟩
  have H : IsSchemeTheoreticallyDominant g := by
    rw [isSchemeTheoreticallyDominant_iff_isDominant, isDominant_iff, denseRange_iff_closure_range,
      Set.eq_univ_iff_forall]
    intro y
    let z : Z := Sigma.ι (fun Z ↦ Spec (pt Z)) ⟨_, irreducibleComponent_mem_irreducibleComponents y⟩
      (IsLocalRing.closedPoint _)
    have hz : g z ⤳ y := by
      simp only [g, z, Z, ← Scheme.Hom.comp_apply, Sigma.ι_desc, pt,
        Scheme.fromSpecStalk_closedPoint]
      exact (IsIrreducible.isGenericPoint_genericPoint _
        isClosed_irreducibleComponent).specializes mem_irreducibleComponent
    exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)
  suffices IsReduced (pullback f g) from IsSchemeTheoreticallyDominant.isReduced (pullback.fst f g)
  have H := IsUniversalColimit.isPullback_of_isColimit_left
    (X := fun Z ↦ Spec (pt Z))
    (FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct _))
    (fun Z ↦ Y.fromSpecStalk _) g f _ _ (fun _ ↦ .of_hasPullback _ _) (coproductIsCoproduct _)
  apply +allowSynthFailures @isReduced_of_isOpenImmersion (f := H.isoPullback.inv)
  apply +allowSynthFailures @IsReduced.of_openCover (𝒰 := sigmaOpenCover _)
  exact fun i ↦ GeometricallyReduced.geometrically_isReduced _ _ _ (.of_hasPullback _ _)

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

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ S
g : Y ⟶ S
inst✝² : IsSchemeTheoreticallyDominant f
inst✝¹ : QuasiCompact f
inst✝ : Flat g
h𝒰 : TopologicalSpace.IsOpenCover fun V ↦ (↑V).1 :=
  TopologicalSpace.Opens.IsBasis.isOpenCover_mem_and_le (Scheme.isBasis_affineOpens Y)
    (TopologicalSpace.IsOpenCover.comap (TopologicalSpace.Opens.IsBasis.isOpenCover (Scheme.isBasis_affineOpens S))
      (TopCat.Hom.hom g.base))
V : TopologicalSpace.Opens ↥Y
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hV : (V, ⟨U, hU⟩).1 ∈ Y.affineOpens
hVU : V ≤ g ⁻¹ᵁ U
x : ↑Γ(Y, V)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app (pullback.snd f g) V))
this : Function.Injective ⇑(ConcreteCategory.hom (pushoutSection ⋯ hVU ⋯ ⋯))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯))

Tactic:
by simpa [Scheme.Hom.appLE] using f.app_injective U

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
⊢ topologically (@IsOpenMap) f'

Tactic:
have hf' : IsOpenImmersion f' := MorphismProperty.of_isPullback hf.flip inferInstance

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
hf' : IsOpenImmersion f'
⊢ topologically (@IsOpenMap) f'
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: ⊢ geometrically IsIntegral = geometrically (IsReduced ⊓ fun x ↦ IrreducibleSpace ↥x)

Tactic:
eta_expand

Goal state after:
⊢ (fun ⦃X Y⦄ x ↦ geometrically (fun X ↦ IsIntegral X) x) = fun ⦃X Y⦄ x ↦
    geometrically (fun a ↦ ((fun X ↦ IsReduced X) ⊓ fun x ↦ IrreducibleSpace ↥x) a) x
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
⊢ CompactSpace ↥X

Tactic:
let q : T ⟶ Spec (.of K) := Spec.map (CommRingCat.ofHom MvPolynomial.C)

Goal state after:
X : Scheme
K : Type u
inst✝¹ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : 𝒰.I₀ → X.Opens := fun i ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
⊢ CompactSpace ↥X
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ (algebraMap R (Localization.Away (f t))) (⟨(fun x ↦ t ^ x) n, ⋯⟩ • (algebraMap S (Localization.Away (f t))) r)
      p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
IsScalarTower.algebraMap_eq R S,

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ ((algebraMap S (Localization.Away (f t))).comp (algebraMap R S))
      (⟨(fun x ↦ t ^ x) n, ⋯⟩ • (algebraMap S (Localization.Away (f t))) r) p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite), and_iff_right (by infer_instance),
    RingHom.finite_respectsIso.arrow_mk_iso_iff (arrowIsoΓSpecOfIsAffine f)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
X✝ Y✝ Z✝ : Type uᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : Scheme
⊢ reindex (⇑(ConcreteCategory.hom (g.unop ≫ f.unop))) x✝ =
    reindex (⇑(ConcreteCategory.hom f.unop)) x✝ ≫ reindex (⇑(ConcreteCategory.hom g.unop)) x✝

Tactic:
exact reindex_comp _ _ _

Goal state after: