mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
a : ↑s
⊢ IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)

Tactic:
convert! (inferInstance : IsLocalization.Away (rₐ a) (Sₐ a))

Goal state after:
case e'_3
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := ⋯
Sₐ : ↑s → Type u := ⋯
this : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
a : ↑s
⊢ Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r)) = Submonoid.powers (rₐ a)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
⊢ ∀ (𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X), P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)

Tactic:
𝒰

Goal state after:
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
⊢ P.universally f ↔ ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (b : { V // ↑V ≤ f ⁻¹ᵁ U }),
      P (CommRingCat.Hom.hom (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm b)) ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Tactic:
Subtype.forall

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (a : ↑X.affineOpens) (b : ↑a ≤ f ⁻¹ᵁ U),
      P
        (CommRingCat.Hom.hom
          (Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ↑((affineOpensRestrict (f ⁻¹ᵁ U)).symm ⟨a, b⟩)) ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
⊢ ∃ s, s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, ↑i

Tactic:
have : Finite s := hs.to_subtype

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact ↑U
f : ↑Γ(X, U)
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i ∈ s, ↑i
g : ↑s → ↑X.affineOpens := fun V ↦ ⟨↑↑V ⊓ X.basicOpen f, ⋯⟩
this : Finite ↑s
⊢ ∃ s, s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, ↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h₇₅
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₁) ⋯)

Tactic:
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]

Goal state after:
case h₇₅
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ ↑S ⊓ X.basicOpen f ≤ U₁ ⊓ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case h₇₆
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ X.basicOpen ((f |_ ↑S) ⋯) ≤ X.basicOpen ((f |_ U₂) ⋯)

Tactic:
simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]

Goal state after:
case h₇₆
X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ ↑S ⊓ X.basicOpen f ≤ U₂ ⊓ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case basicOpen
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen r) ⋯))

Tactic:
← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op

Goal state after:
case basicOpen
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
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H✝ : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
U : ↑X.affineOpens
r : ↑Γ(X, ↑U)
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯ ≫ X.presheaf.map (homOfLE ⋯).op))
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
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ ∀ (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)

Tactic:
𝒰

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
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
𝒰 : X.OpenCover
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.primeHeight = ringKrullDim R
⊢ ↑I.height = ringKrullDim R

Tactic:
by simpa [Ideal.height_eq_primeHeight]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : Ideal R
n : ℕ
inst✝ : p.IsPrime
⊢ (∀ (b : { I // I.IsPrime }),
      (PrimeSpectrum.equivSubtype R).symm b < { asIdeal := p, isPrime := inst✝ } →
        Order.height ((PrimeSpectrum.equivSubtype R).symm b) < ↑n) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

Tactic:
Subtype.forall

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : Ideal R
n : ℕ
inst✝ : p.IsPrime
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      (PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩ < { asIdeal := p, isPrime := inst✝ } →
        Order.height ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩) < ↑n) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
← basicOpen_eq_bot_iff,

Goal state after:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
e : a * b = 0
⊢ X.basicOpen a = ⊥ ∨ X.basicOpen b = ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case hQi
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
this✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q

Tactic:
apply (isLocal_ringHomProperty P (Q := Q)).respectsIso

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U

Tactic:
simp only [radical_ideal, ideal_inf, Pi.inf_apply, Ideal.radical_inf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (stalkClosedPointIso R).inv = StructureSheaf.toStalk (↑R) (closedPoint ↑R)

Tactic:
ext x
  exact (StructureSheaf.stalkIso _ _).commutes _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

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

Tactic:
← Iso.inv_comp_eq,

Goal state after:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ (ΓSpecIso R).inv ≫
      Hom.app (Spec.map φ) ⊤ ≫
        (Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom =
    φ
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Module.finrank ↑(X.residueField x) ↑(X.residueField x) = 1

Tactic:
rw [residueFieldMap_id]

Goal state after:
X : Scheme
x : ↥X
⊢ Module.finrank ↑(X.residueField x) ↑(X.residueField x) = 1
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
⊢ (I.glueData.ι ia) a = (I.glueData.ι ib) b

Tactic:
obtain ⟨f, g, hfg, H⟩ := exists_basicOpen_le_affine_inter ia.2 ib.2
    (I.glueDataObjι ia a).1
      ⟨(I.glueDataObjι ia a).2, this ▸ (I.glueDataObjι ib b).2⟩

Goal state after:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
b : ↥(I.glueDataObj ib)
e :
  I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ia))) a) =
    I.gluedTo ((ConcreteCategory.hom (forget.map (I.glueData.ι ib))) b)
this : ↑((I.glueDataObjι ia) a) = ↑((I.glueDataObjι ib) b)
f : ↑Γ(X, ↑ia)
g : ↑Γ(X, ↑ib)
hfg : X.basicOpen f = X.basicOpen g
H : ↑((I.glueDataObjι ia) a) ∈ X.basicOpen f
⊢ (I.glueData.ι ia) a = (I.glueData.ι ib) b
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
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : ↑Y.affineOpens
⊢ IsAffine ↑(f ⁻¹ᵁ ↑U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U).ι ''ᵁ ⊤)))

Tactic:
· refine ⟨(h U U.2).1, ?_⟩
    change Q (Scheme.Hom.app f ((U : Y.Opens).ι ''ᵁ ⊤)).hom
    rw [Scheme.Opens.ι_image_top]
    exact (h U U.2).2

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
⊢ ∀ (x : ↥Y), ∃ U, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
intro y

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
y : ↥Y
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ pullback.fst (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.glueDataObjι U ≫ (↑U).ι =
    pullback.snd (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.glueDataObjι V ≫ (↑V).ι

Tactic:
← subschemeCover_map_subschemeι,

Goal state after:
X : Scheme
I✝ I J : X.IdealSheafData
h : I ≤ J
U V : J.subschemeCover.openCover.I₀
⊢ pullback.fst (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.subschemeCover.f U ≫ J.subschemeι =
    pullback.snd (J.subschemeCover.f U) (J.subschemeCover.f V) ≫ J.glueDataObjι V ≫ (↑V).ι
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case inr
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme},
    HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Q) →
        ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ g ⁻¹ᵁ ↑U ≫ g ∣_ ↑U)

Tactic:
exact this hA hQ _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2

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

Goal state before:
pp: case 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
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} fun x ↦ x ∈ Set.range (unop ∘ F.obj)

Tactic:
refine CommRingCat.essentiallySmall_of_localizationAway (Q := Q'.isoClosure) ?_

Goal state after:
case 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
Q' : ObjectProperty CommRingCat := fun S ↦ ∃ R ∈ Set.range fun U ↦ Γ(X, U), ∃ f, (CommRingCat.Hom.hom f).FiniteType
this : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q'
⊢ ∀ S ∈ Set.range (unop ∘ F.obj), ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q'.isoClosure (CommRingCat.of (Localization.Away f))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h✝ : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h✝ True.intro
h : IsIso f'
⊢ IsIso f

Tactic:
← isIso_iff_of_reflects_iso _ (MorphismProperty.Over.forget ..),

Goal state after:
Z₁ Z₂ X : Scheme
i₁ : Z₁ ⟶ X
i₂ : Z₂ ⟶ X
inst✝¹ : IsClosedImmersion i₁
inst✝ : IsClosedImmersion i₂
f : Z₁ ⟶ Z₂
h✝ : f ≫ i₂ = i₁
h' : Scheme.Hom.ker i₁ = Scheme.Hom.ker i₂
f' : MorphismProperty.Over.mk ⊤ i₁ inst✝¹ ⟶ MorphismProperty.Over.mk ⊤ i₂ inst✝ :=
  MorphismProperty.Over.homMk f h✝ True.intro
h : IsIso ((MorphismProperty.Over.forget @IsClosedImmersion ⊤ X).map f')
⊢ IsIso f
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
⊢ f = g

Tactic:
let X' : Over Z := Over.mk (f ≫ s)

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)
⊢ f = g
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)
⊢ f = g

Tactic:
let Y' : Over Z := Over.mk s

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
⊢ f = g
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:
rw [← Scheme.Hom.comp_apply, equalizer.lift_ι, Scheme.fromSpecResidueField_apply]

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

Goal state before:
pp: case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H :
  ¬∀ ⦃I : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)⦄,
      I ∈ {J | J.IsPrime} → (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∈ I
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})

Tactic:
simp only [Set.mem_ofPred_eq, Algebra.TensorProduct.algebraMap_apply,
      Ideal.Quotient.algebraMap_eq, not_forall] at H

Goal state after:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
H : ∃ x_1, ∃ (_ : x_1.IsPrime), (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ x_1
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})
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)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
⊢ ∀ (x : ↥Y), x ∈ closure (Set.range ⇑g)

Tactic:
intro y

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
y : ↥Y
⊢ y ∈ closure (Set.range ⇑g)
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

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

Tactic:
and_iff_right (by infer_instance),

Goal state after:
R S : CommRingCat
f : R ⟶ S
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔ (CommRingCat.Hom.hom f).Finite
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (terminal.from X)

Tactic:
rw [← terminal.comp_from X.toSpecΓ]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsSeparated (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsIso (Hom.ker X.toSpecΓ).subschemeι

Tactic:
X.ker_toSpecΓ

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : X.IsQuasiAffine
⊢ IsIso ⊥.subschemeι
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
i : X.affineCover.I₀
⊢ Flat (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)

Tactic:
← Spec.map_preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom),

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝¹ : Subsingleton ↥Y
inst✝ : IsIntegral Y
i : X.affineCover.I₀
⊢ Flat (Spec.map (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)))