awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
⊢ U ≤ V

Tactic:
have hUV : U ≤ V := CategoryTheory.leOfHom i
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
change : ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x
⊢ ChartedSpace.LiftPropAt (M' := M') P (fun (x : ↥U) ↦ f ((i : (a : ↥U) → ↥V) x)) x

Tactic:
change ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x

Premises used: TopologicalSpace.Opens.inclusion, Function.comp, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
rw :
  ChartedSpace.LiftPropAt P f
    (inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV x)
⊢ ChartedSpace.LiftPropAt P (f ∘ Opens.inclusion hUV) x

Tactic:
rw [← hG.liftPropAt_iff_comp_inclusion hUV]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U V : Opens (↑(TopCat.of M) : Type u)
i : U ⟶ V
f : (x : ↥V) → M'
h : ChartedSpace.LiftProp P f
x : ↥U
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f
    (inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV x)

Tactic:
apply h
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
obtain :
  ∀ (U : Opens (↑(TopCat.of M) : Type u)) (hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U) (i : U ⟶ V)
    (hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))), ChartedSpace.LiftPropAt P f x
⊢ ChartedSpace.LiftPropAt P f x

Tactic:
obtain ⟨U, hxU, i, hU : ChartedSpace.LiftProp P (f ∘ _)⟩ := h x

Premises used: ChartedSpace.LiftProp, Function.comp
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
⊢ U ≤ V

Tactic:
have hUV : U ≤ V := CategoryTheory.leOfHom i
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
rw :
  ChartedSpace.LiftPropAt P
    (f ∘ inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV) x'
⊢ ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')

Tactic:
rw [hG.liftPropAt_iff_comp_inclusion hUV]

Premises used: StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P
    (f ∘ inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV) x'

Tactic:
hU x'

Premises used: Set.Mem
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P
    (f ∘ inclusion (s := (↑U : Set (↑(TopCat.of M) : Type u))) (t := (↑V : Set (↑(TopCat.of M) : Type u))) hUV) x'

Tactic:
exact hU x'
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')

Tactic:
have : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x') := by
      rw [hG.liftPropAt_iff_comp_inclusion hUV]
      exact hU x'
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
this : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')
⊢ ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')

Tactic:
this
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
V : Opens (↑(TopCat.of M) : Type u)
f : (x : ↥V) → M'
h :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑(TopCat.of M) : Type u)) (_ : (↑x : (↑(TopCat.of M) : Type u)) ∈ V_1) (i : V_1 ⟶ V),
      ChartedSpace.LiftProp (M' := M') P fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥V) x)
x : ↥V
U : Opens (↑(TopCat.of M) : Type u)
hxU : (↑x : (↑(TopCat.of M) : Type u)) ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp (M := ↥U) P (f ∘ (⇑i : (a : ↥U) → ↥V))
x' : ↥U := Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ U) (↑x : (↑(TopCat.of M) : Type u)) hxU
hUV : U ≤ V
this : ChartedSpace.LiftPropAt P f (Opens.inclusion hUV x')
⊢ ChartedSpace.LiftPropAt P f x

Tactic:
convert! this
-- Module: Mathlib.Geometry.Manifold.Sheaf.Basic
Goal:
H : Type u_1
inst : TopologicalSpace H
H' : Type u_2
inst_1 : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst_2 : TopologicalSpace M
inst_3 : ChartedSpace H M
M' : Type u
inst_4 : TopologicalSpace M'
inst_5 : ChartedSpace H' M'
hG : G.LocalInvariantProp G' P
U : (Opens (↑(TopCat.of M) : Type u))ᵒᵖ
f :
  CategoryTheory.Functor.obj
    (CategoryTheory.ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))) (sheaf (P := P) M M' hG))
    U
⊢ ChartedSpace.LiftProp P
    (↑f : (x : ↥(unop U)) → (fun (x : (↑(TopCat.of M) : Type u)) ↦ M') (↑x : (↑(TopCat.of M) : Type u)))

Tactic:
f.2

Premises used: ChartedSpace.LiftProp, Set.Mem, Subtype.property
-- 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
x : M
f :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
mp :
  IsUnit f →
    f ∉
      RingHom.ker (F :=
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u) →+*
          𝕜)
        (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)
mpr :
  f ∉
      RingHom.ker (F :=
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u) →+*
          𝕜)
        (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) →
    IsUnit f
⊢ IsUnit f ↔
    f ∉
      RingHom.ker (F :=
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
            Type u) →+*
          𝕜)
        (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)

Tactic:
constructor
-- 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
x : M
f g :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
hf : f * g = 1
hg : g * f = 1
h' :
  Eq (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜) f : 𝕜)
    (0 : 𝕜)
⊢ False

Tactic:
simpa [h'] using congr_arg (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x) hf

Premises used: congr_arg, modelWithCornersSelf, smoothSheafCommRing.eval, DFunLike.coe
-- 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
x : M
f :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜) f : 𝕜)
    (0 : 𝕜)
mpr :
  ∀ (U : Opens M) (hxU : x ∈ U) (f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯)
    (hf :
      Ne (α := 𝕜)
        ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
            ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                    (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
                  (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
                f :
              (↑(S.stalk x) : Type u)) :
          𝕜)
        (0 : 𝕜)),
    IsUnit (M :=
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u))
      ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
            (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
          f :
        (↑(S.stalk x) : Type u))
⊢ IsUnit f

Tactic:
obtain ⟨U : Opens M, hxU, f : C^∞⟮IM, U; 𝓘(𝕜), 𝕜⟯, rfl⟩ := S.exists_germ_eq f

Premises used: TopologicalSpace.Opens, TopCat.Presheaf.exists_germ_eq, rfl
-- 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
⊢ Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)

Tactic:
hf
-- 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
h :
  Eq (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
⊢ Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)

Tactic:
convert! hf
-- 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
⊢ Eq (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)

Tactic:
(smoothSheafCommRing.eval_germ U x hxU f).symm

Premises used: smoothSheafCommRing.eval_germ, Set.Mem, Eq.symm
-- 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
⊢ Eq (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)

Tactic:
exact (smoothSheafCommRing.eval_germ U x hxU f).symm

Premises used: smoothSheafCommRing.eval_germ, Eq.symm
-- 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
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf :
  Ne (α := 𝕜)
    ((eval IM 𝓘(𝕜, 𝕜) M 𝕜 x : (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
        ((CategoryTheory.ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                (CC := CommRingCat.carrier) (Y := S.stalk x) (S.germ U x hxU) :
              (a : (↑(S.obj (Opposite.op U)) : Type u)) → (↑(S.stalk x) : Type u))
            f :
          (↑(S.stalk x) : Type u)) :
      𝕜)
    (0 : 𝕜)
⊢ Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)

Tactic:
have hf' : f ⟨x, hxU⟩ ≠ 0 := by
      convert! hf
      exact (smoothSheafCommRing.eval_germ U x hxU f).symm