awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst_2 : LocallyOfFiniteType f
x : ↥X
hx : IsClosed (X := ↥X) {x}
p : { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
pf : IsLocalRing.{u} (↑(CommRingCat.of K) : Type u)
h : IsClosed (X := ↥X) (singleton (α := ↥X) ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X))
pf_1 :
  IsLocalHom (R := (↑(X.presheaf.stalk ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K))) : Type u))
    (S := (↑(CommRingCat.of K) : Type u)) (F :=
    (↑(X.presheaf.stalk ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K))) : Type u) →+*
      (↑(CommRingCat.of K) : Type u))
    (CommRingCat.Hom.hom (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
a : 𝟙 (Spec (CommRingCat.of K)) = (↑p : Spec (CommRingCat.of K) ⟶ X) ≫ f
a₁ a₂ : 𝟙 (Spec (CommRingCat.of K)) = 𝟙 (Spec (CommRingCat.of K))
⊢ 𝟙 (Spec (CommRingCat.of K)) =
    CategoryStruct.comp (Y := Spec (X.residueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K))))
      (Spec.map (Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X))))
      (X.fromSpecResidueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ≫ f)

Tactic:
rw [reassoc_of% Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, p.2]

Premises used: AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst_2 : LocallyOfFiniteType f
x_1 : ↥X
hx : IsClosed (X := ↥X) {x_1}
x : (↑(closedPoints ↥X) : Type u)
⊢ (fun (p : { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }) ↦
        (Subtype.mk (p := fun (x : ↥X) ↦ Membership.mem (γ := Set ↥X) (closedPoints ↥X) x)
            ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⋯ :
          { x : ↥X // Membership.mem (γ := Set ↥X) (closedPoints ↥X) x }))
      ((fun (x : (↑(closedPoints ↥X) : Type u)) ↦
          (Subtype.mk (p := fun (p : Spec (CommRingCat.of K) ⟶ X) ↦ p ≫ f = 𝟙 (Spec (CommRingCat.of K)))
              (pointOfClosedPoint f (↑x : ↥X) ⋯) ⋯ :
            { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : Spec (CommRingCat.of K) ⟶ X
h : X ⟶ Spec (CommRingCat.of K)
inst_2 : LocallyOfFiniteType h
hf : f ≫ h = 𝟙 (Spec (CommRingCat.of K))
hg : g ≫ h = 𝟙 (Spec (CommRingCat.of K))
H : Eq (α := ↥X) (f (IsLocalRing.closedPoint K) : ↥X) (g (IsLocalRing.closedPoint K) : ↥X)
⊢ f = g

Tactic:
congr($((pointEquivClosedPoint h).injective (a₁ := ⟨f, hf⟩) (a₂ := ⟨g, hg⟩) (Subtype.ext H)).1)

Premises used: congrArg, AlgebraicGeometry.pointEquivClosedPoint, id, Equiv.injective, Subtype.val, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
⊢ JacobsonSpace.{u} ↥X

Tactic:
have : JacobsonSpace ↥X := LocallyOfFiniteType.jacobsonSpace (f ≫ i)
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
⊢ f = g

Tactic:
ext_of_fromSpecResidueField_eq f g i (S ∩ closedPoints X) ?_ ?_ H'

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.ext_of_fromSpecResidueField_eq, closedPoints, Inter.inter, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
refine_1 : Dense (S ∩ closedPoints ↥X)
refine_2 : ∀ x ∈ S ∩ closedPoints ↥X, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
⊢ f = g

Tactic:
refine ext_of_fromSpecResidueField_eq f g i (S ∩ closedPoints X) ?_ ?_ H'

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.ext_of_fromSpecResidueField_eq, closedPoints, Inter.inter, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
refine_1 : closure (S ∩ closedPoints ↥X) = Set.univ
refine_1₁ : closure S = Set.univ
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : Dense S
⊢ Dense (S ∩ closedPoints ↥X)

Tactic:
rwa [dense_iff_closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      ← dense_iff_closure_eq]

Premises used: dense_iff_closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
x : ↥X
refine_2 :
  ∀ (hxS : x ∈ S) (hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x),
    X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
⊢ x ∈ S ∩ closedPoints ↥X → X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g

Tactic:
⟨hxS, hx⟩
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
x : ↥X
hxS : x ∈ S
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
refine_2 :
  Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f =
    Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g
⊢ X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g

Tactic:
rw [← cancel_epi (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom)]

Premises used: AlgebraicGeometry.residueFieldIsoBase, AlgebraicGeometry.Spec.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
x : ↥X
hxS : x ∈ S
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
⊢ Eq (α := ↥Y)
    ((Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) (IsLocalRing.closedPoint K) : ↥Y)
    ((Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) (IsLocalRing.closedPoint K) : ↥Y)

Tactic:
simpa using H x hxS hx
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
x : ↥X
hxS : x ∈ S
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
refine_2 :
  (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) ≫ i = 𝟙 (Spec (CommRingCat.of K))
refine_2₁ :
  (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) ≫ i = 𝟙 (Spec (CommRingCat.of K))
⊢ Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f =
    Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g

Tactic:
refine ext_of_apply_closedPoint_eq i ?_ ?_ (by simpa using H x hxS hx)

Premises used: AlgebraicGeometry.ext_of_apply_closedPoint_eq
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
x : ↥X
hxS : x ∈ S
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) ≫ i = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp only [Category.assoc, ← SpecMap_residueFieldIsoBase_inv (f ≫ i) x hx, ← Spec.map_comp,
        Iso.inv_hom_id, Spec.map_id, ← H']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Spec.map_comp, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X Y : Scheme
K : Type u
inst : Field K
inst_1 : IsAlgClosed K
f g : X ⟶ Y
i : Y ⟶ Spec (CommRingCat.of K)
inst_2 : IsSeparated i
inst_3 : LocallyOfFiniteType i
inst_4 : IsReduced X
inst_5 : LocallyOfFiniteType (f ≫ i)
S : Set ↥X
hS : IsLocallyClosed S
hS' : Dense S
H : ∀ x ∈ S, IsClosed (X := ↥X) {x} → Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H' : f ≫ i = g ≫ i
this : JacobsonSpace.{u} ↥X
x : ↥X
hxS : x ∈ S
hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x
⊢ (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) ≫ i = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp only [Category.assoc, ← SpecMap_residueFieldIsoBase_inv (f ≫ i) x hx, ← Spec.map_comp,
        Iso.inv_hom_id, Spec.map_id, ← H']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Spec.map_comp, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
h : IsLocallyArtinian X
inst : IsAffine X
⊢ IsArtinianRing.{u} (↑Γ(X, ⊤) : Type u)

Tactic:
h.1 ⟨⊤, isAffineOpen_top X⟩

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, Subtype.mk, Top.top
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
h : topologicalKrullDim.{u} ↥X ≤ 0
U : (↑X.affineOpens : Type u)
⊢ IsNoetherianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)

Tactic:
have _ : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian U
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
h : topologicalKrullDim.{u} ↥X ≤ 0
U : (↑X.affineOpens : Type u)
h_1 : IsNoetherianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
rw : topologicalKrullDim.{u} (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) ≤ 0
⊢ IsArtinianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)

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

Premises used: CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, ringKrullDim, Nat.cast_zero, Subtype.val, Ring.KrullDimLE, CategoryTheory.Functor.obj, isArtinianRing_iff_krullDimLE_zero, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Order.krullDimLE_iff
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
h : topologicalKrullDim.{u} ↥X ≤ 0
U : (↑X.affineOpens : Type u)
h_1 : IsNoetherianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
rw : topologicalKrullDim.{u} ↥(↑(↑U : X.Opens) : Scheme) ≤ 0
⊢ topologicalKrullDim.{u} ↥(Spec Γ(X, (↑U : X.Opens))) ≤ 0

Tactic:
rw [← IsHomeomorph.topologicalKrullDim_eq _ U.2.isoSpec.hom.homeomorph.isHomeomorph]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Scheme.Hom.homeomorph, Homeomorph.isHomeomorph, IsHomeomorph.topologicalKrullDim_eq, CategoryTheory.Iso.hom, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
h : topologicalKrullDim.{u} ↥X ≤ 0
U : (↑X.affineOpens : Type u)
h_1 : IsNoetherianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ topologicalKrullDim.{u} ↥(↑(↑U : X.Opens) : Scheme) ≤ 0

Tactic:
(topologicalKrullDim_subspace_le X U).trans h

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, Set.Mem, topologicalKrullDim_subspace_le, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, SetLike.coe, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, LE.le.trans, Subtype.val, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
h : topologicalKrullDim.{u} ↥X ≤ 0
U : (↑X.affineOpens : Type u)
h_1 : IsNoetherianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ topologicalKrullDim.{u} ↥(↑(↑U : X.Opens) : Scheme) ≤ 0

Tactic:
exact (topologicalKrullDim_subspace_le X U).trans h

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, topologicalKrullDim_subspace_le, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, SetLike.coe, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, LE.le.trans, Subtype.val, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
inst_1 : DiscreteTopology.{u} ↥X
⊢ IsLocallyArtinian X

Tactic:
.of_topologicalKrullDim_le_zero (topologicalKrullDim_zero_of_discreteTopology X)

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, topologicalKrullDim_zero_of_discreteTopology, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.IsLocallyArtinian.of_topologicalKrullDim_le_zero, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
U : X.Opens
⊢ IsLocallyArtinian.{u} (↑U : Scheme)

Tactic:
.of_isOpenImmersion U.ι

Premises used: _private.0.AlgebraicGeometry.IsLocallyArtinian.of_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
U : Scheme.OpenCover.{u_1, u} X
i : U.I₀
⊢ IsLocallyArtinian.{u} (U.X i)

Tactic:
.of_isOpenImmersion (U.f i)

Premises used: CategoryTheory.PreZeroHypercover.f, _private.0.AlgebraicGeometry.IsLocallyArtinian.of_isOpenImmersion, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
apply : ∀ (a : ↥X), IsOpen (X := ↥X) {a}
⊢ DiscreteTopology.{u} ↥X

Tactic:
apply discreteTopology_iff_isOpen_singleton.mpr

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
x : ↥X
obtain : ∀ (W : X.Opens) (hW1 : IsAffineOpen W) (hW2 : x ∈ W), W.carrier ⊆ (↑⊤ : Set ↥X) → IsOpen (X := ↥X) {x}
⊢ IsOpen (X := ↥X) {x}

Tactic:
obtain ⟨W, hW1, hW2, _⟩ := exists_isAffineOpen_mem_and_subset (TopologicalSpace.Opens.mem_top x)

Premises used: TopologicalSpace.Opens.mem_top, AlgebraicGeometry.exists_isAffineOpen_mem_and_subset
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right : W.carrier ⊆ (↑⊤ : Set ↥X)
⊢ IsArtinianRing.{u} (↑Γ(X, W) : Type u)

Tactic:
have : IsArtinianRing Γ(X, W) := IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hW1⟩
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right : W.carrier ⊆ (↑⊤ : Set ↥X)
this : IsArtinianRing.{u} (↑Γ(X, W) : Type u)
⊢ DiscreteTopology.{u} ↥(Spec Γ(X, W))

Tactic:
have : DiscreteTopology (Spec Γ(X, W)) := inferInstanceAs (DiscreteTopology (PrimeSpectrum _))
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right : W.carrier ⊆ (↑⊤ : Set ↥X)
this_1 : IsArtinianRing.{u} (↑Γ(X, W) : Type u)
this : DiscreteTopology.{u} ↥(Spec Γ(X, W))
⊢ DiscreteTopology.{u} ↥(↑W : Scheme)

Tactic:
have : DiscreteTopology W := hW1.isoSpec.hom.homeomorph.symm.discreteTopology
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
x : ↥X
W : X.Opens
hW1 : IsAffineOpen W
hW2 : x ∈ W
right : W.carrier ⊆ (↑⊤ : Set ↥X)
this_1 : IsArtinianRing.{u} (↑Γ(X, W) : Type u)
this_2 : DiscreteTopology.{u} ↥(Spec Γ(X, W))
this : DiscreteTopology.{u} ↥(↑W : Scheme)
⊢ IsOpen (X := ↥X) {x}

Tactic:
simpa using (isOpen_discrete ({⟨x, hW2⟩} : Set W)).trans W.2

Premises used: IsOpen.trans, isOpen_discrete, TopologicalSpace.Opens.is_open', Singleton.singleton
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
⊢ IsLocallyArtinian X ↔ IsLocallyNoetherian X ∧ DiscreteTopology.{u} ↥X

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ .of_isLocallyNoetherian_of_discreteTopology⟩

Premises used: inferInstance, _private.0.AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.match_1, AlgebraicGeometry.IsLocallyArtinian, And.intro, Iff.intro, AlgebraicGeometry.IsLocallyArtinian.of_isLocallyNoetherian_of_discreteTopology
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsImmersion f
inst_1 : IsLocallyArtinian Y
⊢ IsLocallyArtinian X

Tactic:
iff_isLocallyNoetherian_and_discreteTopology.mpr
    ⟨LocallyOfFiniteType.isLocallyNoetherian f, f.isEmbedding.discreteTopology⟩

Premises used: Iff.mpr, AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, AlgebraicGeometry.Scheme.Hom.isEmbedding, Topology.IsEmbedding.discreteTopology, And.intro
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
⊢ IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)

Tactic:
⟨fun h ↦ inferInstance, fun H ↦ ?_⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
refine : ∀ (H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)), IsLocallyArtinian X
⊢ IsLocallyArtinian X ↔ ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)

Tactic:
refine ⟨fun h ↦ inferInstance, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
⊢ IsLocallyArtinian X

Tactic:
IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, And.intro
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
refine_1 : IsLocallyNoetherian X
refine_2 : DiscreteTopology.{u} ↥X
⊢ IsLocallyArtinian X

Tactic:
refine IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, AlgebraicGeometry.IsLocallyArtinian.iff_isLocallyNoetherian_and_discreteTopology, And.intro
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
⊢ IsLocallyNoetherian X

Tactic:
(isLocallyNoetherian_iff_openCover 𝒰).mpr inferInstance

Premises used: Iff.mpr, inferInstance, AlgebraicGeometry.isLocallyNoetherian_iff_openCover
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
⊢ IsLocallyNoetherian X

Tactic:
exact (isLocallyNoetherian_iff_openCover 𝒰).mpr inferInstance

Premises used: Iff.mpr, inferInstance, AlgebraicGeometry.isLocallyNoetherian_iff_openCover
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
⊢ DiscreteTopology.{u} ↥X

Tactic:
discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
refine_2 : ∀ (x : ↥X), IsOpen (X := ↥X) {x}
⊢ DiscreteTopology.{u} ↥X

Tactic:
refine discreteTopology_iff_isOpen_singleton.mpr fun x ↦ ?_

Premises used: Iff.mpr, discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
x : ↥X
refine_2 : ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)), IsOpen (X := ↥X) (singleton (α := ↥X) ((𝒰.f i) x : ↥X))
⊢ IsOpen (X := ↥X) {x}

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u} X
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian.{u} (𝒰.X i)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ IsOpen (X := ↥X) (singleton (α := ↥X) ((𝒰.f i) x : ↥X))

Tactic:
simpa using (𝒰.f i).isOpenEmbedding.isOpenMap _ (isOpen_discrete {x})

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, isOpen_discrete, Singleton.singleton, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Artinian
Goal:
X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
⊢ IsLocallyArtinian X ↔ ∀ (i : ι), IsArtinianRing.{u} (↑Γ(X, U i) : Type u)

Tactic:
⟨fun _ _ ↦ IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hU' _⟩, fun H ↦ ?_⟩

Premises used: AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj, Subtype.mk, Iff.intro