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 : IsClosedImmersion (X.fromSpecResidueField x)
rw : LocallyOfFiniteType (X.fromSpecResidueField x ≫ f)
⊢ IsFinite (X.fromSpecResidueField x ≫ f)

Tactic:
rw [isFinite_iff_locallyOfFiniteType_of_jacobsonSpace]

Premises used: AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace
-- 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 : IsClosedImmersion (X.fromSpecResidueField x)
⊢ LocallyOfFiniteType (X.fromSpecResidueField x ≫ f)

Tactic:
infer_instance
-- 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}
⊢ IsFinite (X.fromSpecResidueField x ≫ f)

Tactic:
have : IsFinite (X.fromSpecResidueField x ≫ f) := by
      rw [isClosed_singleton_iff_isClosedImmersion] at hx
      rw [isFinite_iff_locallyOfFiniteType_of_jacobsonSpace]
      infer_instance
-- 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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
rw :
  Function.Bijective (α := (↑(CommRingCat.of K) : Type u)) (β := (↑(X.residueField x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))) :
      (a : (↑(CommRingCat.of K) : Type u)) → (↑(X.residueField x) : Type u))
⊢ IsIso (Spec.preimage (X.fromSpecResidueField x ≫ f))

Tactic:
rw [ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- 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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ Function.Bijective (α := (↑(CommRingCat.of K) : Type u)) (β := (↑(X.residueField x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))) :
      (a : (↑(CommRingCat.of K) : Type u)) → (↑(X.residueField x) : Type u))

Tactic:
IsAlgClosed.ringHom_bijective_of_isIntegral _ ?_

Premises used: IsAlgClosed.ringHom_bijective_of_isIntegral
-- 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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
refine :
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))).IsIntegral
⊢ Function.Bijective (α := (↑(CommRingCat.of K) : Type u)) (β := (↑(X.residueField x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))) :
      (a : (↑(CommRingCat.of K) : Type u)) → (↑(X.residueField x) : Type u))

Tactic:
refine IsAlgClosed.ringHom_bijective_of_isIntegral _ ?_

Premises used: IsAlgClosed.ringHom_bijective_of_isIntegral
-- 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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
rw : IsIntegralHom (X.fromSpecResidueField x ≫ f)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) (Spec.preimage (X.fromSpecResidueField x ≫ f))).IsIntegral

Tactic:
rw [← IsIntegralHom.SpecMap_iff, Spec.map_preimage]

Premises used: AlgebraicGeometry.IsIntegralHom.SpecMap_iff, AlgebraicGeometry.Spec.map_preimage
-- 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}
this : IsFinite (X.fromSpecResidueField x ≫ f)
⊢ IsIntegralHom (X.fromSpecResidueField x ≫ f)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X : 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}
⊢ Spec.map (residueFieldIsoBase f x hx).inv = X.fromSpecResidueField x ≫ f

Tactic:
Spec.map_preimage _

Premises used: Quiver.Hom.unop, AlgebraicGeometry.Spec.map_preimage, AlgebraicGeometry.Spec.preimage
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X : 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}
⊢ pointOfClosedPoint f x hx ≫ f = 𝟙 (Spec (CommRingCat.of K))

Tactic:
simp [pointOfClosedPoint, ← SpecMap_residueFieldIsoBase_inv, ← Spec.map_comp]

Premises used: AlgebraicGeometry.pointOfClosedPoint, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv
-- Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic
Goal:
X : 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}
a : ↥(Spec (CommRingCat.of K))
⊢ (pointOfClosedPoint f x hx) a = x

Tactic:
simp [pointOfClosedPoint]

Premises used: AlgebraicGeometry.pointOfClosedPoint
-- 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)) }
⊢ IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)

Tactic:
have := isClosedImmersion_of_comp_eq_id _ _ p.2
-- 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)) }
this : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
⊢ IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑(↑p : Spec (CommRingCat.of K) ⟶ X))

Tactic:
have := p.1.isClosedEmbedding.isClosed_range
-- 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)) }
this_1 : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
this : IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑(↑p : Spec (CommRingCat.of K) ⟶ X))
rwa :
  ∀ (x : ↥(Spec (CommRingCat.of K))),
    Eq (α := ↥X) ((↑p : Spec (CommRingCat.of K) ⟶ X) x : ↥X)
      ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (closedPoints ↥X)
    ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)

Tactic:
rwa [Set.range_eq_singleton] at this

Premises used: Set.range_eq_singleton
-- 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)) }
this_1 : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
this : IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑(↑p : Spec (CommRingCat.of K) ⟶ X))
⊢ ∀ (x : ↥(Spec (CommRingCat.of K))),
    Eq (α := ↥X) ((↑p : Spec (CommRingCat.of K) ⟶ X) x : ↥X)
      ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)

Tactic:
fun x ↦ congr(p.1 $(Subsingleton.elim _ _))

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', IsLocalRing.closedPoint, AlgebraicGeometry.PresheafedSpace.Hom.base, Subsingleton.elim, Subtype.val, DFunLike.coe
-- 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)) }
this_1 : IsClosedImmersion (↑p : Spec (CommRingCat.of K) ⟶ X)
this : IsClosed (X := ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑(↑p : Spec (CommRingCat.of K) ⟶ X))
⊢ ∀ (x : ↥(Spec (CommRingCat.of K))),
    Eq (α := ↥X) ((↑p : Spec (CommRingCat.of K) ⟶ X) x : ↥X)
      ((↑p : Spec (CommRingCat.of K) ⟶ X) (IsLocalRing.closedPoint K) : ↥X)

Tactic:
exact fun x ↦ congr(p.1 $(Subsingleton.elim _ _))

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Subsingleton.elim, Subtype.val, DFunLike.coe
-- 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)) }
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) ⋯) ⋯ :
              { 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)
⊢ (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

Tactic:
ext
-- 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)) }
⊢ (↑((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)

Tactic:
((Scheme.SpecToEquivOfField _ _).symm_apply_eq (x := ⟨_, _⟩)).mpr ?_

Premises used: Iff.mpr, Equiv.symm_apply_eq, AlgebraicGeometry.Scheme.SpecToEquivOfField, AlgebraicGeometry.pointOfClosedPoint
-- 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)) }
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)) ⋯ :
                { 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)) ⋯ :
                    { x : ↥X // Membership.mem (γ := Set ↥X) (closedPoints ↥X) x }))
                p) :
            ↥X)
          ⋯).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))
⊢ (↑((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)

Tactic:
refine ((Scheme.SpecToEquivOfField _ _).symm_apply_eq (x := ⟨_, _⟩)).mpr ?_

Premises used: Iff.mpr, Equiv.symm_apply_eq, AlgebraicGeometry.Scheme.SpecToEquivOfField
-- 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)) }
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)) ⋯).1
    (Scheme.descResidueField (Scheme.stalkClosedPointTo (↑p : Spec (CommRingCat.of K) ⟶ X)))
⊢ ∃ (_ :
    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))

Tactic:
simp only [Category.id_comp, exists_const]

Premises used: exists_const, CategoryTheory.Category.id_comp
-- 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)) }
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)))
⊢ 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)))

Tactic:
generalize_proofs _ h
-- 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)))
⊢ 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:
(Category.comp_id _).symm.trans (((residueFieldIsoBase f _ h).eq_inv_comp).mp ?_)

Premises used: AlgebraicGeometry.residueFieldIsoBase, CategoryTheory.Category.comp_id, Iff.mp, CategoryTheory.Iso.eq_inv_comp, Eq.symm, Eq.trans
-- 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 :
  𝟙 (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))
⊢ 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:
refine (Category.comp_id _).symm.trans (((residueFieldIsoBase f _ h).eq_inv_comp).mp ?_)

Premises used: AlgebraicGeometry.residueFieldIsoBase, CategoryTheory.Category.comp_id, Iff.mp, CategoryTheory.Iso.eq_inv_comp, Eq.symm, Eq.trans
-- 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.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)))
⊢ 𝟙 (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:
rw [← Spec.map_injective.eq_iff]

Premises used: AlgebraicGeometry.Spec.map_injective, Function.Injective.eq_iff
-- 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)) =
    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)
⊢ 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:
simp only [Spec.map_id, Spec.map_comp, SpecMap_residueFieldIsoBase_inv]

Premises used: AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv