mathlib-initiative/mathlib-tactics huggingface dataset:
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
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P.IsStableUnderBaseChange

Tactic:
by
  apply HasAffineProperty.isStableUnderBaseChange
  let := HasAffineProperty.isLocal_affineProperty P
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  intro X Y S _ _ f g H
  rw [← HasAffineProperty.iff_of_isAffine (P := P)] at H ⊢
  wlog hX : IsAffine Y generalizing Y
  · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
      (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
    intro i
    simp only [Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_π_app,
      Category.comp_id]
    apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance
  rw [iff_of_isAffine (P := P)] at H ⊢
  exact hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H

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

Goal state before:
pp: case map_units
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (y : ↥(Submonoid.powers f)), IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑y)

pp: case surj
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

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

Tactic:
· rintro ⟨_, n, rfl⟩
    simp only [map_pow, RingHom.algebraMap_toAlgebra]
    exact IsUnit.pow _ (RingedSpace.isUnit_res_basicOpen _ f)

Goal state after:
case surj
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ {x y : ↑Γ(X, U)},
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) = J.ideal (U i)
⊢ ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)

Tactic:
by aesop

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

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) = J.ideal (U i)
⊢ ∀ (i : ι), J.ideal (U i) ≤ I.ideal (U i)

Tactic:
by aesop

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

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

Tactic:
exact V.2.isLocalization_of_eq_basicOpen _ _ rfl

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f

Tactic:
let f' : Γ(X, V) ⧸ I.ideal V := Ideal.Quotient.mk _ f

Goal state after:
X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
this : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯).toAlgebra
f' : ↑Γ(X, ↑V) ⧸ I.ideal V := (Ideal.Quotient.mk (I.ideal V)) f
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ residueFieldCongr e ≪≫ residueFieldCongr e' = residueFieldCongr ⋯

Tactic:
subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ (residueFieldCongr e).hom ≫ (residueFieldCongr e').hom = (residueFieldCongr ⋯).hom

Tactic:
subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ tensorCongr e ≪≫ tensorCongr e' = tensorCongr ⋯

Tactic:
subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ (tensorCongr e).hom ≫ (tensorCongr e').hom = (tensorCongr ⋯).hom

Tactic:
subst e e'
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom ≫ T.SpecTensorTo ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g

Tactic:
tensorCongr_SpecTensorTo_assoc

Goal state after:
case h₀
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ (ofPoint (T.SpecTensorTo p)).SpecTensorTo ≫ pullback.fst f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.fst f g
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom ≫ T.SpecTensorTo ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g

Tactic:
tensorCongr_SpecTensorTo_assoc

Goal state after:
case h₁
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ (ofPoint (T.SpecTensorTo p)).SpecTensorTo ≫ pullback.snd f g =
    (Spec T.tensor).fromSpecResidueField p ≫ T.SpecTensorTo ≫ pullback.snd f g
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case to_basicOpen
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H this : IsAffine X
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)

Tactic:
Scheme.preimage_basicOpen

Goal state after:
case to_basicOpen
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
r : ↑Γ(Y, ⊤)
H this : IsAffine X
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) r))
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : 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
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))

Tactic:
Scheme.preimage_basicOpen

Goal state after:
case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : 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
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
hf :
  ∀ (r : ↥s),
    IsAffine ↑(X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) ↑r)) ∧
      Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Epi (pullbackComparison forgetToTop f g)

Tactic:
by
  refine (CategoryTheory.forget TopCat).epi_of_epi_map ?_
  rw [← CategoryTheory.epi_comp_iff_of_isIso _
    (pullbackComparison (CategoryTheory.forget TopCat) (forgetToTop.map f) (forgetToTop.map g)),
    ← _root_.CategoryTheory.Limits.pullbackComparison_comp, epi_iff_surjective]
  apply Scheme.pullbackComparison_forget_surjective _ _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
hf : f.EssFiniteType
⊢ ((IsLocalRing.residue S).comp f).EssFiniteType

Tactic:
exact .comp hf (FiniteType.of_surjective _ <| IsLocalRing.residue_surjective).essFiniteType

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
f : R →+* S
inst✝² : IsLocalRing R
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
hf : f.EssFiniteType
⊢ (IsLocalRing.ResidueField.map f).EssFiniteType

Tactic:
refine .of_comp (IsLocalRing.residue R) ?_
  rw [IsLocalRing.ResidueField.map_comp_residue]
  exact .comp hf (FiniteType.of_surjective _ <| IsLocalRing.residue_surjective).essFiniteType

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion ((I.glueDataObjIso U).hom ≫ I.gluedTo ∣_ ↑U)

