-- 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
EP : Type u_5
inst_11 : NormedAddCommGroup EP
inst_12 : NormedSpace 𝕜 EP
HP : Type u_6
inst_13 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_14 : TopologicalSpace P
inst_15 : ChartedSpace HP P
f : M → N
hf : ContMDiff IM IN ∞ f
x : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)
a :
  (↑((locallyRingedSpace IN N).presheaf.stalk
        ((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)) :
    Type u)
ha :
  ¬Eq (α := 𝕜)
      ((smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x :
            (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
          ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x) :
                (a :
                    (↑((locallyRingedSpace IN N).presheaf.stalk
                          ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base :
                              (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                                (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                            x)) :
                      Type u)) →
                  (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u))
              a :
            (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u)) :
        𝕜)
      (0 : 𝕜)
⊢ ¬Eq (α := 𝕜)
      ((smoothSheafCommRing.eval IN 𝓘(𝕜, 𝕜) N 𝕜
              ((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) :
            (a :
                (↑((smoothSheafCommRing IN 𝓘(𝕜, 𝕜) N 𝕜).presheaf.stalk
                      ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base :
                          (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                        x)) :
                  Type u)) →
              𝕜)
          a :
        𝕜)
      (0 : 𝕜)
have h : Eq (α := 𝕜)
  ((smoothSheafCommRing.eval IN 𝓘(𝕜, 𝕜) N 𝕜
          ((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) :
        (a :
            (↑((smoothSheafCommRing IN 𝓘(𝕜, 𝕜) N 𝕜).presheaf.stalk
                  ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base :
                      (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                        (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                    x)) :
              Type u)) →
          𝕜)
      a :
    𝕜)
  ((smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x :
        (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
      ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x) :
            (a :
                (↑((locallyRingedSpace IN N).presheaf.stalk
                      ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base :
                          (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                            (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                        x)) :
                  Type u)) →
              (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u))
          a :
        (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u)) :
    𝕜)
Tactic: convert! ha