-- Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
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
x : M
h :
  ∀
    (a b :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u)),
    a ∈
        (↑(RingHom.ker (F :=
              (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                      x) :
                  Type u) →+*
                𝕜)
              (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) :
          Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) →
      b ∈
          (↑(RingHom.ker (F :=
                (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                        x) :
                    Type u) →+*
                  𝕜)
                (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) :
            Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) →
        a + b ∈
          (↑(RingHom.ker (F :=
                (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                        x) :
                    Type u) →+*
                  𝕜)
                (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) :
            Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u))
⊢ ∀
    (a b :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u)),
    Membership.mem (γ :=
        Set
          (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u))
        (nonunits
          (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u))
        a →
      Membership.mem (γ :=
          Set
            (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                  x) :
              Type u))
          (nonunits
            (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                  x) :
              Type u))
          b →
        Membership.mem (γ :=
          Set
            (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                  x) :
              Type u))
          (nonunits
            (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜))
                  x) :
              Type u))
          (a + b)

Tactic:
rw [smoothSheafCommRing.nonunits_stalk]

Premises used: smoothSheafCommRing.nonunits_stalk