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

Goal state before:
pp: case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑f₁ ∩ Set.range ⇑f₂)
⊢ CompactSpace ↥(pullback f₁ f₂)

Tactic:
isCompact_iff_compactSpace

Goal state after:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ ↑(Set.range ⇑f₁ ∩ Set.range ⇑f₂)
H : ∀ (U V : ↑X.affineOpens), CompactSpace ↑(↑↑U ∩ ↑↑V)
⊢ CompactSpace ↥(pullback f₁ f₂)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ IsCompact ↑U ↔ ∃ R f, Set.range ⇑f = ↑U

Tactic:
refine isCompact_iff_compactSpace.trans ((compactSpace_iff_exists (X := U)).trans ?_)

Goal state after:
X : Scheme
U : X.Opens
⊢ (∃ R f, Function.Surjective ⇑f) ↔ ∃ R f, Set.range ⇑f = ↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ (fun x ↦ ⇑U.ι '' x) (Set.range ⇑(IsOpenImmersion.lift U.ι f ⋯)) = (fun x ↦ ⇑U.ι '' x) Set.univ

Tactic:
simp only [Set.image_univ, Scheme.Opens.range_ι]

Goal state after:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ (fun a ↦ U.ι a) '' Set.range ⇑(IsOpenImmersion.lift U.ι f ⋯) = ↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
S : ↑X.affineOpens
U₁ U₂ : X.Opens
n₁ n₂ : ℕ
y₁ : ↑Γ(X, U₁)
y₂ : ↑Γ(X, U₂)
f : ↑Γ(X, U₁ ⊔ U₂)
x : ↑Γ(X, X.basicOpen f)
h₁ : ↑S ≤ U₁
h₂ : ↑S ≤ U₂
e₁ :
  (y₁ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ =
    ((f |_ U₁) ⋯ |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯ ^ n₁ * (x |_ X.basicOpen ((f |_ U₁) ⋯)) ⋯
e₂ :
  (y₂ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ =
    ((f |_ U₂) ⋯ |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯ ^ n₂ * (x |_ X.basicOpen ((f |_ U₂) ⋯)) ⋯
⊢ (algebraMap ↑Γ(X, ↑S) ↑Γ(X, X.basicOpen ((f |_ ↑S) ⋯))) ((((f |_ U₁) ⋯ ^ n₂ * y₁) |_ ↑S) h₁) =
    (algebraMap ↑Γ(X, ↑S) ↑Γ(X, X.basicOpen ((f |_ ↑S) ⋯))) ((((f |_ U₂) ⋯ ^ n₁ * y₂) |_ ↑S) h₂)

Tactic:
apply exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux (e₁ := e₁) (e₂ := e₂)
    · change X.basicOpen _ ≤ _
      simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
      exact inf_le_inf h₁ le_rfl
    · change X.basicOpen _ ≤ _
      simp only [TopCat.Presheaf.restrictOpenCommRingCat_apply, Scheme.basicOpen_res]
      exact inf_le_inf h₂ le_rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ I.height < J.height

Tactic:
by_cases hJ : J = ⊤
  · grw [hJ, height_top]
    exact I.height_lt_top IsPrime.ne_top'
  · rw [← ENat.add_one_le_iff (I.height_ne_top IsPrime.ne_top'), J.height_eq_inf_minimalPrimes]
    refine le_iInf₂ (fun K hK ↦ ?_)
    have := hK.isPrime
    have : I < K := lt_of_lt_of_le h hK.le
    exact Ideal.height_add_one_le_of_lt_of_isPrime this

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
have : HasRingHomProperty Q (fun f ↦ P (Spec.map (CommRingCat.ofHom f))) :=
      ⟨isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget P, rfl⟩

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ P = affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
⊢ ∃ n, s ^ n * f = 0

Tactic:
by
  suffices h : ∃ n, s ^ n * f = s ^ n * 0 by
    simpa using h
  apply exists_of_res_eq_of_qcqs hU hU'
  simpa

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

Goal state before:
pp: case mpr
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ (∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}) → IsOpenImmersion (Spec.map f)

Tactic:
rintro ⟨e, he, he'⟩

Goal state after:
case mpr
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
e : ↑R
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}
⊢ IsOpenImmersion (Spec.map f)
Module: Mathlib.AlgebraicGeometry.Morphisms.IsIso

Goal state before:
pp: ⊢ isomorphisms Scheme =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f

Tactic:
isomorphisms_eq_isOpenImmersion_inf_surjective,

Goal state after:
⊢ IsOpenImmersion ⊓ @Surjective =
    (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f ↦ Function.Bijective ⇑f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
⊢ I ≤ J

Tactic:
by
  intro U
  rw [← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)),
    ← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) J (le_top (a := U.1))]
  exact Ideal.map_mono H

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: case refine_1
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ⟨x, ⟨f, hf⟩⟩.fst =
    ((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
        ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).fst

pp: case refine_2
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ↑⟨x, ⟨f, hf⟩⟩.snd =
    (X.presheaf.stalkCongr ⋯).hom ≫
      ↑((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
            ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).snd

Tactic:
· simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint,
        Scheme.fromSpecStalk_closedPoint]

Goal state after:
case refine_2
X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
hf : IsLocalHom (CommRingCat.Hom.hom f)
⊢ ↑⟨x, ⟨f, hf⟩⟩.snd =
    (X.presheaf.stalkCongr ⋯).hom ≫
      ↑((fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
            ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) ⟨x, ⟨f, hf⟩⟩)).snd
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
x : ↥(Spec S)
hx : x ∈ ↑(ker f).support
⊢ x ∈ closure (Set.range ⇑f)

Tactic:
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›

Goal state after:
case inr
X✝ Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f],
    (∃ R, X = Spec R) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hX : ¬∃ R, X = Spec R
x : ↥(Spec S)
hx : x ∈ ↑(ker f).support
inst : CompactSpace ↥X
⊢ x ∈ closure (Set.range ⇑f)
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
T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x ⋯
w₁ : ↥(pullback (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) := Triplet.mk' w₁ w₂ ⋯
⊢ z ∈ Set.range ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)

Tactic:
obtain ⟨t, _, ht₂⟩ := T.exists_preimage

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 ⋯
w₁ : ↥(pullback (pullback.fst f' g') i₁)
hw₁ : (pullback.fst (pullback.fst f' g') i₁) w₁ = T₁.x ∧ (pullback.snd (pullback.fst f' g') i₁) w₁ = T₁.y
T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y ⋯
w₂ : ↥(pullback (pullback.snd f' g') i₂)
hw₂ : (pullback.fst (pullback.snd f' g') i₂) w₂ = T₂.x ∧ (pullback.snd (pullback.snd f' g') i₂) w₂ = T₂.y
T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) := Triplet.mk' w₁ w₂ ⋯
t : ↥(pullback (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂))
left✝ : (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.x
ht₂ : (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) t = T.y
⊢ 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
⊢ toImage f ≫ imageι f = f

Tactic:
convert f.toImageAux_spec

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ toImage f = toImageAux f
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
⊢ P ≤ @IsAffineHom

Tactic:
intro X Y f hf

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
hf : P f
⊢ IsAffineHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.Separated

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

Tactic:
by
  ext
  exact isSeparated_iff _

Goal state after:
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
h✝ : Nontrivial R
⊢ Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A

Tactic:
Module.finrank_tensorProduct,

Goal state after:
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
⊢ Module.finrank I.ResidueField I.ResidueField * Module.finrank R A = Module.finrank R A
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: case refine_1
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_2
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
hf' : (RingHom.ker f).FG
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsRetrocompact (zeroLocus ↑(RingHom.ker f))ᶜ

Tactic:
exact isRetrocompact_zeroLocus_compl_of_fg hf'

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
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›

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
⊢ IsLocallyConstructible (⇑f '' s)
Module: Mathlib.AlgebraicGeometry.Noetherian

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

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

Tactic:
· intro h i
    let U := Scheme.Hom.opensRange (𝒰.f i)
    have := h.component_noetherian ⟨U, isAffineOpen_opensRange _⟩
    apply isNoetherianRing_of_ringEquiv (R := Γ(X, U))
    apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
    exact (IsOpenImmersion.ΓIsoTop (𝒰.f i)).symm

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

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ IsArtinianRing ↑Γ(X, ↑U)

Tactic:
rw [isArtinianRing_iff_krullDimLE_zero, Ring.KrullDimLE, Order.krullDimLE_iff, ← ringKrullDim,
      Nat.cast_zero, ← PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim Γ(X, U)]

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
x✝ : IsNoetherianRing ↑Γ(X, ↑U)
⊢ topologicalKrullDim (PrimeSpectrum ↑Γ(X, ↑U)) ≤ 0
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X

Tactic:
· intro h
    convert! IsNoetherian.mk
    · exact isLocallyNoetherian_of_affine_cover hS h
    · constructor
      rw [← Opens.coe_top, ← hS, Opens.iSup_mk]
      apply isCompact_iUnion
      intro i
      apply isCompact_iff_isCompact_univ.mpr
      convert! CompactSpace.isCompact_univ
      have : NoetherianSpace (S i) := by
        apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2
      apply NoetherianSpace.compactSpace (S i)

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

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

Tactic:
by
  refine ⟨fun hf K _ _ ↦ pullback_of_geometrically hf _ _, fun H ↦ ?_⟩
  rw [geometrically_iff_of_isClosedUnderIsomorphisms]
  intro K _ y
  obtain ⟨φ, rfl⟩ := Spec.map_surjective y
  algebraize [φ.hom]
  exact H K

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

Goal state before:
pp: X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ ⊥.map g = ⊥

Tactic:
Scheme.IdealSheafData.map_bot,

Goal state after:
X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ Scheme.Hom.ker g = ⊥
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: ⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral

Tactic:
apply isIntegral_stableUnderComposition.respectsIso

Goal state after:
⊢ ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    IsIntegralHom f ∧ LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔ IsFinite f ∧ monomorphisms Scheme f

Tactic:
IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsClosedImmersion f ↔ IsFinite f ∧ Mono f)
hY : ¬IsAffine Y
⊢ IsClosedImmersion f ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      monomorphisms Scheme f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
IsZariskiLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
inst✝ : JacobsonSpace ↥Y
this :
  ∀ {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y],
    (∃ S, Y = Spec S) → (IsFinite f ↔ LocallyOfFiniteType f)