Tactic:
glueDataObjIso_hom_restrict

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsPreimmersion (I.glueDataObjι U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
⊢ app (toImage f) (imageι f ⁻¹ᵁ ↑U) =
    ((ker f).subschemeObjIso U).hom ≫
      CommRingCat.ofHom (Ideal.Quotient.lift ((ker f).ideal U) (CommRingCat.Hom.hom (app f ↑U)) ⋯)

Tactic:
have := ConcreteCategory.epi_of_surjective _ (f.ker.subschemeι_app_surjective U)
  rw [← cancel_epi (f.ker.subschemeι.app U), ← Scheme.Hom.comp_app,
    Scheme.Hom.congr_app f.toImage_imageι, f.ker.subschemeι_app,
    ← IsIso.eq_comp_inv, ← Functor.map_inv]
  simp only [Hom.comp_base, Opens.map_comp_obj, Category.assoc,
    Iso.inv_hom_id_assoc, eqToHom_op, inv_eqToHom]
  rw [← reassoc_of% CommRingCat.ofHom_comp, Ideal.Quotient.lift_comp_mk, CommRingCat.ofHom_hom,
    eqToHom_refl, CategoryTheory.Functor.map_id]
  exact (Category.comp_id _).symm

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

Goal state before:
pp: case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)) →
    ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ IsAffine X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯

Tactic:
introv H h₁ h₂

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ IsAffine (pullback f₁ f₂)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)

Tactic:
have : IsPreimmersion (f.liftCoborder ≫ f.coborderRange.ι) := by
    simp only [Scheme.Hom.liftCoborder_ι]; infer_instance

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
⊢ IsClosedImmersion (Scheme.Hom.liftCoborder f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : X ⟶ Y
hi : MorphismProperty.isomorphisms Scheme i
f : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)

Tactic:
change IsIso i at hi

Goal state after:
case inst.refine_1
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : X ⟶ Y
f : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
hi : MorphismProperty.isomorphisms Scheme i
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)

Tactic:
change IsIso i at hi

Goal state after:
case inst.refine_2
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
i : Y ⟶ Z
f : X ⟶ Y
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) f
hi : IsIso i
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)) (f ≫ i)
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S✝
inst✝⁴ : Algebra R S✝
ι : Type u_3
inst✝³ : Finite ι
S : ι → Type u_4
inst✝² : (i : ι) → CommRing (S i)
inst✝¹ : (i : ι) → Algebra R (S i)
inst✝ : ∀ (i : ι), FinitePresentation R (S i)
⊢ FinitePresentation R ((a : ι) → S a)

Tactic:
let (i : ι) : Algebra (Π a, S a) (S i) := (Pi.evalAlgHom R S i).toAlgebra
  have (i : ι) : IsLocalization.Away (Pi.single i 1 : ∀ a, S a) (S i) := by
    refine IsLocalization.away_of_isIdempotentElem ?_ (RingHom.ker_evalRingHom _ _)
      ((Pi.evalRingHom S i).surjective)
    simp [IsIdempotentElem, ← Pi.single_mul_left]
  exact Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway
    _ (Ideal.span_single_eq_top S) (fun i ↦ S i)

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
f✝ : R✝ →+* S✝
hf : f✝.FinitePresentation
s✝ : Set (PrimeSpectrum S✝)
hs✝ : IsConstructible s✝
R : Type u_1
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
T : Type u_2
inst✝ : CommRing T
f : R →+* S
g : S →+* T
H₁ : ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
H₂ : ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)
s : Set (PrimeSpectrum T)
hs : IsConstructible s
⊢ IsConstructible (comap (g.comp f) '' s)

Tactic:
simp only [comap_comp, Set.image_comp]

Goal state after:
case refine_2
R✝ : Type u_1
S✝ : Type u_2
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S✝
f✝ : R✝ →+* S✝
hf : f✝.FinitePresentation
s✝ : Set (PrimeSpectrum S✝)
hs✝ : IsConstructible s✝
R : Type u_1
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
T : Type u_2
inst✝ : CommRing T
f : R →+* S
g : S →+* T
H₁ : ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
H₂ : ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)
s : Set (PrimeSpectrum T)
hs : IsConstructible s
⊢ IsConstructible (comap f '' comap g '' s)
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: 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
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

Tactic:
cases subsingleton_or_nontrivial R
  · have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial
    simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0]
  have : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A := by
    rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
  rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective]
  simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply,
    Algebra.coe_lmul_eq_mul, Algebra.TensorProduct.comm_tmul]
  rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)),
    LinearMap.isNilpotent_iff_charpoly, ← Algebra.baseChange_lmul, LinearMap.charpoly_baseChange,
    this]
  simp_rw [← ((LinearMap.mul R A) f).charpoly_natDegree]
  constructor
  · intro e i hi
    replace e := congr(($e).coeff i)
    simpa only [Algebra.coe_lmul_eq_mul, coeff_map, coeff_X_pow, hi.ne, ↓reduceIte,
      ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using e
  · intro H
    ext i
    obtain (hi | hi) := eq_or_ne i ((LinearMap.mul R A) f).charpoly.natDegree
    · simp only [Algebra.coe_lmul_eq_mul, hi, coeff_map, coeff_X_pow, ↓reduceIte]
      rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
    obtain (hi | hi) := lt_or_gt_of_ne hi
    · simpa [hi.ne, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using H i hi
    · simp [hi.ne', coeff_eq_zero_of_natDegree_lt hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ comap ((evalRingHom 0).comp C) x = x

Tactic:
(show (evalRingHom 0).comp C = .id R by ext; simp),

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ comap (RingHom.id R) x = x
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Finite R (R[X] ⧸ Ideal.span {g})

Tactic:
exact .of_basis (AdjoinRoot.powerBasis' hg).basis

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

Goal state before:
pp: case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})

Tactic:
exact .of_basis (AdjoinRoot.powerBasis' hg).basis

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
𝒰 : X.OpenCover := X.openCoverOfIsOpenCover (fun x ↦ { carrier := {x}, is_open' := ⋯ }) ⋯
⊢ IsLocallyArtinian X

Tactic:
have inst (i : _) : DiscreteTopology (𝒰.X i) := (𝒰.f i).isOpenEmbedding.discreteTopology

Goal state after:
case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
𝒰 : X.OpenCover := X.openCoverOfIsOpenCover (fun x ↦ { carrier := {x}, is_open' := ⋯ }) ⋯
inst : ∀ (i : 𝒰.I₀), DiscreteTopology ↥(𝒰.X i)
⊢ IsLocallyArtinian X
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Set.range ⇑(asFiberHom f x) = {asFiber f x}

Tactic:
by aesop

Goal state after:
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
Z : ↑(irreducibleComponents ↥Y)
⊢ closure {⋯.genericPoint} ∈ irreducibleComponents ↥Y

Tactic:
Z.property.1.closure_genericPoint (isClosed_of_mem_irreducibleComponents _ Z.property)

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
Z : ↑(irreducibleComponents ↥Y)
⊢ ↑Z ∈ irreducibleComponents ↥Y
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyOpen

Tactic:
by
  rw [eq]
  infer_instance

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

Goal state before:
pp: Z S : Scheme
⊢ @IsIntegralHom ≤ topologically @IsClosedMap

Tactic:
intro X Y f

Goal state after:
Z S X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩
  clear * -
  wlog hY : ∃ R, Y = Spec R
  · rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover]
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂
    exact fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩
  obtain ⟨R, rfl⟩ := hY
  wlog hX : ∃ S, X = Spec S
  · have inst : IsAffine X := isAffine_of_isAffineHom f
    rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]
    exact this _ inferInstance inferInstance ⟨_, rfl⟩
  obtain ⟨S, rfl⟩ := hX
  obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩
  rw [SpecMap_iff]
  apply PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom
  algebraize [φ.1, Polynomial.mapRingHom φ.1]
  exact H₁.universally_isClosedMap (Spec.map (CommRingCat.ofHom Polynomial.C))
    (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
    (isPullback_SpecMap_of_isPushout _ _ _ _
    (CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))

Tactic:
rw [← toSpecΓ_naturality]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
⊢ IsImmersion (f ≫ Y.toSpecΓ)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
⊢ X.IsQuasiAffine

Tactic:
have := QuasiCompact.compactSpace_of_compactSpace f
  refine .of_forall_exists_mem_basicOpen _ fun x ↦ ?_
  obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ := (IsQuasiAffine.isBasis_basicOpen
    Y).exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
  refine ⟨f.appTop r, ?_⟩
  rw [← preimage_basicOpen_top]
  exact ⟨hr.preimage _, hxr⟩

Goal state after: