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

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : (Scheme.Cover.ulift 𝒰).I₀
⊢ P ((Scheme.Hom.opensRange ((Scheme.Cover.ulift 𝒰).f i)).ι ≫ f)

Tactic:
dsimp

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
i : (Scheme.Cover.ulift 𝒰).I₀
⊢ P ((Scheme.Hom.opensRange (𝒰.f (Scheme.Cover.idx 𝒰 i))).ι ≫ f)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
⊢ IsOpenImmersion
    ({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
          f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
      i)

Tactic:
dsimp

Goal state after:
case refine_2
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i :
  { I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
      f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.I₀
⊢ IsOpenImmersion (pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
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✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
      (Cover.pushforwardIso (openCoverOfLeft 𝒰 g f) (pullbackSymmetry g f).hom).f ((Equiv.refl 𝒰.I₀) i)

Tactic:
dsimp

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : Y.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map f (𝒰.f i ≫ g) f g (𝟙 X) (𝒰.f i) (𝟙 Z) ⋯ ⋯ =
    (pullbackSymmetry f (𝒰.f i ≫ g)).hom ≫
      pullback.map (𝒰.f i ≫ g) f g f (𝒰.f i) (𝟙 X) (𝟙 Z) ⋯ ⋯ ≫ (pullbackSymmetry g f).hom
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, hU⟩)

Tactic:
dsimp

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
⊢ P ((f ≫ e.hom) ∣_ U)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z W : Scheme
fWX : W ⟶ X
fWY : W ⟶ Y
fXZ : X ⟶ Z
fYZ : Y ⟶ Z
𝒰 : X.OpenCover
H :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom 𝒰 fWX i) ((Precoverage.ZeroHypercover.pullback₁ fWX 𝒰).f i ≫ fWY) (𝒰.f i ≫ fXZ) fYZ
h : fWX ≫ fXZ = fWY ≫ fYZ
i : (openCoverOfLeft 𝒰 fXZ fYZ).toPreZeroHypercover.1
f : pullback (𝒰.f i ≫ fXZ) fYZ ⟶ pullback fXZ fYZ := pullback.map (𝒰.f i ≫ fXZ) fYZ fXZ fYZ (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ fXZ) fYZ) f (𝒰.f i) (pullback.fst fXZ fYZ)
⊢ pullback.fst fWX (𝒰.f i) ≫ pullback.lift fWX fWY h =
    pullback.lift (pullback.snd fWX (𝒰.f i)) (pullback.fst fWX (𝒰.f i) ≫ fWY) ⋯ ≫ f

Tactic:
ext <;> simp [f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
m : (forgetToLocallyRingedSpace.mapCocone (cocone F)).pt ⟶ s.pt
hm : ∀ (j : J), (forgetToLocallyRingedSpace.mapCocone (cocone F)).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).toLocallyRingedSpaceGlueData.J).R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ (algebraMap S (S ⊗[R] T)) (y • x) = x ⊗ₜ[R] (algebraMap R T) y

Tactic:
dsimp

Goal state after:
case h
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : R
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] (algebraMap R T) y
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P (algebraMap S (Localization.Away (1 ⊗ₜ[R] g)))

Tactic:
rw [← e.toAlgHom.comp_algebraMap]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R T)
g : T
hg : P (algebraMap R (Localization.Away g))
e : S ⊗[R] Localization.Away g ≃ₐ[S] Localization.Away (1 ⊗ₜ[R] g) :=
  IsLocalization.Away.tensorProductEquivTMulRight R S g (Localization.Away g)
⊢ P ((↑↑e).comp (algebraMap S (S ⊗[R] Localization.Away g)))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks

Tactic:
eq_stalkwise,

Goal state after:
R S : CommRingCat
φ : R ⟶ S
⊢ stalkwise (fun {R S} [CommRing R] [CommRing S] x ↦ Function.Surjective ⇑x) (Spec.map φ) ↔
    (CommRingCat.Hom.hom φ).SurjectiveOnStalks
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case refine_1.convert_1
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ≤ X.basicOpen f

Tactic:
· simp only [Scheme.basicOpen_res, inf_le_right]

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ ((affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q')
      f✝ ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] f ↦ Q f ∧ Q' f) f✝

Tactic:
change _ ∧ _ ↔ _

Goal state after:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f✝ ∧
      affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q') f✝ ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] f ↦ Q f ∧ Q' f) f✝
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
⊢ QuasiSober ↥X

Tactic:
apply +allowSynthFailures
    quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.f x))

Goal state after:
case hS
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), IsOpen ↑s

case inst
X : Scheme
⊢ ∀ (s : ↑(Set.range fun x ↦ Set.range ⇑(X.affineCover.f x))), QuasiSober ↑↑s

case hS'
X : Scheme
⊢ (⋃₀ Set.range fun x ↦ Set.range ⇑(X.affineCover.f x)) = ⊤
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
x : ↥(Spec R)
⊢ _root_.IsReduced ↑(CommRingCat.of (Localization.AtPrime x.asIdeal))

Tactic:
dsimp

Goal state after:
X : Scheme
R : CommRingCat
H : _root_.IsReduced ↑R
x : ↥(Spec R)
⊢ _root_.IsReduced (Localization.AtPrime x.asIdeal)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ((I.ideal ⊓ J.ideal) U) =
    (I.ideal ⊓ J.ideal) (X.affineBasicOpen f)

Tactic:
dsimp

Goal state after:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) =
    I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f)
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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ iSup V = ⊤

Tactic:
apply f.iSup_preimage_eq_top
      apply U.ι.image_injective
      simp only [U.ι.image_iSup, U.ι.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]
      conv_rhs => rw [Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι, heq]
      ext : 1
      have (i : Us) : U ⊓ i.1 = i.1 := by simp [heq, le_sSup i.property]
      simp [this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : closure {x} ∈ irreducibleComponents ↥(Spec R)
inst✝ : IsReduced (Spec R)
⊢ x.asIdeal ∈ minimalPrimes ↑R

Tactic:
← PrimeSpectrum.vanishingIdeal_singleton,

Goal state after:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : closure {x} ∈ irreducibleComponents ↥(Spec R)
inst✝ : IsReduced (Spec R)
⊢ PrimeSpectrum.vanishingIdeal {x} ∈ minimalPrimes ↑R
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))) =
    Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ))

Tactic:
rw [← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv, RingHom.comap_ker,
    RingEquiv.toRingHom_eq_coe, Iso.commRingCatIsoToRingEquiv_toRingHom, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp]

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
φ : Γ(X, ↑U) ⟶ CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U) := CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
          (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).hom)) =
    RingHom.ker (CommRingCat.Hom.hom ((↑U).topIso.hom ≫ φ))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
by
  ext U : 2
  simp only [radical_ideal, ideal_inf, Pi.inf_apply, Ideal.radical_inf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x y : ↥X
h : x ⤳ y
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ
  have hxU : x ∈ U := h.mem_open U.2 hyU
  rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]

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

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

Tactic:
dsimp

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑I.support) = (I.ideal U).radical
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case refine_2
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ↑⟨x, ⟨f, hf⟩⟩.snd =
    (X.presheaf.stalkCongr ⋯).hom ≫
      ↑((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
            ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).snd

Tactic:
refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
      simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk,
        TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
simp [Hom.residueFieldMap]

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Y.residue (f x) ≫ CommRingCat.ofHom (ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ X.residue x
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
← Spec.map_comp_assoc

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

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this : QuasiCompact f'
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
have : IsOpenImmersion iU := MorphismProperty.of_isPullback H inferInstance

Goal state after:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝ : QuasiCompact f'
this : IsOpenImmersion iU
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine Z
h : IsPullback fst snd f g
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)

Tactic:
have : IsAffine P := .of_isPullback h

Goal state after:
X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : IsAffine X
inst✝¹ : IsAffine Y
inst✝ : IsAffine Z
h : IsPullback fst snd f g
this : IsAffine P
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)
Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType

Goal state before:
pp: case refine_1.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
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 : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))

Tactic:
dsimp

Goal state after:
case refine_1.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
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 : P.CostructuredArrow ⊤ Scheme.Spec X
f : ↥(Spec (unop (F.obj S))) → ↑(unop (F.obj S))
hqf : ∀ (q : ↥(Spec (unop (F.obj S)))), q ∈ PrimeSpectrum.basicOpen (f q)
hf : ∀ (q : ↥(Spec (unop (F.obj S)))), Q' Γ(Spec (unop (F.obj S)), PrimeSpectrum.basicOpen (f q))
⊢ ∀ (i : ↥(Spec (unop (F.obj S)))), Q'.isoClosure (CommRingCat.of (Localization.Away (f i)))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

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

Tactic:
dsimp

Goal state after:
X✝ : Scheme
X Y : (MorphismProperty.Over @IsClosedImmersion ⊤ X✝)ᵒᵖ
f : X ⟶ Y
⊢ inv (Scheme.Hom.toImage (unop Y).hom) ≫ (MorphismProperty.Comma.Hom.hom f.unop).left =
    Scheme.IdealSheafData.inclusion ⋯ ≫ inv (Scheme.Hom.toImage (unop X).hom)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inr.mpr.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

Tactic:
obtain (hi | hi) := lt_or_gt_of_ne hi

Goal state after:
case inr.mpr.inr.inl
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : i < ((LinearMap.mul R A) f).charpoly.natDegree
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i

case inr.mpr.inr.inr
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
h✝ : Nontrivial R
this : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A
H : ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I
i : ℕ
hi✝ : i ≠ ((LinearMap.mul R A) f).charpoly.natDegree
hi : ((LinearMap.mul R A) f).charpoly.natDegree < i
⊢ (Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f))).coeff i =
    (X ^ ((LinearMap.mul R A) f).charpoly.natDegree).coeff i