hY : ¬∃ S, Y = Spec S
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    LocallyOfFiniteType f
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case e'_1
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
toSpecΓ_preimage_basicOpen

Goal state after:
case e'_1
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ X.basicOpen r = X.basicOpen r
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: case e'_3.e'_6
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1✝ : ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) = ↑(X.basicOpen r)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
toSpecΓ_preimage_basicOpen

Goal state after:
case e'_3.e'_6
X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this✝ : QuasiSeparatedSpace ↥X
x : ↥X
r : ↑Γ(X, ⊤)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1✝ : ↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) = ↑(X.basicOpen r)
⊢ X.basicOpen r = X.basicOpen r
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
hw : w ∉ s
⊢ 0 = D w

Tactic:
have : w ∉ support D := by simpa only [hs, Set.Finite.mem_toFinset] using hw

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : (support D).Finite
w : X
s : Finset X := h.toFinset
hs : s = h.toFinset
hw : w ∉ s
this : w ∉ support D
⊢ 0 = D w
Module: Mathlib.AlgebraicGeometry.SpreadingOut

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

Tactic:
have := hU.isLocalization_basicOpen f

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ t = 0
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst✝ : IsLocallyNoetherian X
⊢ X.IsGermInjective

Tactic:
suffices ∀ (R : CommRingCat.{u}) (_ : IsNoetherianRing R), (Spec R).IsGermInjective by
    refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
    exact isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))
  refine fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_
  let J := RingHom.ker <| algebraMap R (Localization.AtPrime I)
  have hJ (x) : x ∈ J ↔ ∃ y : I.primeCompl, y * x = 0 :=
    IsLocalization.map_eq_zero_iff I.primeCompl _ x
  choose f hf using fun x ↦ (hJ x).mp
  obtain ⟨s, hs⟩ := (isNoetherianRing_iff_ideal_fg R).mp ‹_› J
  have hs' : (s : Set R) ⊆ J := hs ▸ Ideal.subset_span
  refine ⟨_, (s.attach.prod fun x ↦ f x (hs' x.2)).2, fun x y e hy ↦ ⟨1, ?_⟩⟩
  rw [pow_one, mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton]
  refine SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)
  rw [← hs, Ideal.span_le]
  intro i hi
  rw [SetLike.mem_coe, Submodule.mem_annihilator_span_singleton, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton, Submonoid.coe_finsetProd]
  refine Ideal.mem_of_dvd _ (Finset.dvd_prod_of_mem _ (s.mem_attach ⟨i, hi⟩)) ?_
  rw [Submodule.mem_annihilator_span_singleton, smul_eq_mul]
  exact hf i _

Goal state after: