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

Goal state before:
pp: 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), affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) (f ∣_ Y.basicOpen ↑r)
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
dsimp [affineAnd] at hf
    have : IsAffine X := by
      apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
      · apply_fun Ideal.map (f.appTop).hom at hs
        rwa [Ideal.map_span, Ideal.map_top] at hs
      · rintro - ⟨r, hr, rfl⟩
        simp_rw [Scheme.preimage_basicOpen] at hf
        exact (hf ⟨r, hr⟩).left
    refine ⟨inferInstance, hQs.ofIsLocalization' hPi (f.appTop).hom s hs fun a ↦ ?_⟩
    refine ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance,
      inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩
    · exact (isAffineOpen_top X).isLocalization_basicOpen (f.appTop a.val)
    · obtain ⟨_, hf⟩ := hf a
      rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf
      -- Not sure why the `show` fixes the following `rw` complaining about "motive is incorrect"
      have hf : Q (Scheme.Hom.app f ((Y.basicOpen a.1).ι ''ᵁ ⊤)).hom := hf
      rw [Scheme.Opens.ι_image_top] at hf
      rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map _ (isAffineOpen_top X)] at hf
      rwa [CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U = ⇑I.gluedTo '' ⇑I.gluedTo ⁻¹' ↑↑U

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U = ↑↑U ∩ Set.range ⇑I.gluedTo
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: 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 = ⊤
h : ∀ (i : ↥s), FiniteType R (Localization.Away ↑i)
⊢ FiniteType R S

Tactic:
replace h := fun r => (h r).1

Goal state after:
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 = ⊤
h : ∀ (r : ↥s), ⊤.FG
⊢ FiniteType R S
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Hom.app I.subschemeι ↑U ≫ Hom.app (I.subschemeCover.f U) (I.subschemeι ⁻¹ᵁ ↑U) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫
      (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).inv ≫
        (Spec (I.subschemeCover.X U)).presheaf.map
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom ⋯).unop).op ≫
          (Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯)
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv

Tactic:
simp_rw [← Category.assoc, ← IsIso.comp_inv_eq] at this

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  (((Hom.app I.subschemeι ↑U ≫ Hom.app (I.subschemeCover.f U) (I.subschemeι ⁻¹ᵁ ↑U)) ≫
          inv ((Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯))) ≫
        inv
          ((Spec (I.subschemeCover.X U)).presheaf.map
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map
                (eqToHom ⋯).unop).op)) ≫
      inv (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).inv =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case mp.inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this✝¹ :
  HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) fun {R S} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this✝ :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
    (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      ∀ {X Y : Scheme} (f : X ⟶ Y),
        (HasRingHomProperty (affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q)
            fun {R S} [CommRing R] [CommRing S] ↦ Q) →
          IsAffineHom f →
            IsAffine Y →
              (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
                affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
this : IsAffine ↑(f ⁻¹ᵁ ↑U)
⊢ IsAffineOpen ↑U

Tactic:
exact U.2

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) =
    @IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
ext X Y f

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    (@IsAffineHom ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) 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))
⊢ P = targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)

Tactic:
ext X Y 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
⊢ P f ↔ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) f
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
exact HasRingHomProperty.isLocal_ringHomProperty P'

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFiniteType = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType

Tactic:
ext X Y f

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFiniteType f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: ⊢ @IsClosedImmersion =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓ @SurjectiveOnStalks

Tactic:
ext X Y f

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.snd f I.subschemeι = (I.comap f).subschemeMap I f ⋯

Tactic:
← cancel_mono I.subschemeι

Goal state after:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ ((I.comapIso f).hom ≫ pullback.snd f I.subschemeι) ≫ I.subschemeι = (I.comap f).subschemeMap I f ⋯ ≫ I.subschemeι
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)
⊢ f ((pullback.fst f f) x) = f ((pullback.snd f f) x)

Tactic:
← Scheme.Hom.comp_apply,

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)
⊢ (pullback.fst f f ≫ f) x = f ((pullback.snd f f) 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
hf : Function.Injective ⇑f
x : ↥(pullback.diagonalObj f)
⊢ (pullback.fst f f ≫ f) x = f ((pullback.snd f f) x)

Tactic:
← Scheme.Hom.comp_apply,

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)
⊢ (pullback.fst f f ≫ f) x = (pullback.snd f f ≫ f) x
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

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

Tactic:
by
  conv_rhs => enter [1]; rw [← f.liftCoborder_ι]
  rw [Scheme.Hom.comp_preimage, Scheme.Hom.preimage_image_eq]

Goal state after:
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
z : ↥(pullback f (𝒰.f i))
hz₁ : (pullback.fst f (𝒰.f i)) z = x
hz₂ : (pullback.snd f (𝒰.f i)) z = y
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w) =
    (pullback.diagonal f) ((pullback.fst f (𝒰.f i)) (((𝒱 i).f j) w))

Tactic:
← Scheme.Hom.comp_apply,

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
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) ((pullback.diagonal ((𝒱 i).f j ≫ pullback.snd f (𝒰.f i))) w) =
    (pullback.fst f (𝒰.f i) ≫ pullback.diagonal f) (((𝒱 i).f j) w)
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ comap (Ideal.Quotient.mk I) '' comap (Ideal.Quotient.mk I) ⁻¹' ↑(basicOpen (↑C).f) = (↑C).toSet

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
R : Type u
inst✝ : CommRing R
s : ConstructibleSetData R
hs : IsConstructible s.toSet
e_2✝ : ↥s = ↑↑s
C : ↥s
I : Ideal R := Ideal.span (Set.range (↑C).g)
f : R ⧸ I := (Ideal.Quotient.mk I) (↑C).f
⊢ ↑(basicOpen (↑C).f) ∩ Set.range (comap (Ideal.Quotient.mk I)) = (↑C).toSet
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), IsAffine ((𝒱 i).X j)
⊢ IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)

Tactic:
by
  let U : (Σ i, (𝒱 i).I₀) → (diagonalCoverDiagonalRange f 𝒰 𝒱).toScheme.Opens := fun i ↦
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ⁻¹ᵁ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange
  have hU (i) : (diagonalCoverDiagonalRange f 𝒰 𝒱).ι ''ᵁ U i =
      ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange := by
    rw [Scheme.Hom.image_preimage_eq_opensRange_inf, inf_eq_right, Opens.opensRange_ι]
    exact le_iSup (fun i : Σ i, (𝒱 i).I₀ ↦ ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange) i
  have hf : iSup U = ⊤ := (TopologicalSpace.Opens.map_iSup _ _).symm.trans
    (diagonalCoverDiagonalRange f 𝒰 𝒱).ι_preimage_self
  rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsClosedImmersion) _ hf]
  intro i
  rw [MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictRestrict _ _ _),
    MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (morphismRestrictEq _ (hU i)),
    MorphismProperty.arrow_mk_iso_iff (P := @IsClosedImmersion) (diagonalRestrictIsoDiagonal ..)]
  infer_instance

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 := 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
this : IsDominant (Over.Hom.left (equalizer.ι f' g'))
⊢ f = g

Tactic:
have : Surjective (equalizer.ι f' g').left :=
    surjective_of_isDominant_of_isClosed_range _ (Scheme.Hom.isClosedEmbedding _).isClosed_range

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
this✝ : IsDominant (Over.Hom.left (equalizer.ι f' g'))
this : Surjective (Over.Hom.left (equalizer.ι f' g'))
⊢ f = g
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.app f U))

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally @IsClosedImmersion]
  exact targetAffineLocally_affineAnd_iff' RingHom.surjective_respectsIso _

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

Goal state before:
pp: X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst✝¹ : IsSeparated i
inst✝ : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
x : ↥X
hx : x ∈ S
⊢ (equalizer.ι f g) ((equalizer.lift (X.fromSpecResidueField x) ⋯) default) = x

Tactic:
← Scheme.Hom.comp_apply,

Goal state after:
X Y Z : Scheme
f g : X ⟶ Y
i : Y ⟶ Z
inst✝¹ : IsSeparated i
inst✝ : IsReduced X
S : Set ↥X
hS' : Dense S
H : ∀ x ∈ S, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
H' : f ≫ i = g ≫ i
x : ↥X
hx : x ∈ S
⊢ (equalizer.lift (X.fromSpecResidueField x) ⋯ ≫ equalizer.ι f g) default = x
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : X.IsSeparated
⊢ IsSeparated f

Tactic:
apply +allowSynthFailures @IsSeparated.of_comp (g := terminal.from Y)
  rw [terminal.comp_from]
  infer_instance

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
inst✝ : Algebra.FinitePresentation R S
⊢ IsOpenMap (comap (algebraMap R S))

Tactic:
by
  rw [isBasis_basic_opens.isOpenMap_iff]
  rintro _ ⟨_, ⟨f, rfl⟩, rfl⟩
  exact isOpen_of_stableUnderGeneralization_of_isConstructible
    ((basicOpen f).2.stableUnderGeneralization.image
      (Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp ‹_›))
    (isConstructible_comap_image (RingHom.finitePresentation_algebraMap.mpr ‹_›)
      isConstructible_basicOpen)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ @LocallyOfFinitePresentation = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation

Tactic:
ext X Y f

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFinitePresentation f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ Subtype.val '' Subtype.val ⁻¹' ⇑f '' s =
    Subtype.val ''
      ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
        ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ Set.range Subtype.val =
    Subtype.val ''
      ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i))) ''
        ⇑(Cover.pullbackHom Y.affineCover f i) '' ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent (e ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f))

Tactic:
AlgEquiv.commutes,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField)) f)
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)ᶜ
x✝ : ↑↑t
⊢ IsCompact (zeroLocus {↑x✝})ᶜ

Tactic:
simpa using isCompact_basicOpen _

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

Goal state before:
pp: X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ ⇑(TopCat.Hom.hom f.base) '' (s ∩ ↑(opensRange (𝒰.f i))) =
    ⇑(TopCat.Hom.hom f.base) '' ⇑(TopCat.Hom.hom (𝒰.f i).base) '' ⇑(𝒰.f i) ⁻¹' s

Tactic:
Set.image_preimage_eq_inter_range,

Goal state after:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst✝ : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ ⇑(TopCat.Hom.hom f.base) '' (s ∩ ↑(opensRange (𝒰.f i))) =
    ⇑(TopCat.Hom.hom f.base) '' (s ∩ Set.range ⇑(TopCat.Hom.hom (𝒰.f i).base))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
rw [Opens.map_coe, ← Set.preimage_inter_range]

Goal state after:
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (⇑f ⁻¹' (↑U ∩ Set.range ⇑f))
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)

Tactic:
by
  refine ⟨fun h ↦ inferInstance, fun H ↦ ?_⟩
  refine IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.mpr ⟨?_, ?_⟩
  · exact (isLocallyNoetherian_iff_openCover 𝒰).mpr inferInstance
  · refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    simpa using (𝒰.f i).isOpenEmbedding.isOpenMap _ (isOpen_discrete {x})

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

Goal state before:
pp: P : ObjectProperty Scheme
⊢ geometrically P = MorphismProperty.universally fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X

Tactic:
ext X Y f

Goal state after:
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔ MorphismProperty.universally (fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: ⊢ @UniversallyOpen = (topologically @IsOpenMap).universally

Tactic:
ext X Y f

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyOpen f ↔ (topologically @IsOpenMap).universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: ⊢ @UniversallyClosed = (topologically @IsClosedMap).universally

Tactic:
ext X Y f

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ (topologically @IsClosedMap).universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ @Flat = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Flat

Tactic:
ext X Y f

Goal state after:
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ Flat f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Flat) f