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

Goal state before:
pp: X : Scheme
x : ↥X
s : ↥(Spec (X.residueField x))
⊢ (X.fromSpecResidueField x) s = x

Tactic:
simp [fromSpecResidueField]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ Spec.map (residueFieldIso R x).inv ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField)) =
    (Spec R).fromSpecResidueField x

Tactic:
simp only [Scheme.fromSpecResidueField, Spec.fromSpecStalk_eq, ← Spec.map_comp]

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv) =
    Spec.map (((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case a.inr.refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ x ∈ (𝒰.X i).zeroLocus ↑((ker (Cover.pullbackHom 𝒰 f i)).ideal ⟨⊤, ⋯⟩)

Tactic:
rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
        · exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
        · exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2
        · exact (IsPullback.of_hasPullback _ _).flip

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(I.glueData.ι U) = Set.range ⇑(I.gluedTo ⁻¹ᵁ ↑U).ι

Tactic:
simp only [Scheme.Opens.range_ι, TopologicalSpace.Opens.map_coe, range_glueData_ι]

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 : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]

Goal state after:
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)
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]

Goal state after:
case refine_1
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
h : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: R S : Type u_5
x✝¹ : CommRing R
x✝ : CommRing S
e : R ≃+* S
algInst✝ : Algebra R S := e.toRingHom.toAlgebra
⊢ e.toRingHom.FiniteType

Tactic:
apply Algebra.FiniteType.equiv (inferInstanceAs <| Algebra.FiniteType R R) <|
    .ofRingEquiv (congrFun rfl)

Goal state after:
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

Tactic:
simp [← Spec.map_comp_assoc, F]

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

Goal state before:
pp: W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ autoParam (IsClosedImmersion (pullback.diagonal (Spec.map f))) isClosedImmersion_diagonal._autoParam

Tactic:
change IsClosedImmersion
    (Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))))

Goal state after:
W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsClosedImmersion (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

Goal state before:
pp: R : Type u_3
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ LinearMap.det (baseChange A f) = (algebraMap R A) (LinearMap.det f)

Tactic:
nontriviality A
  have := (algebraMap R A).domain_nontrivial
  rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]
  simp

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

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.toImage f))) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.ker f).subschemeι)))

Tactic:
Scheme.Hom.appTop,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.toImage f) ⊤)) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.ker f).subschemeι)))
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.toImage f) ⊤)) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop (Scheme.Hom.ker f).subschemeι)))

Tactic:
Scheme.Hom.appTop,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ Function.Surjective
    (⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.toImage f) ⊤)) ∘
      ⇑(CommRingCat.Hom.hom (Scheme.Hom.app (Scheme.Hom.ker f).subschemeι ⊤)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: case e'_2
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f

Tactic:
Scheme.isSeparated_iff,

Goal state after:
case e'_2
W X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsSeparated (terminal.from X) ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
⊢ geometrically P f ↔
    ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))

Tactic:
refine ⟨fun hf K _ _ ↦ pullback_of_geometrically hf _ _, fun H ↦ ?_⟩

Goal state after:
X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))
⊢ geometrically P 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 := ⋯
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := ⋯
Z : Scheme := ⋯
g : Z ⟶ Y := ⋯
this✝ : Finite ↥Z
this : QuasiCompact g
H✝ : IsSchemeTheoreticallyDominant g
H :
  IsPullback
    (Cofan.IsColimit.desc (coproductIsCoproduct fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)) fun x ↦
      pullback.fst f (Y.fromSpecStalk ⋯.genericPoint))
    (Cofan.IsColimit.desc (coproductIsCoproduct fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)) fun x ↦
      pullback.snd f (Y.fromSpecStalk ⋯.genericPoint) ≫
        (Cofan.mk (∐ fun Z ↦ Spec (pt Z)) (Sigma.ι fun Z ↦ Spec (pt Z))).inj x)
    f g
⊢ ∀ (i : (sigmaOpenCover fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)).I₀),
    IsReduced ((sigmaOpenCover fun i ↦ pullback f (Y.fromSpecStalk ⋯.genericPoint)).X i)

Tactic:
exact fun i ↦ GeometricallyReduced.geometrically_isReduced _ _ _ (.of_hasPullback _ _)

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

Goal state before:
pp: case a
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally

Tactic:
exact universally_mono fun X Y f ⟨h₁, h₂⟩ ↦ (isClosedMap_iff_specializingMap _).mpr h₁

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
this :
  ∀ (r : ↑Γ(Y, ⊤)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
      (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) ↑r))

Tactic:
rw [← Scheme.preimage_basicOpen_top]; exact r.2.preimage f

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ ((𝔸(n; S).toSpecΓ ≫
          Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)))) ≫
        homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
          (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X)) ≫
      𝔸(n; S) ↘ S =
    𝟙 𝔸(n; S) ≫ 𝔸(n; S) ↘ S

Tactic:
simp only [Category.assoc, homOfVector_over, Category.id_comp]

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))) ≫
        Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv =
    𝔸(n; S) ↘ S
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map
          (CommRingCat.ofHom ((eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)).comp C)) ≫
        S.isoSpec.inv =
    𝔸(n; S) ↘ S

Tactic:
eval₂Hom_comp_C,

Goal state after:
case h₁
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ 𝔸(n; S).toSpecΓ ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S)))) ≫ S.isoSpec.inv =
    𝔸(n; S) ↘ S
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.app
            (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
            ⊤)).comp
      ((eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S)).comp C) =
    CommRingCat.Hom.hom (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv)

Tactic:
eval₂Hom_comp_C,

Goal state after:
case hC
n : Type u
S : Scheme
inst✝ : IsAffine S
⊢ (CommRingCat.Hom.hom
          (Scheme.Hom.app
            (homOfVector (Spec.map (CommRingCat.ofHom C) ≫ S.isoSpec.inv)
              (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv) ∘ X))
            ⊤)).comp
      (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) =
    CommRingCat.Hom.hom (CommRingCat.ofHom C ≫ (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).inv)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
R : CommRingCat
⊢ (SpecIso n R).inv ≫ 𝔸(n; Spec R) ↘ Spec R = Spec.map (CommRingCat.ofHom C)

Tactic:
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, Scheme.Spec_map,
    Quiver.Hom.unop_op, Category.assoc, isoOfIsAffine_inv_over, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]

Goal state after:
n : Type u
R : CommRingCat
⊢ Spec.map
      ((Scheme.ΓSpecIso R).inv ≫
        CommRingCat.ofHom C ≫ (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) =
    Spec.map (CommRingCat.ofHom C)
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ ↑p (IsLocalRing.closedPoint K) ∈ closedPoints ↥X

Tactic:
have := isClosedImmersion_of_comp_eq_id _ _ p.2
    have := p.1.isClosedEmbedding.isClosed_range
    rwa [Set.range_eq_singleton] at this
    exact fun x ↦ congr(p.1 $(Subsingleton.elim _ _))

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Tactic:
rw [H _ ht, IsLocalization.mk'_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: R : CommRingCat
inst✝ : IsDomain ↑R
⊢ genericPoint ↥(Spec R) = ⊥

Tactic:
by
  apply (genericPoint_spec (Spec R)).eq
  rw [isGenericPoint_def]
  rw [← PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.vanishingIdeal_singleton]
  rw [← PrimeSpectrum.zeroLocus_singleton_zero]
  rfl

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

Goal state before:
pp: case e'_2.e'_4
R₀ : Type u_1
inst✝² : CommRing R₀
n : ℕ
R : Type u_6
inst✝¹ : CommRing R
inst✝ : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] R ⧸ Ideal.span {c} := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective : Surjective ⇑q₂
e₁ : InductionObj (Localization.Away c) n :=
  { val := Polynomial.C (IsLocalization.Away.invSelf c) • ⇑(mapRingHom ↑q₁) ∘ e.val }
e₂ : InductionObj (R ⧸ Ideal.span {c}) n := { val := ⇑(mapRingHom ↑q₂) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (R ⧸ Ideal.span {c}) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (R ⧸ Ideal.span {c})
hT₁ : comap Polynomial.C '' (zeroLocus (Set.range e₁.val) \ zeroLocus {(mapRingHom ↑q₁) f}) = T₁.toSet
hT₁deg : ∀ x ∈ T₁, x.n ≤ e₁.degBound
hT₂ : comap Polynomial.C '' (zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}) = T₂.toSet
hT₂deg : ∀ x ∈ T₂, x.n ≤ e₂.degBound
x✝ : Invertible (q₁ c) := { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  coeffSubmodule R₀ e₁ ^ e₁.powBound =
    ⅟(q₁ c ^ e₁.powBound) • Submodule.map q₁.toLinearMap (span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → Fin x.n → R
hg₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), g₁ x i ∈ ↑(span R₀ ({c} ∪ ⋃ i, coeff(e.val i)) ^ e₁.powBound)
hq₁g₁ : ∀ x ∈ T₁, ∀ (i : Fin x.n), q₁.toLinearMap (g₁ x i) = q₁ c ^ e₁.powBound * x.g i
n₁ : Localization.Away c → ℕ
f₁ : Localization.Away c → R
hf₁ : ∀ (x : Localization.Away c), x * q₁ c ^ n₁ x = q₁ (f₁ x)
g₂ : (x : BasicConstructibleSetData (R ⧸ Ideal.span {c})) → Fin x.n → R
hg₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), g₂ x i ∈ ↑(coeffSubmodule R₀ e ^ e₂.powBound)
hq₂g₂ : ∀ x ∈ T₂, ∀ (i : Fin x.n), q₂.toLinearMap (g₂ x i) = x.g i
f₂ : R ⧸ Ideal.span {c} → R
hf₂ : ∀ (x : R ⧸ Ideal.span {c}), q₂ (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) := Finset.image (fun x ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun x ↦ { f := f₂ x.f, n := x.n + 1, g := Fin.cons c (g₂ x) }) T₂
⊢ comap (mapRingHom q₂.toRingHom) ⁻¹' (zeroLocus (Set.range e.val) \ zeroLocus {f}) =
    zeroLocus (Set.range e₂.val) \ zeroLocus {(mapRingHom ↑q₂) f}

Tactic:
rw [Set.preimage_sdiff, preimage_comap_zeroLocus, preimage_comap_zeroLocus,
          Set.image_singleton, Set.range_comp, AlgHom.toRingHom_eq_coe]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
this : f.restrict W hW hWl = g.restrict W hW hWr
⊢ (g.restrict W hW hWr).fromFunctionField = g.fromFunctionField

Tactic:
g.fromFunctionField_restrict

Goal state after:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝ : IrreducibleSpace ↥X
f✝ : X ⤏ Y
f g : X.PartialMap Y
W : X.Opens
hW : Dense ↑W
hWl : W ≤ f.domain
hWr : W ≤ g.domain
e : (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
this : f.restrict W hW hWl = g.restrict W hW hWr
⊢ g.fromFunctionField = g.fromFunctionField
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
x✝ : I
⊢ (vanishingIdeal { carrier := Z x✝, isClosed' := ⋯ }).subschemeMap (vanishingIdeal { carrier := Z x✝, isClosed' := ⋯ })
      (D.map (𝟙 x✝)) ⋯ =
    𝟙 (vanishingIdeal { carrier := Z x✝, isClosed' := ⋯ }).subscheme

Tactic:
by simp [← cancel_mono (subschemeι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofilteredOrEmpty I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
X✝ Y✝ Z✝ : I
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ (vanishingIdeal { carrier := Z X✝, isClosed' := ⋯ }).subschemeMap (vanishingIdeal { carrier := Z Z✝, isClosed' := ⋯ })
      (D.map (x✝¹ ≫ x✝)) ⋯ =
    (vanishingIdeal { carrier := Z X✝, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y✝, isClosed' := ⋯ }) (D.map x✝¹) ⋯ ≫
      (vanishingIdeal { carrier := Z Y✝, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Z✝, isClosed' := ⋯ }) (D.map x✝) ⋯

Tactic:
by simp [← cancel_mono (subschemeι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case e'_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ x ∈ ↑((opensDiagram D i U).map f ⁻¹ᵁ V) ↔
    x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V)

Tactic:
change _ ∈ V ↔ _

Goal state after:
case e'_2
I : Type u
inst✝¹ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f✝ : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
j k : Over i
f : j ⟶ k
V : ((opensDiagram D i U).obj k).Opens
hV : IsAffineOpen V
e_1✝ : (opensDiagram D i U).obj j = ↑(D.map j.hom ⁻¹ᵁ U)
x : ↥((opensDiagram D i U).obj j)
⊢ ((opensDiagram D i U).map f) x ∈ V ↔
    x ∈ ↑((D.map j.hom ⁻¹ᵁ U).ι ⁻¹ᵁ D.map (Over.Hom.left f) ⁻¹ᵁ (D.map k.hom ⁻¹ᵁ U).ι ''ᵁ V)