-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : FormallyUnramified f
inst_1 : LocallyOfFiniteType f
x_1 : ↥X
algInst : Algebra (↑(Y.presheaf.stalk (f x_1)) : Type u) (↑(X.presheaf.stalk x_1) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x_1)).toAlgebra
this :
  IsLocalHom.{u, u, u} (R := (↑(Y.presheaf.stalk (f x_1)) : Type u)) (S := (↑(X.presheaf.stalk x_1) : Type u)) (F :=
    (↑(Y.presheaf.stalk (f x_1)) : Type u) →+* (↑(X.presheaf.stalk x_1) : Type u))
    (algebraMap (↑(Y.presheaf.stalk (f x_1)) : Type u) (↑(X.presheaf.stalk x_1) : Type u))
h :
  Algebra.IsSeparable.{u, u} (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
    (IsLocalRing.ResidueField (↑(X.presheaf.stalk x_1) : Type u))
e_1 : (↑(Y.residueField (f x_1)) : Type u) = IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u)
e_2 : (↑(X.residueField x_1) : Type u) = IsLocalRing.ResidueField (↑(X.presheaf.stalk x_1) : Type u)
e_3 :
  HEq.{u + 1} (α := CommRing (↑(Y.residueField (f x_1)) : Type u))
    (CommRingCat.instCommRingObjForgetRingHomCarrier :
      CommRing
        (Functor.obj
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Y.residueField (f x_1))))
    (β := CommRing (IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u)))
    (IsLocalRing.instCommRingResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
e_4 :
  HEq.{u + 1} (α := Ring (↑(X.residueField x_1) : Type u)) DivisionRing.toRing (β :=
    Ring (IsLocalRing.ResidueField (↑(X.presheaf.stalk x_1) : Type u))) DivisionRing.toRing
x : (↑(Y.residueField (f x_1)) : Type u)
⊢ Eq (α := (↑(X.residueField x_1) : Type u))
    ((algebraMap (↑(Y.residueField (f x_1)) : Type u) (↑(X.residueField x_1) : Type u) :
          (a : (↑(Y.residueField (f x_1)) : Type u)) → (↑(X.residueField x_1) : Type u))
        x :
      (↑(X.residueField x_1) : Type u))
    ((algebraMap (↑(Y.residueField (f x_1)) : Type u) (↑(X.residueField x_1) : Type u) :
          (a : (↑(Y.residueField (f x_1)) : Type u)) → (↑(X.residueField x_1) : Type u))
        x :
      (↑(X.residueField x_1) : Type u))
have h₁ : ∀ (x : (↑(Y.presheaf.stalk (f x_1)) : Type u)),
  Eq (α := (↑(X.residueField x_1) : Type u))
    ((algebraMap (↑(Y.residueField (f x_1)) : Type u) (↑(X.residueField x_1) : Type u) :
          (a : (↑(Y.residueField (f x_1)) : Type u)) → (↑(X.residueField x_1) : Type u))
        ((IsLocalRing.residue (↑(Y.presheaf.stalk (f x_1)) : Type u) :
            (a : (↑(Y.presheaf.stalk (f x_1)) : Type u)) →
              IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
          x) :
      (↑(X.residueField x_1) : Type u))
    ((algebraMap (↑(Y.residueField (f x_1)) : Type u) (↑(X.residueField x_1) : Type u) :
          (a : (↑(Y.residueField (f x_1)) : Type u)) → (↑(X.residueField x_1) : Type u))
        ((IsLocalRing.residue (↑(Y.presheaf.stalk (f x_1)) : Type u) :
            (a : (↑(Y.presheaf.stalk (f x_1)) : Type u)) →
              IsLocalRing.ResidueField (↑(Y.presheaf.stalk (f x_1)) : Type u))
          x) :
      (↑(X.residueField x_1) : Type u))
Tactic: obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x
Cleared hypotheses: x