-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X : Scheme
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e_1 : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op V')) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV')) :
      (a : (↑(X.presheaf.obj (Opposite.op V')) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)) ≤ (CommRingCat.Hom.hom f).range
e : (↑(X.presheaf.obj (Opposite.op V')) : Type u) ≃+*
  ↥(RingHom.range
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))) :=
  RingEquiv.ofLeftInverse ⋯
a : (↑R : Type u)
⊢ Eq (α :=
    ↥(RingHom.range
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))
    ((e :
          (a : (↑(X.presheaf.obj (Opposite.op V')) : Type u)) →
            ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range)
        ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op) : (a : (↑R : Type u)) → (↑Γ(X, V') : Type u)) a) :
      ↥(RingHom.range
          (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))
    ((e :
          (a : (↑(X.presheaf.obj (Opposite.op V')) : Type u)) →
            ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range)
        ((CommRingCat.Hom.hom
              (φRA ≫
                CommRingCat.ofHom
                  (e.symm.toRingHom.comp
                    ((CommRingCat.Hom.hom φ).codRestrict
                      (RingHom.range
                        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                          (CC := CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV')))
                      ⋯))) :
            (a : (↑R : Type u)) → (↑Γ(X, V') : Type u))
          a) :
      ↥(RingHom.range
          (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))
have refine_2 : Eq (α :=
  ↥(RingHom.range
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))
  ((e : (a : (↑(X.presheaf.obj (Opposite.op V')) : Type u)) → ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range)
      ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map sorry.hom.op) : (a : (↑R : Type u)) → (↑Γ(X, V') : Type u)) a) :
    ↥(RingHom.range
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))
  ((e : (a : (↑(X.presheaf.obj (Opposite.op V')) : Type u)) → ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range)
      ((e.symm :
          (a : ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range) →
            (↑(X.presheaf.obj (Opposite.op V')) : Type u))
        ((((CommRingCat.Hom.hom φ).codRestrict
                  (RingHom.range
                    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV')))
                  sorry :
                (↑A : Type u) →+*
                  ↥(RingHom.range
                      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV')))) :
              (a : (↑A : Type u)) → ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range)
            ((φRA.hom' : (a : (↑R : Type u)) → (↑A : Type u)) a) :
          ↥(RingHom.range
              (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))) :
    ↥(RingHom.range
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))))
Tactic: change e _ = e (e.symm _)