-- 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:
𝕜 : 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
V : Opens M := { carrier := Subtype.val '' V₀, is_open' := ⋯ }
hUV : V ≤ U
⊢ V₀ = Set.range (Set.inclusion hUV)

Tactic:
convert (Set.range_inclusion hUV).symm

Result:
case h.e'_2.h
𝕜 : 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₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
V : Opens M := { carrier := Subtype.val '' V₀, is_open' := ⋯ }
hUV : V ≤ U
e_1✝ : Set ↥U = Set ↑↑U
⊢ V₀ = {x | ↑x ∈ ↑V}

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.refine_2.refine_2
𝕜 : 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⟩
⊢ (CategoryTheory.ConcreteCategory.hom (S.germ V x hxV)) (g * (ContMDiffMap.restrictRingHom IM 𝓘(𝕜, 𝕜) 𝕜 hUV) f) = 1

Tactic:
convert RingHom.map_one _

Result:
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

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
H : ∃ t, (∀ y ∈ t, f y ≠ 0) ∧ IsOpen t ∧ ⟨x, hxU⟩ ∈ t
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Tactic:
obtain ⟨V₀, hV₀f, hV₀, hxV₀⟩ := H

Result:
case mpr.intro.intro.intro.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
V₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

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
H : ∀ᶠ (z : ↥U) in 𝓝 ⟨x, hxU⟩, f z ≠ 0
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Tactic:
rw [eventually_nhds_iff] at H

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 : ∃ t, (∀ y ∈ t, f y ≠ 0) ∧ IsOpen t ∧ ⟨x, hxU⟩ ∈ t
⊢ IsUnit ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f)

Proof state:
case mp
𝕜 : 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
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ IsUnit f → f ∉ RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)

Tactic:
rintro ⟨⟨f, g, hf, hg⟩, rfl⟩ (h' : smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x f = 0)

Result:
case mp.intro.mk
𝕜 : 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
f g : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
hf : f * g = 1
hg : g * f = 1
h' : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) f = 0
⊢ False