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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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) ⋯) ↔
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
constructor

Goal state after:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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) ⋯) →
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

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) ⋯
Module: Mathlib.RingTheory.Finiteness.FiniteTypeLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := algebraMap R S
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ FiniteType R S

Tactic:
constructor

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set R
hs✝ : Ideal.span s✝ = ⊤
s : Finset R
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FiniteType (Localization.Away ↑i) (Localization.Away ↑i ⊗[R] S)
f : R →+* S := ⋯
this : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ ⊤.FG
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this✝ : IsAffine ↑U
this : IsAffine ↑V
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (X.homOfLE ⋯)

Tactic:
ext

Goal state after:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁] [IsOpenImmersion f₂],
    IsAffine (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this✝ : IsAffine ↑U
this : IsAffine ↑V
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
x✝ : ↥↑V
⊢ x✝ ∈ ↑(V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι) ↔ x✝ ∈ ↑(Scheme.Hom.opensRange (X.homOfLE ⋯))
Module: Mathlib.RingTheory.RingHom.Finite

Goal state before:
pp: R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (Localization.awayMap f ↑r).Finite
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r ↦ (Localization.awayMap f ↑r).toAlgebra
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ f.Finite

Tactic:
constructor

Goal state after:
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : ↥s), (Localization.awayMap f ↑r).Finite
this✝² : Algebra R S := ⋯
this✝¹ : (r : ↥s) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := ⋯
this✝ : ∀ (r : ↥s), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : ↥s), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ ⊤.FG
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: case e'_5
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FiniteType R (Localization.Away ↑r)
algInst✝ : Algebra R S := ⋯
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
⊢ OreLocalization.instAlgebra = ((algebraMap S (Localization.Away ↑⟨r, hr⟩)).comp f).toAlgebra

Tactic:
ext

Goal state after:
case e'_5
R S : Type u_5
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FiniteType R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
r✝ : R
x✝ : OreLocalization (Submonoid.powers r) S
⊢ (have I := OreLocalization.instAlgebra;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
x : ↥X
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
exact Function.Surjective.of_comp h

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

Goal state before:
pp: X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J ≤ I.map f ↔ J.comap f ≤ I

Tactic:
constructor

Goal state after:
case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J ≤ I.map f → J.comap f ≤ I

case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
⊢ J.comap f ≤ I → J ≤ I.map f
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g
⊢ lift f g H ≫ f = g

Tactic:
by
  nth_rw 2 [← f.toImage_imageι]
  simp [lift, -Scheme.Hom.toImage_imageι, g.toImage_imageι]

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

Goal state before:
pp: ⊢ @IsSeparated = MorphismProperty.diagonal @IsClosedImmersion

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsSeparated x✝ ↔ MorphismProperty.diagonal (@IsClosedImmersion) x✝
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
⊢ IsSeparated (Spec.map f)

Tactic:
constructor

Goal state after:
W X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
R S : CommRingCat
f : R ⟶ S
⊢ autoParam (IsClosedImmersion (pullback.diagonal (Spec.map f))) isClosedImmersion_diagonal._autoParam
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range (⇑(Scheme.Hom.coborderRange f).ι ∘ ⇑(Scheme.Hom.liftCoborder f)) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f

Tactic:
← TopCat.coe_comp,

Goal state after:
case e'_3
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
this✝ : IsPreimmersion (Scheme.Hom.liftCoborder f ≫ (Scheme.Hom.coborderRange f).ι)
this : IsPreimmersion (Scheme.Hom.liftCoborder f)
⊢ Set.range ⇑(ConcreteCategory.hom ((Scheme.Hom.liftCoborder f).base ≫ (Scheme.Hom.coborderRange f).ι.base)) =
    ⇑(Scheme.Hom.coborderRange f).ι '' Subtype.val ⁻¹' Set.range ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: ⊢ @IsImmersion = @IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f ↦ IsLocallyClosed (Set.range f)

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsImmersion x✝ ↔ (@IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f ↦ IsLocallyClosed (Set.range f)) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ IsImmersion g'

Tactic:
← Limits.pullback.lift_fst (f := f) (g := g.coborderRange.ι) g' (f' ≫ g.liftCoborder)
      (by simpa using H.w.symm)

Goal state after:
X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Y' S : Scheme
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
H : IsPullback f' g' g f
hg : IsImmersion g
Z : Scheme := pullback f (Scheme.Hom.coborderRange g).ι
e : Y' ⟶ Z := pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯
this : IsClosedImmersion e
⊢ IsImmersion (pullback.lift g' (f' ≫ Scheme.Hom.liftCoborder g) ⋯ ≫ pullback.fst f (Scheme.Hom.coborderRange g).ι)
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: case e'_5
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FinitePresentation R (Localization.Away ↑r)
algInst✝ : Algebra R S := ⋯
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
⊢ OreLocalization.instAlgebra = ((algebraMap S (Localization.Away ↑⟨r, hr⟩)).comp f).toAlgebra

Tactic:
ext

Goal state after:
case e'_5
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), Algebra.FinitePresentation R (Localization.Away ↑r)
algInst✝ : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4✝ : OreLocalization.instSemiring = CommRing.toCommSemiring.toSemiring
r✝ : R
x✝ : OreLocalization (Submonoid.powers r) S
⊢ (have I := OreLocalization.instAlgebra;
    r✝ • x✝) =
    r✝ • x✝
Module: Mathlib.RingTheory.RingHom.FinitePresentation

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), ((algebraMap S (Localization.Away ↑r)).comp f).FinitePresentation
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FinitePresentation

Tactic:
replace H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FinitePresentation] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
algInst✝ : Algebra R S := f.toAlgebra
H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away r)
⊢ f.FinitePresentation
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : S →+* T
g : R →+* S
s : ConstructibleSetData R
⊢ map (f.comp g) s = map f (map g s)

Tactic:
simp [map, image_image, Function.comp_def, BasicConstructibleSetData.map_comp']

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

Goal state before:
pp: case sdiff.e'_3
R : Type u_1
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite ↑s
⊢ (Set.range fun i ↦ ↑((Finite.equivFin ↑s).symm i)) = s

Tactic:
ext

Goal state after:
case sdiff.e'_3
R : Type u_1
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
i : R
s : Set R
hs : s.Finite
this : Finite ↑s
x✝ : R
⊢ (x✝ ∈ Set.range fun i ↦ ↑((Finite.equivFin ↑s).symm i)) ↔ x✝ ∈ s
Module: Mathlib.LinearAlgebra.Charpoly.BaseChange

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

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module.Free R M
inst✝² : Module.Finite R M
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : M ≃ₗ[R] M
⊢ ↑(LinearEquiv.det (baseChange R A M M f)) = ↑((Units.map ↑(algebraMap R A)) (LinearEquiv.det f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
⊢ IsSeparated f

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
⊢ autoParam (IsClosedImmersion (pullback.diagonal f)) IsSeparated.isClosedImmersion_diagonal._autoParam
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsClosedImmersion f ↔ ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

Tactic:
constructor

Goal state after:
case mp
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ IsClosedImmersion f → ∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))

case mpr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
⊢ (∃ I e, f = e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) → IsClosedImmersion f
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ AffineTargetMorphismProperty.of (@IsClosedImmersion) x✝¹ →
    IsAffine x✝³ ∧ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop x✝¹))

Tactic:
by apply isAffine_surjective_of_isAffine

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
⊢ IsConstructible (comap Polynomial.C '' S.toSet)

Tactic:
hT

Goal state after:
R : Type u_1
inst✝ : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
⊢ IsConstructible T.toSet
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case 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
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree ↔
    ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

Tactic:
constructor

Goal state after:
case inr.mp
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
⊢ Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree →
    ∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I

case inr.mpr
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
⊢ (∀ i < ((LinearMap.mul R A) f).charpoly.natDegree, ((LinearMap.mul R A) f).charpoly.coeff i ∈ I) →
    Polynomial.map (algebraMap R I.ResidueField) (LinearMap.charpoly ((Algebra.lmul R A) f)) =
      X ^ ((LinearMap.mul R A) f).charpoly.natDegree
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
⊢ ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))

Tactic:
ext

Goal state after:
case ha
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
x✝ : ↥B'
⊢ ((AlgHom.restrictScalars K (ψ.comp Algebra.TensorProduct.includeLeft)).comp Algebra.TensorProduct.includeRight) x✝ =
    ((AlgHom.restrictScalars K
            (((↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
                  ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
                    ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
                      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
                        ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))).comp
              Algebra.TensorProduct.includeLeft)).comp
        Algebra.TensorProduct.includeRight)
      x✝
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
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) ↔
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
constructor

Goal state after:
case mp
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) →
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)

case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f) →
    x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})

Tactic:
refine ⟨comap (algebraMap A _) ⟨q, hq⟩, ⟨by simpa [Set.subset_def], by simpa⟩, ?_⟩

Goal state after:
case mpr
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap R A)
      (comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq }) =
    x
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
constructor

Goal state after:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsLocallyNoetherian X → ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ (∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)) → IsLocallyNoetherian X
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ IsNilpotent (e ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f)) ↔
    map (algebraMap R x.asIdeal.ResidueField) f = 0

Tactic:
isNilpotent_iff_eq_zero

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ e ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) = 0 ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

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

Tactic:
ext

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ IsNilpotent
      (e
        ((Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f))) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
isNilpotent_iff_eq_zero

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ e
        ((Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField)
          ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f)) =
      0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsNoetherianRing ↑R
⊢ NoetherianSpace ↥(Spec R)

Tactic:
convert! PrimeSpectrum.instNoetherianSpace (R := R)

Goal state after: