-- Lean 4 proof step from Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
EM : Type u_1
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_2
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace HM M
EN : Type u_3
inst_6 : NormedAddCommGroup EN
inst_7 : NormedSpace 𝕜 EN
HN : Type u_4
inst_8 : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace HN N
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u)
hxU :
  Membership.mem (α := (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u)) U
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (locallyRingedSpaceMapAux f hf).base :
          (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
        x :
      (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)
⊢ Eq (α := (↑(CommRingCat.of 𝕜) : Type u))
    ((CommRingCat.Hom.hom
            ((locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
              (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
                smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x) :
          (a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)) → (↑(CommRingCat.of 𝕜) : Type u))
        a :
      (↑(CommRingCat.of 𝕜) : Type u))
    ((CommRingCat.Hom.hom
            ((locallyRingedSpace IN N).presheaf.germ U
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) (locallyRingedSpaceMapAux f hf).base :
                    (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                      (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                  x)
                hxU ≫
              smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)) :
          (a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)) → (↑(CommRingCat.of 𝕜) : Type u))
        a :
      (↑(CommRingCat.of 𝕜) : Type u))
have ih : (CommRingCat.Hom.hom
        ((locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
          (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
            smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x) :
      (a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)) → (↑(CommRingCat.of 𝕜) : Type u))
    a =
  (↑a :
      (x : ↥(Opposite.unop (Opposite.op U))) →
        (fun (x : (↑(TopCat.of N) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of N) : Type u)))
    (Subtype.mk (p := fun (x : (↑(TopCat.of N) : Type u)) ↦ x ∈ Opposite.unop (Opposite.op U)) (f x) hxU)
Tactic: refine Eq.trans ?_ (smoothSheafCommRing.evalHom_germ _ _ _ _ _ _ _ a).symm