-- Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean
theorem smoothSheafCommRing.isUnit_stalk_iff {x : M}
    (f : (smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf.stalk x) :
    IsUnit f ↔ f ∉ RingHom.ker (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x)

Proof state:
case h.e'_2.h.e'_6
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.intro.intro.intro.intro.intro.intro.refine_1⟩
⊢ g * (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f = 1

Tactic:
apply Subtype.ext

Result:
case h.e'_2.h.e'_6.a
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V : Opens M
hUV : V ≤ U
hV₀f : ∀ y ∈ Set.range (Set.inclusion hUV), f y ≠ 0
hV₀ : IsOpen (Set.range (Set.inclusion hUV))
hxV₀ : ⟨x, hxU⟩ ∈ Set.range (Set.inclusion hUV)
hxV : x ∈ ↑V
hVf : ∀ (y : ↥V), f (Set.inclusion hUV y) ≠ 0
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ := ⟨(⇑f ∘ Set.inclusion hUV)⁻¹, ?mpr.intro.intro.intro.intro.intro.intro.refine_1⟩
⊢ ↑(g * (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f) = ↑1

Proof state:
case mpr.intro.intro.intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Tactic:
have H :  ∀ᶠ (z : U) in 𝓝 ⟨x, hxU⟩, f z ≠ 0 := f.2.continuous.continuousAt.eventually_ne hf'

Result:
case mpr.intro.intro.intro
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
H : ∀ᶠ (z : ↥U) in 𝓝 ⟨x, hxU⟩, f z ≠ 0
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)