-- 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) ((↑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))
⊢ ∃ (e :
    Eq.{u + 1} (α := ↥X)
      (Sigma.fst (β := fun (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))
      (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((Scheme.SpecToEquivOfField K X :
            (a : Spec (CommRingCat.of K) ⟶ X) → (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
          (↑p : Spec (CommRingCat.of K) ⟶ X)))),
    Eq.{u + 1} (α :=
      X.residueField
          (Sigma.fst (β := fun (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)) ⟶
        CommRingCat.of K)
      (Sigma.snd (β := fun (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) :
        X.residueField
            (Sigma.fst (β := fun (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)) ⟶
          CommRingCat.of K)
      ((Scheme.residueFieldCongr e).hom ≫
          Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            ((Scheme.SpecToEquivOfField K X :
                (a : Spec (CommRingCat.of K) ⟶ X) → (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
              (↑p : Spec (CommRingCat.of K) ⟶ X)) :
        X.residueField
            (Sigma.fst (β := fun (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)) ⟶
          CommRingCat.of K)

Tactic:
dsimp [Scheme.SpecToEquivOfField]

Premises used: AlgebraicGeometry.Scheme.SpecToEquivOfField