awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)) }
⊢ (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)) }))
      ((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 }))
        p) =
    p
have a : (↑((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) sorry) sorry :
            { p : Spec (CommRingCat.of K) ⟶ X // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }))
        ((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)) sorry :
              { x : ↥X // Membership.mem (γ := Set ↥X) (closedPoints ↥X) x }))
          p)) :
    Spec (CommRingCat.of K) ⟶ X) =
  (↑p : Spec (CommRingCat.of K) ⟶ X)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)) }
⊢ (↑((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)) }))
          ((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 }))
            p)) :
      Spec (CommRingCat.of K) ⟶ X) =
    (↑p : Spec (CommRingCat.of K) ⟶ X)
have a : Eq.{u + 1} (α := (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
  (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
    (↑((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)) sorry :
              { x : ↥X // Membership.mem (γ := Set ↥X) (closedPoints ↥X) x }))
          p) :
      ↥X)
    (residueFieldIsoBase f
        (↑((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)) sorry :
                  { x : ↥X // Membership.mem (γ := Set ↥X) (closedPoints ↥X) x }))
              p) :
          ↥X)
        sorry).1)
  ((Scheme.SpecToEquivOfField K X :
      (a : Spec (CommRingCat.of K) ⟶ X) → (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
    (↑p : Spec (CommRingCat.of K) ⟶ X))
Tactic: refine ((Scheme.SpecToEquivOfField _ _).symm_apply_eq (x := ⟨_, _⟩)).mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)) }
⊢ ∃ (_ :
    Eq (α := ↥X) ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)
      ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)),
    (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⋯).1 =
      𝟙 (X.residueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K))) ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X))
have a : Eq (α := X.residueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⟶ CommRingCat.of K)
  (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) sorry).1
  (Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
Tactic: simp only [Category.id_comp, exists_const]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)) }
⊢ Eq (α := X.residueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⟶ CommRingCat.of K)
    (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⋯).1
    (Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
have a : ∀ (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)))),
  Eq (α := X.residueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⟶ CommRingCat.of K)
    (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) h).1
    (Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
Tactic: generalize_proofs _ h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)))
⊢ Eq (α := X.residueField ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) ⟶ CommRingCat.of K)
    (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) h).1
    (Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
have a : 𝟙 (CommRingCat.of K) =
  (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) h).inv ≫
    Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X))
Tactic: refine (Category.comp_id _).symm.trans (((residueFieldIsoBase f _ h).eq_inv_comp).mp ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)))
⊢ 𝟙 (CommRingCat.of K) =
    (residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) h).inv ≫
      Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X))
have a : Spec.map (𝟙 (CommRingCat.of K)) =
  Spec.map
    ((residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) h).inv ≫
      Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
Tactic: rw [← Spec.map_injective.eq_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)))
⊢ Spec.map (𝟙 (CommRingCat.of K)) =
    Spec.map
      ((residueFieldIsoBase f ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K)) h).inv ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
have a : 𝟙 (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: simp only [Spec.map_id, Spec.map_comp, SpecMap_residueFieldIsoBase_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)))
⊢ 𝟙 (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)
have a : 𝟙 (Spec (CommRingCat.of K)) = (↑p : Spec (CommRingCat.of K) ⟶ X) ≫ f
Tactic: rw [reassoc_of% Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, p.2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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
⊢ 𝟙 (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)
have a₁ : 𝟙 (Spec (CommRingCat.of K)) = 𝟙 (Spec (CommRingCat.of K))
Tactic: rw [reassoc_of% Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, p.2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (hypothesis)
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
⊢ f = g
have this : JacobsonSpace.{u} ↥X
Tactic: have : JacobsonSpace ↥X := LocallyOfFiniteType.jacobsonSpace (f ≫ i)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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
have refine_1 : Dense (S ∩ closedPoints ↥X)
Tactic: refine ext_of_fromSpecResidueField_eq f g i (S ∩ closedPoints X) ?_ ?_ H'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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)
⊢ f = g
have refine_2 : ∀ x ∈ S ∩ closedPoints ↥X, X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
Tactic: refine ext_of_fromSpecResidueField_eq f g i (S ∩ closedPoints X) ?_ ?_ H'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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
⊢ Dense (S ∩ closedPoints ↥X)
have refine_1 : closure (S ∩ closedPoints ↥X) = Set.univ
Tactic: rwa [dense_iff_closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      ← dense_iff_closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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
⊢ Dense (S ∩ closedPoints ↥X)
have refine_1₁ : closure S = Set.univ
Tactic: rwa [dense_iff_closure_eq, JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      ← dense_iff_closure_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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
⊢ x ∈ S ∩ closedPoints ↥X → X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
have refine_2 : ∀ (hxS : x ∈ S) (hx : Membership.mem (γ := Set ↥X) (closedPoints ↥X) x),
  X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
Tactic: ⟨hxS, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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
⊢ X.fromSpecResidueField x ≫ f = X.fromSpecResidueField x ≫ g
have 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
Tactic: rw [← cancel_epi (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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 =
    Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g
have refine_2 : (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f) ≫ i = 𝟙 (Spec (CommRingCat.of K))
Tactic: refine ext_of_apply_closedPoint_eq i ?_ ?_ (by simpa using H x hxS hx)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AlgClosed.Basic (goal)
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))
⊢ Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ f =
    Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g
have refine_2₁ : (Spec.map (residueFieldIsoBase (f ≫ i) x hx).hom ≫ X.fromSpecResidueField x ≫ g) ≫ i = 𝟙 (Spec (CommRingCat.of K))
Tactic: refine ext_of_apply_closedPoint_eq i ?_ ?_ (by simpa using H x hxS hx)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
Goal:
X : Scheme
inst : IsLocallyNoetherian X
h : topologicalKrullDim.{u} ↥X ≤ 0
U : (↑X.affineOpens : Type u)
⊢ IsArtinianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
have x : IsNoetherianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
Tactic: have _ : IsNoetherianRing Γ(X, U) := IsLocallyNoetherian.component_noetherian U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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)
⊢ IsArtinianRing.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)
have rw : topologicalKrullDim.{u} (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) ≤ 0
Tactic: rw [isArtinianRing_iff_krullDimLE_zero, Ring.KrullDimLE, Order.krullDimLE_iff, ← ringKrullDim,
      Nat.cast_zero, ← PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim Γ(X, U)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
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} ↥(Spec Γ(X, (↑U : X.Opens))) ≤ 0
have rw : topologicalKrullDim.{u} ↥(↑(↑U : X.Opens) : Scheme) ≤ 0
Tactic: rw [← IsHomeomorph.topologicalKrullDim_eq _ U.2.isoSpec.hom.homeomorph.isHomeomorph]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
⊢ DiscreteTopology.{u} ↥X
have apply : ∀ (a : ↥X), IsOpen (X := ↥X) {a}
Tactic: apply discreteTopology_iff_isOpen_singleton.mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyArtinian X
x : ↥X
⊢ IsOpen (X := ↥X) {x}
have obtain : ∀ (W : X.Opens) (hW1 : IsAffineOpen W) (hW2 : x ∈ W), W.carrier ⊆ (↑⊤ : Set ↥X) → IsOpen (X := ↥X) {x}
Tactic: obtain ⟨W, hW1, hW2, _⟩ := exists_isAffineOpen_mem_and_subset (TopologicalSpace.Opens.mem_top x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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)
⊢ IsOpen (X := ↥X) {x}
have this : IsArtinianRing.{u} (↑Γ(X, W) : Type u)
Tactic: have : IsArtinianRing Γ(X, W) := IsLocallyArtinian.isArtinianRing_presheaf_obj ⟨_, hW1⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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)
⊢ IsOpen (X := ↥X) {x}
have this₁ : DiscreteTopology.{u} ↥(Spec Γ(X, W))
Tactic: have : DiscreteTopology (Spec Γ(X, W)) := inferInstanceAs (DiscreteTopology (PrimeSpectrum _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Artinian (hypothesis)
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))
⊢ IsOpen (X := ↥X) {x}
have this₁ : DiscreteTopology.{u} ↥(↑W : Scheme)
Tactic: have : DiscreteTopology W := hW1.isoSpec.hom.homeomorph.symm.discreteTopology