-- 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.{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))
have a : ∃ (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)) 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))
    (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)) 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)) ⟶
      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)) 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) :
      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)) 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)) ⟶
        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)) 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)) ⟶
        CommRingCat.of K)
Tactic: rw [Scheme.SpecToEquivOfField_eq_iff]