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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ LocallyOfFiniteType f

Tactic:
]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ LocallyOfFiniteType f
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)
hψeq :
  ψ =
    (↑(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))))
⊢ Injective
    ⇑((↑(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:
]

Goal state after:
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)
hψeq :
  ψ =
    (↑(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))))
⊢ Injective
    ⇑((↑(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)))))
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
]

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f
⊢ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

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

Tactic:
]

Goal state after:
R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
⊢ s ⊆ ↑q.asIdeal
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)
hψeq :
  ψ =
    (↑(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))))
hψ : Injective ⇑ψ
⊢ IsNilpotent
      ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField))
        ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f)) ↔
    IsNilpotent (ψ ((algebraMap (A ⊗[K] ↥B') (A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)) f))

Tactic:
]

Goal state after:
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)
hψeq :
  ψ =
    (↑(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))))
hψ : Injective ⇑ψ
⊢ IsNilpotent
      ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField))
        ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f)) ↔
    IsNilpotent (ψ ((algebraMap (A ⊗[K] ↥B') (A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)) f))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: 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
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal (Algebra.ofId R A) ⋯) ⋯
this : f ∈ q.asIdeal
⊢ False

Tactic:
]

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
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
hs : Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
F : (A ⧸ Ideal.span s) ⊗[R] (Ideal.comap (algebraMap R A) q.asIdeal).ResidueField →ₐ[A] q.asIdeal.ResidueField :=
  Algebra.TensorProduct.lift (Ideal.Quotient.liftₐ (Ideal.span s) (Algebra.ofId A q.asIdeal.ResidueField) hs)
    (Ideal.ResidueField.mapₐ (Ideal.comap (algebraMap R A) q.asIdeal) q.asIdeal (Algebra.ofId R A) ⋯) ⋯
this : f ∈ q.asIdeal
⊢ False
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
H :
  ¬∀ ⦃I : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)⦄,
      I ∈ {J | J.IsPrime} → (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∈ I
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})

Tactic:
]

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
H :
  ¬∀ ⦃I : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)⦄,
      I ∈ {J | J.IsPrime} → (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f ∈ I
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f})
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    (Subtype.val ∘ ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i)))) ∘ ⇑(Cover.pullbackHom Y.affineCover f i) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s

Tactic:
]

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    (Subtype.val ∘ ⇑(homeoOfIso (isoOpensRange (Y.affineCover.f i)))) ∘ ⇑(Cover.pullbackHom Y.affineCover f i) ''
      ⇑((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i) ⁻¹' s
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := ⋯
suitableN : R → Set ℕ := ⋯
minN : R → ℕ := ⋯
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := ⋯
⊢ ∀ (m : ℕ), N ≤ m → I N = I m

Tactic:
have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
⊢ ∀ (m : ℕ), N ≤ m → I N = I m
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I n))

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
⊢ ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I N)) =
    ⨅ x, Ideal.under R (Ideal.map (algebraMap R (Localization.Away ↑x)) (I n))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
s : Subtype (Membership.mem S)
⊢ Ideal.map (floc ↑s) (I (minN ↑s)) = Ideal.map (algebraMap R (Localization.Away ↑s)) (I n)

Tactic:
]

Goal state after:
case h
R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN✝ : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN ↑s ≤ N
n : ℕ
hn : N ≤ n
s : Subtype (Membership.mem S)
⊢ Ideal.map (floc ↑s) (I (minN ↑s)) = Ideal.map (algebraMap R (Localization.Away ↑s)) (I n)
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
⊢ comap (algebraMap R x.asIdeal.ResidueField) ⊥ = x

Tactic:
]

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 x.asIdeal.ResidueField) ⊥ = x
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ ⊥

Tactic:
]

Goal state after:
case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ ⊥
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    ⇑(TopCat.Hom.hom f.base) ''
      (s ∩ Set.range ⇑(TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base))

Tactic:
]

Goal state after:
case e'_3
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝¹ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X},
    IsLocallyConstructible s → (∃ R, Y = Spec R) → IsLocallyConstructible (⇑f '' s)
hY : ¬∃ R, Y = Spec R
i : Y.affineCover.I₀
inst✝ : LocallyOfFinitePresentation (Cover.pullbackHom Y.affineCover f i)
inst : QuasiCompact (Cover.pullbackHom Y.affineCover f i)
e_1✝ : ↑↑(opensRange (Y.affineCover.f i)) = ↥↑(opensRange (Y.affineCover.f i))
⊢ ⇑f '' s ∩ ↑(opensRange (Y.affineCover.f i)) =
    ⇑(TopCat.Hom.hom f.base) ''
      (s ∩ Set.range ⇑(TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base))
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
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus {f})ᶜ ↔ x ∈ comap (algebraMap R A) '' (zeroLocus {f})ᶜ

Tactic:
]

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

Goal state before:
pp: case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ (¬∀ i < Module.finrank R (A ⧸ Ideal.span s),
        (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((algebraMap A (A ⧸ Ideal.span s)) f))).coeff i ∈
          x.asIdeal) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ

Tactic:
]

Goal state after:
case h
R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
x : PrimeSpectrum R
⊢ (¬∀ i < Module.finrank R (A ⧸ Ideal.span s),
        (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((algebraMap A (A ⧸ Ideal.span s)) f))).coeff i ∈
          x.asIdeal) ↔
    x ∈
      (zeroLocus
          ↑(Finset.image
              (LinearMap.charpoly ((Algebra.lmul R (A ⧸ Ideal.span s)) ((Ideal.Quotient.mk (Ideal.span s)) f))).coeff
              (Finset.range (Module.finrank R (A ⧸ Ideal.span s)))))ᶜ
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
⊢ e ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) = 0 ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0

Tactic:
]

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
f : R[X]
p : PrimeSpectrum R
⊢ (∃ i, f.coeff i ∉ p.asIdeal) ↔ p ∈ (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
p : PrimeSpectrum R
⊢ (∃ i, f.coeff i ∉ p.asIdeal) ↔ p ∈ (zeroLocus (Set.range f.coeff))ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
S : Set (Set (PrimeSpectrum R[X]))
hS : S ⊆ Set.range fun r ↦ ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image (comap C) '' S))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : PrimeSpectrum R
⊢ (fun x ↦ x) x = x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋃ i, (zeroLocus {↑i})ᶜ)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋃ i, (zeroLocus {↑i})ᶜ)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.hS
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
⊢ ⨆ i, ↑(fS i) = ⨆ i, Scheme.Hom.opensRange (𝒰.f i)

Tactic:
]

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

Goal state before:
pp: case inr
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible (⋃ i, ⇑f '' (s ∩ ↑(opensRange (𝒰.f i))))

Tactic:
]

Goal state after:
case inr
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} {s : Set ↥X},
    IsLocallyConstructible s →
      ∀ (R : CommRingCat) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
        (∃ S, X = Spec S) → IsLocallyConstructible (⇑f '' s)
hX : ¬∃ S, X = Spec S
inst : CompactSpace ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible (⋃ i, ⇑f '' (s ∩ ↑(opensRange (𝒰.f i))))
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (zeroLocus ↑t)ᶜ

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (zeroLocus ↑t)ᶜ