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

Goal state before:
pp: case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (pullback.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫ pullback.fst (𝒰.f i ≫ f) g =
    ((((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
            pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
          (pullbackSymmetry s.fst (𝒰.f i)).hom) ≫
        pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g

Tactic:
simp_rw [Category.assoc, pullbackP1Iso_hom_fst, pullback.lift_fst, Category.comp_id,
      pullbackSymmetry_hom_comp_fst, pullback.lift_snd, Category.comp_id,
      pullbackRightPullbackFstIso_hom_snd]

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
X : Scheme
ι : Type v
inst✝ : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
hf : ∀ (i : ι), P (f i)
⊢ P (Sigma.desc f)

Tactic:
by
  rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Scheme.IsLocallyDirected.openCover _)]
  exact fun i ↦ by simp [hf]

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

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
⊢ P ((f ≫ e.hom) ∣_ U)

Tactic:
have : IsAffine _ := hU.preimage_of_isIso e.hom

Goal state after:
case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine ↑(e.hom ⁻¹ᵁ U)
⊢ P ((f ≫ e.hom) ∣_ U)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).OpenCover

Tactic:
by
  apply (openCoverOfLeft (𝒰.pullback₁ f) f g).bind
  intro i
  haveI := ((IsPullback.of_hasPullback (pullback.snd g (𝒰.f i))
    (pullback.snd f (𝒰.f i))).paste_horiz (IsPullback.of_hasPullback _ _)).flip
  refine
    @coverOfIsIso _ _ _ _ _
      (f := (pullbackSymmetry (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).hom ≫
        (limit.isoLimitCone ⟨_, this.isLimit⟩).inv ≫
        pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_) inferInstance
  · simp [← pullback.condition]
  · simp only [Category.comp_id, Category.id_comp]

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

Goal state before:
pp: X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U V : Set ↥X
hU : IsOpen U
hU' : IsCompact U
hV : IsOpen V
hV' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated ↑U
⊢ IsQuasiSeparated ↑(f ⁻¹ᵁ U)

Tactic:
have : QuasiSeparatedSpace U := (isQuasiSeparated_iff_quasiSeparatedSpace _ U.2).mp hU
  exact (isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ IsMin { asIdeal := I, isPrime := inst✝ } ↔ I ∈ minimalPrimes R

Tactic:
minimalPrimes_eq_minimals

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ IsMin { asIdeal := I, isPrime := inst✝ } ↔ I ∈ {x | Minimal IsPrime x}
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ⊥.height = 0

Tactic:
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes (R := R) (I := ⊥) top_ne_bot.symm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : Ideal R
hp : p ∈ ⊥.minimalPrimes
⊢ ⊥.height = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : Subsingleton R
⊢ I.height = ⊤

Tactic:
rw [Subsingleton.elim I ⊤, Ideal.height_top]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsMaximal), i'.height

Tactic:
obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top

Goal state after:
case a.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hIM : I ≤ M
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsMaximal), i'.height
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y

Tactic:
← sub_eq_zero,

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x - (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y = 0 → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y

Tactic:
RingHom.algebraMap_toAlgebra

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ U ⊓ X.basicOpen x = ⊥ → X.basicOpen x = ⊥

Tactic:
contrapose!

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥

Tactic:
simp_rw [Ne, ← Opens.not_nonempty_iff_eq_bot, Classical.not_not]

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ (↑(X.basicOpen x)).Nonempty → (↑(U ⊓ X.basicOpen x)).Nonempty
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e'
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
intro R S _ _ f
      exact (locally_iff_of_localizationSpanTarget (isLocal_ringHomProperty P).respectsIso
        (isLocal_ringHomProperty P).ofLocalizationSpanTarget _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁ = Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Tactic:
← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op,

Goal state after:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
trans x ∈ X.zeroLocus (U := U.1) (vanishingIdeal (U.2.fromSpec ⁻¹' Z)) ∩ U.1

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

X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) ∩ ↑↑U ↔
    x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z))
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : (X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫ (X.presheaf.stalkCongr ⋯).hom

Tactic:
simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes]

Goal state after:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : (X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
← SpecMap_stalkMap_fromSpecStalk,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (residueFieldMap f x) ≫ Spec.map (Y.residue (f x)) ≫ Y.fromSpecStalk (f x) =
    Spec.map (X.residue x) ≫ Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x)
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsEmpty ↥(pullback f g) → ∀ ⦃a : ↥S⦄, a ∈ Set.range ⇑f → ∀ ⦃b : ↥S⦄, b ∈ Set.range ⇑g → a ≠ b

Tactic:
contrapose!

Goal state after:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ (∃ a ∈ Set.range ⇑f, ∃ b ∈ Set.range ⇑g, a = b) → Nonempty ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case respectsIso.h₁
X✝ Y✝ Z✝ : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y Z : Scheme
e : X ≅ Y
f✝ : Y ⟶ Z
inst✝ : IsAffine Z
H : IsAffine Y
⊢ IsAffine X

Tactic:
have : IsAffine _ := H

Goal state after:
case respectsIso.h₁
X✝ Y✝ Z✝ : Scheme
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
X Y Z : Scheme
e : X ≅ Y
f✝ : Y ⟶ Z
inst✝ : IsAffine Z
H this : IsAffine Y
⊢ IsAffine X
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: ⊢ MorphismProperty.IsStableUnderBaseChange @Surjective

Tactic:
by
  refine .mk' ?_
  introv hg
  simp only [surjective_iff, ← Set.range_eq_univ, Scheme.Pullback.range_fst] at hg ⊢
  rw [hg, Set.preimage_univ]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
a : ↥(I.glueDataObj (X.affineBasicOpen f))
H : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) ∈ X.basicOpen f
b : ↥(I.glueDataObj (X.affineBasicOpen f))
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), (I.glueDataObjMap ⋯) b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) ((I.glueDataObjMap ⋯) a)) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) ((I.glueDataObjMap ⋯) b))
this : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) = ↑((I.glueDataObjι ib) ((I.glueDataObjMap ⋯) b))
⊢ (I.glueData.ι ia) ((I.glueDataObjMap ⋯) a) = (I.glueData.ι ib) ((I.glueDataObjMap ⋯) b)

Tactic:
simp only [glueData_U, ← Scheme.Hom.comp_apply, glueDataObjMap_glueDataObjι] at this ⊢

Goal state after:
X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
a : ↥(I.glueDataObj (X.affineBasicOpen f))
H : ↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) ∈ X.basicOpen f
b : ↥(I.glueDataObj (X.affineBasicOpen f))
hmem : ∀ (W : ↑X.affineOpens) (hW : W = X.affineBasicOpen g), (I.glueDataObjMap ⋯) b ∈ Set.range ⇑(I.glueDataObjMap ⋯)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) ((I.glueDataObjMap ⋯) a)) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) ((I.glueDataObjMap ⋯) b))
this :
  ↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯) a) = ↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯) b)
⊢ (I.glueDataObjMap ⋯ ≫ I.glueData.ι ia) a = (I.glueDataObjMap ⋯ ≫ I.glueData.ι ib) b
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
⊢ IsAffineHom f

Tactic:
apply isAffineHom_of_forall_exists_isAffineOpen
  intro y
  by_cases hy : y ∈ Set.range f
  · obtain ⟨x, rfl⟩ := hy
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen
    obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V := by
      obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
      exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩
    obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f x, hxV⟩ hxU
    refine ⟨_, hxr, hU.basicOpen r, ?_⟩
    convert hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r))
    simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]
    simpa using ((Opens.map f.base).map (homOfLE hrU')).le
  · obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open hy hf₂.isOpen_compl
    rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'
    refine ⟨U, hyU, hU, ?_⟩
    convert isAffineOpen_bot _
    exact Opens.ext hU'

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
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
⊢ P = @IsAffineHom ⊓ P'

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    targetAffineLocally_affineAnd_eq_affineLocally,
    HasRingHomProperty.eq_affineLocally (P := P')]

Goal state after:
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
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝³ : Algebra R S := f.toAlgebra
this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝¹ : Algebra R' S' := f'.toAlgebra
this✝ : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ IsLocalization (Submonoid.map (algebraMap R S) M) S'

Tactic:
RingHom.algebraMap_toAlgebra

Goal state after:
R S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝³ : Algebra R S := f.toAlgebra
this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝¹ : Algebra R' S' := f'.toAlgebra
this✝ : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ IsLocalization (Submonoid.map f M) S'
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_2.refine_1
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ Scheme.Spec.map e.hom ≫
      (MorphismProperty.CostructuredArrow.mk ⊤ ↑⟨Spec.map e.inv.unop ≫ S.hom, ?refine_2.refine_2⟩ ⋯).hom =
    S.hom

pp: case refine_2.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.hom)

Tactic:
· simp [← Spec.map_comp_assoc, F]

Goal state after:
case refine_2.refine_2
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst✝ : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
x✝ : (fun x ↦ Nonempty (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.hom)
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)
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
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    Set.range
      ⇑(pullback.map ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) ((𝒱 i).f j ≫ Cover.pullbackHom 𝒰 f i) f f
          ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) (𝒰.f i) ⋯ ⋯)

Tactic:
rw [range_map]

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
j : (𝒱 i).I₀ := Cover.idx (𝒱 i) z
w : ↥((𝒱 i).X j)
hy : ((𝒱 i).f j) w = z
⊢ x ∈
    ⇑(pullback.fst f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i)) ∩
      ⇑(pullback.snd f f) ⁻¹' Set.range ⇑((𝒱 i).f j ≫ pullback.fst f (𝒰.f i))
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
⊢ ι' ≫ f' = ι' ≫ g'

Tactic:
· ext1; exact hU

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

Goal state before:
pp: case inr
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
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
refine .of_isOpenCover Y.affineCover.isOpenCover_opensRange fun i ↦ ?_

Goal state after:
case inr
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₀
⊢ IsLocallyConstructible (Subtype.val ⁻¹' ⇑f '' s)
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 ?_)
    let e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField]
        MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
    rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm ..).injective,
      ← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]
    change (e.toAlgHom.toRingHom.comp (Algebra.TensorProduct.comm ..).toRingHom).comp
      (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0
    congr!
    ext
    · simp [scalarRTensorAlgEquiv, e, Algebra.smul_def]
    · simp [e, scalarRTensorAlgEquiv, coeff, map, X, monomial]

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

Goal state before:
pp: P : ObjectProperty Scheme
X Y✝ : Scheme
f : X ⟶ Y✝
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y✝), P (pullback f y)
K : Type u
x✝¹ : Field K
x✝ : Spec (of K) ⟶ Y✝
Y : Scheme
fst : Y ⟶ X
snd : Y ⟶ Spec (of K)
h : IsPullback fst snd f x✝
⊢ P Y

Tactic:
exact P.prop_of_iso h.isoPullback.symm (H _ _)

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
⊢ IsOpenMap ⇑f

Tactic:
by
  change topologically IsOpenMap f
  wlog hY : ∃ R, Y = Spec R
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically IsOpenMap) Y.affineCover]
    intro i
    dsimp only [Scheme.Cover.pullbackHom]
    refine this _ ?_ ⟨_, rfl⟩
    exact IsZariskiLocalAtTarget.of_isPullback (P := topologically GeneralizingMap)
      (iY := Y.affineCover.f i) (IsPullback.of_hasPullback ..) hf
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · rw [IsZariskiLocalAtSource.iff_of_openCover (P := topologically IsOpenMap) X.affineCover]
    intro i
    refine this f _ _ ?_ ⟨_, rfl⟩
    exact IsZariskiLocalAtSource.comp (P := topologically GeneralizingMap) hf _
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
  algebraize [φ.hom]
  convert! PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
  · rwa [Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap]
  · apply (HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)).mp inferInstance

Goal state after: