awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
y : ↥(Opposite.unop (Opposite.op V))
⊢ Ne (α := (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑y : (↑(TopCat.of M) : Type u)))
    (((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV) y) 0

Tactic:
hVf y
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
g : C^∞⟮IM, ↥V; 𝓘(𝕜, 𝕜), 𝕜⟯ :=
  Subtype.mk (p := fun (f : ↥V → 𝕜) ↦ ContMDiff IM 𝓘(𝕜, 𝕜) ∞ f)
    ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹ ⋯
y : ↥(Opposite.unop (Opposite.op V))
⊢ Ne (α := (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑y : (↑(TopCat.of M) : Type u)))
    (((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV) y) 0

Tactic:
exact hVf y
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
y : ↥V
⊢ ContMDiffAt IM 𝓘(𝕜, 𝕜) (M' := 𝕜) ∞ ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹
    y

Tactic:
(((contDiffAt_inv _ (hVf y)).contMDiffAt).comp y
        (f.contMDiff.comp (contMDiff_inclusion hUV)).contMDiffAt :)

Premises used: ContMDiff.comp, contMDiff_inclusion, ContMDiffMap.contMDiff, ContMDiff.contMDiffAt, ContMDiffAt.comp
-- 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 : 𝕜)
hf' : Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU) : 𝕜) (0 : 𝕜)
V : Opens M
hUV : V ≤ U
hV₀f :
  ∀ y ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV),
    Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) y : 𝕜) (0 : 𝕜)
hV₀ : IsOpen[instTopologicalSpaceSubtype] (Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV))
hxV₀ :
  Subtype.mk (p := fun (x : M) ↦ x ∈ U) x hxU ∈ Set.range (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)
hxV : x ∈ (↑V : Set M)
hVf :
  ∀ (y : ↥V), Ne (α := 𝕜) ((f : (a : ↥U) → 𝕜) (Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV y) : 𝕜) (0 : 𝕜)
y : ↥V
⊢ ContMDiffAt IM 𝓘(𝕜, 𝕜) (M' := 𝕜) ∞ ((⇑f : (a : ↥U) → 𝕜) ∘ Set.inclusion (s := (↑V : Set M)) (t := (↑U : Set M)) hUV)⁻¹
    y

Tactic:
exact (((contDiffAt_inv _ (hVf y)).contMDiffAt).comp y
        (f.contMDiff.comp (contMDiff_inclusion hUV)).contMDiffAt :)

Premises used: ContMDiff.comp, contMDiff_inclusion, ContMDiffMap.contMDiff, ContMDiff.contMDiffAt, ContMDiffAt.comp
-- 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
h :
  ∀
    (f :
      (↑(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))
        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)) :
          Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u))
⊢ nonunits
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
        Type u) =
    (↑(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))

Tactic:
ext1 f
-- 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)
h :
  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)) :
        Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk 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))
      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)) :
        Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u))

Tactic:
rw [mem_nonunits_iff, not_iff_comm, Iff.comm]

Premises used: mem_nonunits_iff, Iff.comm, not_iff_comm
-- 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)
⊢ 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)) :
        Set (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u))

Tactic:
apply smoothSheafCommRing.isUnit_stalk_iff

Premises used: smoothSheafCommRing.isUnit_stalk_iff
-- 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)),
    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)
⊢ IsLocalRing.{u}
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) :
      Type u)

Tactic:
apply IsLocalRing.of_nonunits_add

Premises used: IsLocalRing.of_nonunits_add
-- 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
f g :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
⊢ f ∈
      (↑(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)) →
    g ∈
        (↑(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)) →
      f + g ∈
        (↑(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))

Tactic:
Ideal.add_mem _

Premises used: Ideal.add_mem
-- 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
f g :
  (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜)) x) : Type u)
⊢ f ∈
      (↑(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)) →
    g ∈
        (↑(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)) →
      f + g ∈
        (↑(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))

Tactic:
exact Ideal.add_mem _

Premises used: Ideal.add_mem
-- 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
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
ih :
  ∀ (U : Opens (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
    (hxU :
      Membership.mem (α := (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u)) U
        ((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 :
          (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))),
    (locallyRingedSpace IN N).presheaf.germ U
          ((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)
          hxU ≫
        PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x ≫ smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
      (locallyRingedSpace IN N).presheaf.germ U
          ((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)
          hxU ≫
        smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)
⊢ PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x ≫ smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)

Tactic:
apply TopCat.Presheaf.stalk_hom_ext

Premises used: TopCat.Presheaf.stalk_hom_ext
-- 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
f : M → N
hf : ContMDiff IM IN ∞ f
x : M
U : Opens (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u)
hxU :
  Membership.mem (α := (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u)) U
    ((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 :
      (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
ih :
  (locallyRingedSpaceMapAux f hf).c.app (Opposite.op U) ≫
      (locallyRingedSpace IM M).presheaf.germ ((Opens.map (locallyRingedSpaceMapAux f hf).base).obj U) x hxU ≫
        smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    (locallyRingedSpace IN N).presheaf.germ U
        ((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)
        hxU ≫
      smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)
⊢ (locallyRingedSpace IN N).presheaf.germ U
        ((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)
        hxU ≫
      PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x ≫ smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    (locallyRingedSpace IN N).presheaf.germ U
        ((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)
        hxU ≫
      smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)

Tactic:
rw [PresheafedSpace.stalkMap_germ_assoc]

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc