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

Goal state before:
pp: case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU'✝ : IsQuasiSeparated ⊥.carrier
f : ↑Γ(X, ⊥)
x : ↑Γ(X, X.basicOpen f)
⊢ X.basicOpen f = ⊥

Tactic:
eq_bot_iff

Goal state after:
case h
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU'✝ : IsQuasiSeparated ⊥.carrier
f : ↑Γ(X, ⊥)
x : ↑Γ(X, X.basicOpen f)
⊢ X.basicOpen f ≤ ⊥
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
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffine Y
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : ↑X.affineOpens
S : 𝒰.I₀ → ↑X.affineOpens := fun i ↦ ⟨Scheme.Hom.opensRange (𝒰.f i), ⋯⟩
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑U ⋯))

Tactic:
induction U using of_affine_open_cover S 𝒰.iSup_opensRange with

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.primeHeight = 0 ↔ I ∈ minimalPrimes R

Tactic:
← Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I.height = 0 ↔ I ∈ minimalPrimes R
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.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (𝟙 Γ(↑(𝟙 X ⁻¹ᵁ ↑U), ⊤)))

Tactic:
apply hP

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.primeHeight = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
← Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (x : I.IsMaximal), I.primeHeight) = ringKrullDim R

Tactic:
← Ideal.height_eq_primeHeight,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ ↑(⨆ I, ⨆ (_ : I.IsMaximal), I.height) = ringKrullDim R
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
⊢ s = 0

Tactic:
apply Presheaf.section_ext X.sheaf U s 0

Goal state after:
X : Scheme
inst✝ : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
U : X.Opens
s : ↑Γ(X, U)
hs : IsNilpotent s
⊢ ∀ (x : ↥X) (hx : x ∈ U),
    (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : ∀ (x : ↥X), _root_.IsReduced ↑(X.presheaf.stalk x)
⊢ IsReduced X

Tactic:
refine ⟨fun U => ⟨fun s hs => ?_⟩⟩
  apply Presheaf.section_ext X.sheaf U s 0
  intro x hx
  change (X.sheaf.presheaf.germ U x hx) s = (X.sheaf.presheaf.germ U x hx) 0
  rw [map_zero]
  change X.presheaf.germ U x hx s = 0
  exact (hs.map _).eq_zero

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
x : ↥X
hx : closure {x} ∈ irreducibleComponents ↥X
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
⊢ IsField ↑(X.presheaf.stalk x)

pp: X✝ X : Scheme
x : ↥X
hx : closure {x} ∈ irreducibleComponents ↥X
inst✝ : IsReduced X
hX : ∃ R, X = Spec R
⊢ IsField ↑(X.presheaf.stalk x)

Tactic:
· obtain ⟨i, x, rfl⟩ := X.affineCover.exists_eq x
    have inst : IsReduced (X.affineCover.X i) := isReduced_of_isOpenImmersion (X.affineCover.f i)
    refine (asIso <| (X.affineCover.f i).stalkMap x).commRingCatIsoToRingEquiv.isField
      (this _ x ?_ ⟨_, rfl⟩)
    rw [(X.affineCover.f i).isOpenEmbedding.closure_eq_preimage_closure_image, Set.image_singleton]
    exact preimage_mem_irreducibleComponents hx (X.affineCover.f i).isOpenEmbedding
      ⟨X.affineCover.f i x, subset_closure rfl, _, rfl⟩

Goal state after:
X✝ X : Scheme
x : ↥X
hx : closure {x} ∈ irreducibleComponents ↥X
inst✝ : IsReduced X
hX : ∃ R, X = Spec R
⊢ IsField ↑(X.presheaf.stalk x)
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)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
⊢ Ideal.span (Set.range r) = ⊤

Tactic:
rw [← V.2.self_le_iSup_basicOpen_iff]

Goal state after:
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)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
⊢ ↑V ≤ ⨆ f, X.basicOpen ↑f
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ f = φ ≫ i.inv

Tactic:
apply Spec.map_injective

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := ⋯
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) := ⋯
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ Spec.map f = Spec.map (φ ≫ i.inv)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case neg
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hxU : x ∉ ↑U
⊢ x ∈ I.supportSet ∩ ↑↑U ↔ x ∈ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

Tactic:
simp [hxU]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ ↑Z ↔ x ∈ ↑Z ∩ ↑↑U

Tactic:
simp [hxU]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)) ∩ ↑↑U ↔
    x ∈ X.zeroLocus ↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z))

Tactic:
simp [hxU]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯) ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V

Tactic:
rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
          exact fun x _ ↦ by simpa using (F x).2.2

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) ≫
      Spec.map T.tensorInr =
    (Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr

Tactic:
rw [← cancel_mono <| Y.fromSpecResidueField T.y]
    simp_rw [Category.assoc, ← T.specTensorTo_snd, tensorCongr_SpecTensorTo_assoc]
    rw [← Hom.SpecMap_residueFieldMap_fromSpecResidueField_assoc, ofPointTensor_SpecTensorTo_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↥(pullback f' g')
x : ↥X
hx : i₁ x = (pullback.fst f' g') z
y : ↥Y
hy : i₂ y = (pullback.snd f' g') z
⊢ z ∈ Set.range ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)

Tactic:
let T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x hx.symm

Goal state after:
case mpr
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
z : ↥(pullback f' g')
x : ↥X
hx : i₁ x = (pullback.fst f' g') z
y : ↥Y
hy : i₂ y = (pullback.snd f' g') z
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
⊢ z ∈ Set.range ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app f ↑U ≫ e.hom = (ΓSpecIso Γ(Y, ↑U)).inv ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)

Tactic:
← (Iso.inv_comp_eq _).mpr U.2.isoSpec_inv_appTop,

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : ↑Y.affineOpens
e : Γ(X, f ⁻¹ᵁ ↑U) ≅ Γ(pullback f (↑U).ι, ⊤) :=
  Functor.mapIso X.presheaf (eqToIso ⋯).op ≪≫ Hom.appIso (pullback.fst f (↑U).ι) ⊤
⊢ Hom.app f ↑U ≫ e.hom =
    ((↑U).topIso.inv ≫ Hom.appTop (IsAffineOpen.isoSpec ⋯).inv) ≫ Hom.appTop (pullback.snd f (↑U).ι ≫ (↑U).toSpecΓ)
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)
⊢ IsClosedEmbedding ⇑f

Tactic:
have h := (f ≫ g).isClosedEmbedding

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsClosedImmersion g
inst✝ : IsClosedImmersion (f ≫ g)
h : IsClosedEmbedding ⇑(f ≫ g)
⊢ IsClosedEmbedding ⇑f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

Goal state before:
pp: case mp
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J ≤ I.map f
⊢ J.comap f ≤
    Hom.ker (pullback.lift I.subschemeι (Hom.toImage (I.subschemeι ≫ f) ≫ inclusion H) ⋯ ≫ pullback.fst f J.subschemeι)

Tactic:
exact Hom.le_ker_comp _ _

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

Goal state before:
pp: case mpr
X Y : Scheme
I : X.IdealSheafData
f : X ⟶ Y
J : Y.IdealSheafData
H : J.comap f ≤ I
this : (inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι = I.subschemeι ≫ f
⊢ Hom.ker J.subschemeι ≤ Hom.ker ((inclusion H ≫ (J.comapIso f).hom ≫ pullback.snd f J.subschemeι) ≫ J.subschemeι)

Tactic:
exact Hom.le_ker_comp _ _

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

Goal state before:
pp: X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : ↑X.affineOpens
⊢ (I.comap f).ideal U = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso f ↑U).inv) (I.ideal ⟨f ''ᵁ ↑U, ⋯⟩)

Tactic:
by
  refine (ker_ideal_of_isPullback_of_isOpenImmersion _ _ _ _
    (IsPullback.of_hasPullback f I.subschemeι) U).trans ?_
  simp

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ IsSeparated f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsSeparated) _
      (iSup_affineOpens_eq_top Y)]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
h : IsAffineHom f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f], IsAffine Y → IsSeparated f
hY : ¬IsAffine Y
⊢ ∀ (i : ↑Y.affineOpens), IsSeparated (f ∣_ ↑i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ IsDominant (Scheme.Hom.coborderRange f).ι

Tactic:
rw [isDominant_iff, DenseRange, Scheme.Opens.range_ι]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
inst✝ : IsImmersion f
⊢ Dense ↑(Scheme.Hom.coborderRange f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this :
  IsClosedImmersion
    (pullback.diagonal f ≫
      (pullbackDiagonalMapIdIso f f g).inv ≫
        pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))
⊢ IsSeparated f

Tactic:
exact ⟨@IsClosedImmersion.of_comp _ _ _ _ _ this inferInstance⟩

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 f '' comap g '' s)

Tactic:
exact H₁ _ (H₂ _ hs)

Goal state after:
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
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:
rintro ⟨q, ⟨hqg, hqf⟩, rfl⟩ H

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
hqg : q ∈ zeroLocus s
hqf : q ∉ zeroLocus {f}
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
⊢ False
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 ⊆ ↑(RingHom.ker (algebraMap A q.asIdeal.ResidueField))

Tactic:
Ideal.ker_algebraMap_residueField

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.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 ∈ RingHom.ker (algebraMap A q.asIdeal.ResidueField)
⊢ False

Tactic:
Ideal.ker_algebraMap_residueField

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: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ comap C '' ↑(basicOpen f) = (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
ext p
  rw [mem_image_comap_C_basicOpen]
  simp [Set.range_subset_iff]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
⊢ comap C '' ↑(basicOpen f) = (zeroLocus (Set.range fun m ↦ coeff m f))ᶜ

Tactic:
ext p
  rw [mem_image_comap_C_basicOpen]
  simp [Set.range_subset_iff]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ comap ((eval₂Hom (RingHom.id R) 0).comp C) x = x

Tactic:
(show (eval₂Hom (.id _) 0).comp C = .id R by ext; simp),

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ comap (RingHom.id R) x = x
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝⁴ : GeometricallyIntegral f
inst✝³ : Flat f
inst✝² : UniversallyOpen f
inst✝¹ : IsIntegral S
inst✝ : IsLocallyNoetherian S
⊢ IsIntegral X

Tactic:
by
  rw [isIntegral_iff_irreducibleSpace_and_isReduced]
  exact ⟨GeometricallyIrreducible.irreducibleSpace f f.isOpenMap,
    GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian f⟩

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

Goal state before:
pp: case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ LocallyOfFiniteType (Spec.map φ)

Tactic:
HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)

Goal state after:
case inr
S : CommRingCat
inst✝² : JacobsonSpace ↥(Spec S)
R : CommRingCat
inst✝¹ : Subsingleton ↥(Spec R)
inst✝ : IsReduced (Spec R)
h✝ : Nonempty ↥(Spec R)
this✝ : IrreducibleSpace ↥(Spec R)
this : IsDomain ↑R
φ : S ⟶ R
⊢ (CommRingCat.Hom.hom φ).Finite ↔ (CommRingCat.Hom.hom φ).FiniteType
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
y : ↥Y
⊢ IsCompact (⇑f ⁻¹' {y})

Tactic:
have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : UniversallyClosed f
y : ↥Y
this : CompactSpace ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (⇑f ⁻¹' {y})
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
g : s.pt ⟶ cF.pt
hg : ∀ (j : I), g ≫ cF.π.app j = s.π.app j
⊢ g ≫ cF.π.app (Classical.arbitrary I) =
    ⋯.lift (s.π.app (Classical.arbitrary I)) (hcG.lift ((Cone.postcompose α).obj s)) ⋯ ≫
      cF.π.app (Classical.arbitrary I)

Tactic:
simp [hg]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
g : cG.pt ⟶ s.pt
hg : ∀ (j : I), cG.ι.app j ≫ g = s.ι.app j
⊢ ∀ (j : I),
    cF.ι.app j ≫ f.hom ≫ g =
      cF.ι.app j ≫ f.hom ≫ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app (Classical.arbitrary I)) ⋯

Tactic:
simp [hg]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
g : cG.pt ⟶ s.pt
hg : ∀ (j : I), cG.ι.app j ≫ g = s.ι.app j
⊢ cG.ι.app (Classical.arbitrary I) ≫ g =
    cG.ι.app (Classical.arbitrary I) ≫
      ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app (Classical.arbitrary I)) ⋯

Tactic:
simp [hg]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineSpace

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

Tactic:
intro i
          rw [CommRingCat.comp_apply, ConcreteCategory.hom_ofHom, coe_eval₂Hom]
          simp only [eval₂_X]
          exact homOfVector_appTop_coord _ _ _

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite

Tactic:
suffices (f ⁻¹' (U ∩ {z | (f ⁻¹' {z} ∩ c.support).Nonempty}) ∩ c.support).Finite from
      (this.image f).subset (fun a ha ↦ by grind [Set.Nonempty])

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y : Y
x✝ : y ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y ∈ U ∧ U ⊆ ⊤
⊢ (f ⁻¹' (U ∩ {z | (f ⁻¹' {z} ∩ locallyFinsuppWithin.support c).Nonempty}) ∩ locallyFinsuppWithin.support c).Finite
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case H
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x

Tactic:
apply Spec.map_injective

Goal state after:
case H
X Y : Scheme
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) = Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)