-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
have obtain : ∀
  (l :
    Spec
        (CommRingCat.of
          { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := sorry, valuationRing := sorry,
              K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
              algebra := A.instAlgebraSubtypeMem, isFractionRing := sorry, i₁ := X.fromSpecResidueField x',
              i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := sorry : ValuativeCommSq f }.R) ⟶
      X)
  (hl₁ :
    Spec.map
          (CommRingCat.ofHom
            (algebraMap
              { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := sorry, valuationRing := sorry,
                  K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
                  algebra := A.instAlgebraSubtypeMem, isFractionRing := sorry, i₁ := X.fromSpecResidueField x',
                  i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := sorry : ValuativeCommSq f }.R
              { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := sorry, valuationRing := sorry,
                  K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
                  algebra := A.instAlgebraSubtypeMem, isFractionRing := sorry, i₁ := X.fromSpecResidueField x',
                  i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := sorry : ValuativeCommSq f }.K)) ≫
        l =
      { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := sorry, valuationRing := sorry,
          K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
          algebra := A.instAlgebraSubtypeMem, isFractionRing := sorry, i₁ := X.fromSpecResidueField x',
          i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := sorry : ValuativeCommSq f }.i₁)
  (hl₂ :
    l ≫ f =
      { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := sorry, valuationRing := sorry,
          K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
          algebra := A.instAlgebraSubtypeMem, isFractionRing := sorry, i₁ := X.fromSpecResidueField x',
          i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := sorry }.i₂),
  ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
Tactic: obtain ⟨l, hl₁, hl₂⟩ := (H { R := A, K := X.residueField x', commSq := ⟨w⟩, .. }).exists_lift