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

Goal state before:
pp: case refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
    IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩ <;>
        ext x <;> obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x <;> simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this✝ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
this : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))

Tactic:
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) :=
      IsOpenImmersion.of_isLocalization (1, 0)

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
this✝¹ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inl x)
this✝ : Algebra (R × S) R := (RingHom.fst R S).toAlgebra
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.fst R S)))
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.fst R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inl x))
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
i : 𝒰.I₀
⊢ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
      pullback.snd (𝒰.f i ≫ f) g =
    pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g

Tactic:
pullback.lift_snd

Goal state after:
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
i : 𝒰.I₀
⊢ pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫ pullback.snd (p1 𝒰 f g) (𝒰.f i) =
    pullback.fst (𝒰.f i ≫ f) g

Tactic:
pullback.lift_snd

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H.mpr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
x y : (a : ι) → R a
e : Function.update 0 i 1 * x = Function.update 0 i 1 * y
⊢ (algebraMap ((a : ι) → R a) (R i)) x = (algebraMap ((a : ι) → R a) (R i)) y

Tactic:
simpa using! congr_fun e i

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case H'
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := ⋯
⊢ Function.Surjective ⇑(algebraMap ((a : ι) → R a) (R i))

Tactic:
· exact Function.surjective_eval _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ iSup U = Scheme.Hom.opensRange (Sigma.desc fun i ↦ (U i).ι)

pp: ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ IsAffine (∐ fun i ↦ ↑(U i))

Tactic:
· ext
    simp [(sigmaMk _).symm.exists_congr_left, ← Scheme.Hom.comp_apply, Scheme.Opens.exists_toScheme]

Goal state after:
ι : Type u
X : Scheme
inst✝ : Finite ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
this : IsOpenImmersion (Sigma.desc fun i ↦ (U i).ι)
⊢ IsAffine (∐ fun i ↦ ↑(U i))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = ⨆ i, U i

Tactic:
simp [Scheme.Hom.image_preimage_eq_opensRange_inf, le_iSup U]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)

Tactic:
let e : Localization.Away t ≃+* Sₜ :=
      (IsLocalization.algEquiv (Submonoid.powers t) _ _).toRingEquiv

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
e : Localization.Away t ≃+* Sₜ := (IsLocalization.algEquiv (Submonoid.powers t) (Localization.Away t) Sₜ).toRingEquiv
⊢ P ((algebraMap S Sₜ).comp f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
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)
this✝¹ :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
H : ∀ (a : ↑s), Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))
this✝ : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
⊢ Ideal.span (Set.range fun a ↦ (algebraMap S S') ↑a) = ⊤

Tactic:
rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
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'
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)
Mₐ : (a : ↑s) → Submonoid (Localization.Away ↑a) :=
  fun a ↦ Submonoid.map (algebraMap S (Localization.Away ↑a)) (Submonoid.map f M)
Sₐ : ↑s → Type u := fun a ↦ Localization (Mₐ a)
hM : ∀ (a : ↑s), Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M = Mₐ a
this✝² : ∀ (a : ↑s), IsLocalization (Submonoid.map ((algebraMap S (Localization.Away ↑a)).comp f) M) (Sₐ a)
this✝¹ : ∀ (a : ↑s), IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f M)) (Sₐ a)
this✝ : (a : ↑s) → Algebra S' (Sₐ a) :=
  fun a ↦ (IsLocalization.map (Sₐ a) (algebraMap S (Localization.Away ↑a)) ⋯).toAlgebra
this : ∀ (a : ↑s), IsScalarTower S S' (Sₐ a)
⊢ Ideal.span (Set.range fun a ↦ (algebraMap S S') ↑a) = ⊤

Tactic:
rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ x = 0

Tactic:
rw [← (IsLocalization.map_units S m).mul_left_inj, hx, zero_mul,
    IsLocalization.map_eq_zero_iff M]

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ ∃ m, ↑m * y = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ Order.krullDim ↑(Set.Iic { asIdeal := J, isPrime := inst✝ }) =
    Order.krullDim ↑(Set.Iic { asIdeal := comap (algebraMap R A) J, isPrime := ⋯ })

Tactic:
let e := IsLocalization.orderIsoOfPrime S A

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
e : { p // p.IsPrime } ≃o { p // p.IsPrime ∧ Disjoint ↑S ↑p } := orderIsoOfPrime S A
⊢ Order.krullDim ↑(Set.Iic { asIdeal := J, isPrime := inst✝ }) =
    Order.krullDim ↑(Set.Iic { asIdeal := comap (algebraMap R A) J, isPrime := ⋯ })
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hP : 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 : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z), P f → P g → IsAffine Z → P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
      intro U
      rw [morphismRestrict_comp]
      exact this _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2

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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
this : ∀ {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z}, P (f ≫ g) → IsAffine Z → P f
hZ : ¬IsAffine Z
⊢ P f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _
      (g.iSup_preimage_eq_top (iSup_affineOpens_eq_top Z))]
    intro U
    have H := IsZariskiLocalAtTarget.restrict h U.1
    rw [morphismRestrict_comp] at H
    exact this H inferInstance

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
⊢ x ∉ X.basicOpen s

Tactic:
hxs

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ J.support ≤ I.support

Tactic:
← SetLike.coe_subset_coe,

Goal state after:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ ↑J.support ⊆ ↑I.support
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ (Ideal.Quotient.mk (I.ideal U)).comp (algebraMap ↑Γ(X, ↑V) ↑Γ(X, ↑U)) =
    (algebraMap (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U)).comp (Ideal.Quotient.mk (I.ideal V))

pp: case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ RingHom.ker (Ideal.Quotient.mk (I.ideal U)) ≤
    Ideal.map (algebraMap ↑Γ(X, ↑V) ↑Γ(X, ↑U)) (RingHom.ker (Ideal.Quotient.mk (I.ideal V)))

Tactic:
· simp [RingHom.algebraMap_toAlgebra, Ideal.quotientMap_comp_mk]; rfl

Goal state after:
case refine_2
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ RingHom.ker (Ideal.Quotient.mk (I.ideal U)) ≤
    Ideal.map (algebraMap ↑Γ(X, ↑V) ↑Γ(X, ↑U)) (RingHom.ker (Ideal.Quotient.mk (I.ideal V)))
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
s : ↑Γ(Y, U)
hs : s ∈ (ker f).ideal ⟨U, hU⟩
⊢ f x ∉ Y.basicOpen s

Tactic:
hxs

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

Goal state before:
pp: X : Scheme
x y : ↥X
h : x = y
⊢ X.residue x ≫ (residueFieldCongr h).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue y

Tactic:
subst h
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.RightInverse (fun T ↦ T.fst.SpecTensorTo T.snd) fun t ↦ ⟨Triplet.ofPoint t, SpecOfPoint t⟩

Tactic:
intro ⟨T, p⟩
    apply carrierEquiv_eq_iff.mpr
    use T.ofPoint_SpecTensorTo p
    have : Spec.map (Hom.residueFieldMap T.SpecTensorTo p) (⊥ : PrimeSpectrum _) =
        (⊥ : PrimeSpectrum _) :=
      (PrimeSpectrum.instUnique).uniq _
    simp only [SpecOfPoint, Triplet.tensorCongr_inv, ← this, ← Scheme.Hom.comp_apply,
      ← Scheme.Hom.comp_apply]
    simp [Triplet.Spec_ofPointTensor_SpecTensorTo]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsEmpty ↥(pullback f g) ↔ Disjoint (Set.range ⇑f) (Set.range ⇑g)

Tactic:
refine ⟨?_, Scheme.isEmpty_pullback f g⟩
  rw [Set.disjoint_iff_forall_ne]
  contrapose!
  rintro ⟨_, ⟨x, rfl⟩, _, ⟨y, rfl⟩, e⟩
  obtain ⟨z, -⟩ := exists_preimage_pullback x y e
  exact ⟨z⟩

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
⊢ IsIso (f ∣_ U) ↔ IsIso (Scheme.Hom.app f U)

Tactic:
have : IsAffine U := hU
  refine (HasAffineProperty.iff_of_isAffine (P := .isomorphisms _)).trans <|
    (and_iff_right (hU.preimage f)).trans ?_
  rw [Scheme.Hom.app_eq_appLE]
  simp only [morphismRestrict_app', TopologicalSpace.Opens.map_top]
  congr! <;> simp [Scheme.Opens.toScheme_presheaf_obj]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ SurjectiveOnStalks f ∧ IsClosedEmbedding ⇑f ↔ (SurjectiveOnStalks f ∧ IsEmbedding ⇑f) ∧ IsClosed (Set.range ⇑f)

Tactic:
and_assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ SurjectiveOnStalks f ∧ IsClosedEmbedding ⇑f ↔ SurjectiveOnStalks f ∧ IsEmbedding ⇑f ∧ IsClosed (Set.range ⇑f)
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
⊢ ∃ y, ((diagonalCover f 𝒰 𝒱).f ⟨i, (j, j)⟩) y = x

Tactic:
diagonalCover_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
⊢ ∃ y,
    (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) ⋯ ⋯)
        y =
      x
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
⊢ IsImmersion (pullback.diagonal f)

Tactic:
have := isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange f 𝒰 𝒱

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover := Y.affineCover
𝒱 : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover := fun i ↦ (pullback f (𝒰.f i)).affineCover
H : pullback.diagonal f ⁻¹ᵁ diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
this : IsClosedImmersion (pullback.diagonal f ∣_ diagonalCoverDiagonalRange f 𝒰 𝒱)
⊢ IsImmersion (pullback.diagonal f)
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
⊢ ∀ s ∈ SetLike.coe '' Set.range basicOpen, IsOpen (comap (algebraMap R S) '' s)

Tactic:
rintro _ ⟨_, ⟨f, rfl⟩, rfl⟩

Goal state after:
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
f : S
⊢ IsOpen (comap (algebraMap R S) '' ↑(basicOpen f))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
⊢ Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)

Tactic:
rwa [Ideal.span_le, Ideal.ker_algebraMap_residueField]

Goal state after:
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))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    (Subtype.val ∘ ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i)))) ∘ ⇑(Cover.pullbackHom Y.affineCover f i) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
change _ = (Y.affineCover.pullbackHom f i ≫
      (Y.affineCover.f i).isoOpensRange.hom ≫ Opens.ι _).base.hom '' _

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 ∩ ↑(opensRange (Y.affineCover.f i)) =
    ⇑(TopCat.Hom.hom
          (Cover.pullbackHom Y.affineCover f i ≫
              (isoOpensRange (Y.affineCover.f i)).hom ≫ (opensRange (Y.affineCover.f i)).ι).base) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case basicOpen
X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
hN : IsNoetherianRing ↑Γ(X, ↑U)
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ IsNoetherianRing ↑Γ(X, ↑(X.affineBasicOpen f))

Tactic:
exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN

Goal state after: