mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
            𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
erw [limit.lift_π_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j ↦ D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app
            (op (WalkingMultispan.left (i, j))) ≫
          𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : closure (Set.range ⇑(f ≫ g)) = Set.univ
⊢ closure (Set.range ⇑g) = Set.univ

Tactic:
← Set.univ_subset_iff

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Set.univ ⊆ closure (Set.range ⇑(f ≫ g))
⊢ Set.univ ⊆ closure (Set.range ⇑g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
g : T ⟶ Y
inst✝ : HasPullback g f
i : (Precoverage.ZeroHypercover.pullback₁ (pullback.snd g f) 𝒰).I₀
⊢ P (pullback.fst g (𝒰.f i ≫ f))

Tactic:
exact hf i _ _ _ (IsPullback.of_hasPullback ..)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ SurjectiveOnStalks f ↔ SurjectiveOnStalks (Spec.map (Scheme.Hom.app f ⊤))

Tactic:
MorphismProperty.arrow_mk_iso_iff @SurjectiveOnStalks (arrowIsoSpecΓOfIsAffine f)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
⊢ SurjectiveOnStalks (Spec.map (Scheme.Hom.appTop f)) ↔ SurjectiveOnStalks (Spec.map (Scheme.Hom.app f ⊤))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : ↑X.affineOpens), P S → P (S ⊔ ↑U)
s : Set ↑X.affineOpens
hs : s.Finite
hS : IsCompact ↑(⨆ i ∈ s, ↑i)
⊢ P (⨆ i ∈ ∅, ↑i)

Tactic:
by simpa using h₁

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 Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
⊢ ∀ (U : ↑Z.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))

Tactic:
intro U V e

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion f
H :
  ∀ (U : ↑Z.affineOpens) (V : ↑Y.affineOpens) (e : ↑V ≤ g ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE g (↑U) (↑V) e))
U : ↑Z.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ (f ≫ g) ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) (↑U) (↑V) e))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.FiniteHeight
inst✝ : I.IsPrime
⊢ I.height ≠ ⊤

Tactic:
exact Ideal.height_ne_top ‹I.IsPrime›.ne_top

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 Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource P

Tactic:
apply HasAffineProperty.isZariskiLocalAtSource
  intro X Y f _ 𝒰
  simp_rw [← HasAffineProperty.iff_of_isAffine (P := P),
    iff_of_source_openCover 𝒰.affineRefinement.openCover,
    fun i ↦ iff_of_source_openCover (P := P) (f := 𝒰.f i ≫ f) (𝒰.X i).affineCover]
  simp [Scheme.OpenCover.affineRefinement, Sigma.forall]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s : ToType (X.presheaf.obj (op U))
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) (s ^ n) = (CommRingCat.Hom.hom (X.presheaf.germ U x hxU)) 0
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' : (ConcreteCategory.hom (X.presheaf.map iU.op)) s = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hxU)) s = 0

Tactic:
rw [← X.presheaf.germ_res iU x hxV, CommRingCat.comp_apply, e', map_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
k : Algebra ↑R ↑((Spec R).presheaf.stalk x) := StructureSheaf.stalkAlgebra (↑R) x
this : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x)) x.asIdeal
⊢ ↑x.asIdeal.height = ↑(coheight x)

Tactic:
apply WithBot.coe_eq_coe.mpr

Goal state after:
R : CommRingCat
x : ↥(Spec R)
k : Algebra ↑R ↑((Spec R).presheaf.stalk x) := ⋯
this : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x)) x.asIdeal
⊢ x.asIdeal.height = coheight x
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:
obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    hxU U.2

Goal state after:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑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
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)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n : ℕ
hx : (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s))) x = 0
⊢ ((CommRingCat.Hom.hom (f.app ↑U)) x |_ f ⁻¹ᵁ Y.basicOpen s) ⋯ = 0

Tactic:
f.naturality

Goal state after:
case a
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 : (CommRingCat.Hom.hom (f.app ↑U ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op)) x = 0
⊢ ((CommRingCat.Hom.hom (f.app ↑U)) x |_ f ⁻¹ᵁ Y.basicOpen s) ⋯ = 0
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ (Spec R).presheaf.germ ⊤ ((Spec.map φ) (closedPoint ↑S)) trivial ≫ stalkClosedPointTo (Spec.map φ) =
    (ΓSpecIso R).hom ≫ φ

Tactic:
rw [stalkClosedPointTo, Scheme.Hom.germ_stalkMap_assoc, ← Iso.inv_comp_eq,
    ← ΓSpecIso_inv_naturality_assoc]
  simp_rw [Opens.map_top]
  rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ f x ∈ Y.zeroLocus ↑((ker f).ideal ⟨U, hU⟩)

Tactic:
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ ∀ f_1 ∈ (ker f).ideal ⟨U, hU⟩, f x ∉ Y.basicOpen f_1
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ residueDegree (𝟙 X) x = 1

Tactic:
by
  dsimp [residueDegree]
  rw [residueFieldMap_id]
  exact CommSemiring.finrank_self _

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

Goal state before:
pp: case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : IsEmpty 𝒰.I₀
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

Tactic:
have : IsEmpty X := Function.isEmpty 𝒰.idx
    simp [ker_eq_top_of_isEmpty]

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)

Tactic:
rw [Scheme.Hom.comp_base, Opens.map_comp_obj]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((Opens.map f.base).obj ((Opens.map g.base).obj U))
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case hs₂
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ ∀ i ∈ ⇑(ConcreteCategory.hom U.topIso.inv) '' s, IsAffineOpen ((↑U).basicOpen i)

Tactic:
· rintro _ ⟨j, hj, rfl⟩
    rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]
    simpa [Scheme.Opens.toScheme_presheaf_obj] using hs₂ j hj

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ adjoin R ↑(t r)

Tactic:
rw [ht]

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
t : (r : ↥s) → Finset (Localization.Away ↑r)
ht : ∀ (r : ↥s), adjoin R ↑(t r) = ⊤
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
sf : ↥s → Finset S := fun x ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ↑x) (t x)
x : S
r : ↑↑s
⊢ (algebraMap S (Localization.Away ↑r)) x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ (𝟭 (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ).map f ≫
      (MorphismProperty.Over.isoMk (asIso (Scheme.Hom.toImage (unop Y).hom)).symm ⋯).op.hom =
    (MorphismProperty.Over.isoMk (asIso (Scheme.Hom.toImage (unop X).hom)).symm ⋯).op.hom ≫
      (((MorphismProperty.Over.forget @IsClosedImmersion ⊤ X✝).op ⋙ X✝.kerFunctor) ⋙
            { obj := fun I ↦ op (MorphismProperty.Over.mk ⊤ I.subschemeι ⋯),
              map := fun {I J} h ↦ (MorphismProperty.Over.homMk (Scheme.IdealSheafData.inclusion ⋯) ⋯ ⋯).op,
              map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
by
      apply Quiver.Hom.unop_inj
      ext1
      dsimp
      rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq,
        ← cancel_mono (Scheme.IdealSheafData.subschemeι _)]
      simp

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

Goal state before:
pp: case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (I.map f).map g ≤ I.map (f ≫ g)

Tactic:
rw [le_map_iff_comap_le, comap_comp]

Goal state after:
case a
X Y Z : Scheme
I : X.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
⊢ (((I.map f).map g).comap g).comap f ≤ I
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| f ⁻¹ᵁ (coborderRange f).ι ''ᵁ U

Tactic:
enter [1]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
U : (↑(coborderRange f)).Opens
| TopologicalSpace.Opens.map f.base
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A →ₐ[R] S
hf : Function.Surjective ⇑f
t : Finset A
ht : Ideal.span ↑t = ⊤
H : ∀ (g : ↥t), FinitePresentation R (Localization.Away (f ↑g))
⊢ FinitePresentation R S

Tactic:
apply Algebra.FinitePresentation.of_surjective hf
  apply RingHom.ker_fg_of_localizationSpan t ht
  intro g
  let f' : Localization.Away g.val →ₐ[R] Localization.Away (f g) :=
    Localization.awayMapₐ f g.val
  have (g : t) : Algebra.FinitePresentation R (Localization.Away g.val) :=
    haveI : Algebra.FinitePresentation A (Localization.Away g.val) :=
      IsLocalization.Away.finitePresentation g.val
    Algebra.FinitePresentation.trans R A (Localization.Away g.val)
  apply Algebra.FinitePresentation.ker_fG_of_surjective f'
  exact IsLocalization.Away.mapₐ_surjective_of_surjective _ hf

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

Goal state before:
pp: case refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
⊢ IsPullback (e ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι) f' f
    (Scheme.Hom.liftCoborder g ≫ (Scheme.Hom.coborderRange g).ι)

Tactic:
· simpa [e] using H.flip

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

Goal state before:
pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := ⋯
Y' : Over Z := ⋯
U' : Over Z := ⋯
f' : X' ⟶ Y' := ⋯
g' : X' ⟶ Y' := ⋯
ι' : U' ⟶ X' := ⋯
this : IsSeparated Y'.hom
⊢ IsDominant (Over.Hom.left (equalizer.lift ι' ?m.149) ≫ Over.Hom.left (equalizer.ι f' g'))

pp: W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ ι' ≫ f' = ι' ≫ g'

Tactic:
· rwa [← Over.comp_left, equalizer.lift_ι]

Goal state after:
W X Y Z : Scheme
inst✝² : IsReduced X
f g : X ⟶ Y
s : Y ⟶ Z
inst✝¹ : IsSeparated s
h : f ≫ s = g ≫ s
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
X' : Over Z := Over.mk (f ≫ s)
Y' : Over Z := Over.mk s
U' : Over Z := Over.mk (ι ≫ f ≫ s)
f' : X' ⟶ Y' := Over.homMk f ⋯
g' : X' ⟶ Y' := Over.homMk g ⋯
ι' : U' ⟶ X' := Over.homMk ι ⋯
this : IsSeparated Y'.hom
⊢ ι' ≫ f' = ι' ≫ g'
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f →
      (RingHom.ker f).FG → ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)

Tactic:
intro R _ S _ f hf hf' s hs
    refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_
    rw [range_comap_of_surjective _ f hf]
    exact isRetrocompact_zeroLocus_compl_of_fg hf'

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
rw [ht]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (zeroLocus ↑t)ᶜ
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
⊢ IsOpen {x}

Tactic:
have : IsArtinianRing Γ(X, W) := IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hW1⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right✝ : W.carrier ⊆ ↑⊤
this : IsArtinianRing ↑Γ(X, W)
⊢ IsOpen {x}
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ Scheme.Hom.ker g = ⊥

Tactic:
g.ker_eq_bot

Goal state after:
X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ ⊥ = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ ↑V
hVU : V ≤ U
⊢ (ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op ≫ app f V)) s =
    (ConcreteCategory.hom (app f V)) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op)) 0)

Tactic:
f.naturality

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
s : ↑Γ(Y, U)
hs : (ConcreteCategory.hom (app f U)) s = 0
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ ↑V
hVU : V ≤ U
⊢ (ConcreteCategory.hom
        (app f (Opposite.unop (Opposite.op U)) ≫
          X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE hVU).op.unop).op))
      s =
    (ConcreteCategory.hom (app f V)) ((ConcreteCategory.hom (Y.presheaf.map (homOfLE hVU).op)) 0)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)

Tactic:
convert! PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation

Goal state after:
case convert_6
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.HasGoingDown ↑R ↑S

case convert_7
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.FinitePresentation ↑R ↑S
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))

Tactic:
intro U V e

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
⊢ topologically (@IsClosedMap) f'

Tactic:
have := UniversallyClosed.universally_isClosedMap _ _ _
    ((IsPullback.of_hasPullback i₁ f).paste_horiz H)

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
this : topologically (@IsClosedMap) (pullback.fst i₁ f ≫ f')
⊢ topologically (@IsClosedMap) f'
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))

Tactic:
← toSpecΓ_naturality

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (f ≫ Y.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app (Spec.map (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
          ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (isoOfIsAffine n (Spec R)).inv ⊤)) (coord (Spec R) i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
isoOfIsAffine_inv_appTop_coord,

Goal state after:
n : Type u
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app (Spec.map (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
          ⊤))
      ((ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(Spec R, ⊤)))).inv) (X i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
⊢ IsIso (Spec.preimage (X.fromSpecResidueField x ≫ f))

Tactic:
have : IsFinite (X.fromSpecResidueField x ≫ f) := by
      rw [isClosed_singleton_iff_isClosedImmersion] at hx
      rw [isFinite_iff_locallyOfFiniteType_of_jacobsonSpace]
      infer_instance

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ IsIso (Spec.preimage (X.fromSpecResidueField x ≫ f))