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
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))
a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)
⊢ Eq (α := (↑(CommRingCat.of 𝕜) : Type u))
    ((CommRingCat.Hom.hom
            ((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) :
          (a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)) → (↑(CommRingCat.of 𝕜) : Type u))
        a :
      (↑(CommRingCat.of 𝕜) : Type u))
    ((CommRingCat.Hom.hom
            ((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)) :
          (a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)) → (↑(CommRingCat.of 𝕜) : Type u))
        a :
      (↑(CommRingCat.of 𝕜) : Type u))

Tactic:
Eq.trans ?_ (smoothSheafCommRing.evalHom_germ _ _ _ _ _ _ _ a).symm

Premises used: smoothSheafCommRing.evalHom_germ, Eq.symm, Eq.trans
-- 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))
a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)
⊢ (CommRingCat.Hom.hom
          ((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) :
        (a : (↑((locallyRingedSpace IN N).presheaf.obj (Opposite.op U)) : Type u)) → (↑(CommRingCat.of 𝕜) : Type u))
      a =
    (↑a :
        (x : ↥(Opposite.unop (Opposite.op U))) →
          (fun (x : (↑(TopCat.of N) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of N) : Type u)))
      (Subtype.mk (p := fun (x : (↑(TopCat.of N) : Type u)) ↦ x ∈ Opposite.unop (Opposite.op U)) (f x) hxU)

Tactic:
apply smoothSheafCommRing.evalHom_germ

Premises used: smoothSheafCommRing.evalHom_germ
-- 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
f : M → N
hf : ContMDiff IM IN ∞ f
x : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalHom (R :=
    (↑((locallyRingedSpace IN N).presheaf.stalk
          ((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)) :
      Type u))
    (S := (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u)) (F :=
    (↑((locallyRingedSpace IN N).presheaf.stalk
            ((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)) :
        Type u) →+*
      (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x))

Tactic:
⟨fun a ha ↦ ?_⟩

Premises used: IsLocalHom.mk
-- 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
f : M → N
hf : ContMDiff IM IN ∞ f
x : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)
a :
  (↑((locallyRingedSpace IN N).presheaf.stalk
        ((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)) :
    Type u)
ha :
  ¬Eq (α := 𝕜)
      ((smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x :
            (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
          ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x) :
                (a :
                    (↑((locallyRingedSpace IN N).presheaf.stalk
                          ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base :
                              (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                                (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                            x)) :
                      Type u)) →
                  (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u))
              a :
            (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u)) :
        𝕜)
      (0 : 𝕜)
⊢ ¬Eq (α := 𝕜)
      ((smoothSheafCommRing.eval IM 𝓘(𝕜, 𝕜) M 𝕜 x :
            (a : (↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) : Type u)) → 𝕜)
          ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (locallyRingedSpaceMapAux f hf) x) :
                (a :
                    (↑((locallyRingedSpace IN N).presheaf.stalk
                          ((ConcreteCategory.hom (locallyRingedSpaceMapAux f hf).base :
                              (a : (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)) →
                                (↑(↑(locallyRingedSpace IN N).toPresheafedSpace : TopCat) : Type u))
                            x)) :
                      Type u)) →
                  (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u))
              a :
            (↑((locallyRingedSpace IM M).presheaf.stalk x) : Type u)) :
        𝕜)
      (0 : 𝕜)

Tactic:
ha
-- 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
⊢ LocallyRingedSpace.Hom.stalkMap (locallyRingedSpaceMap f hf) x ≫ smoothSheafCommRing.evalHom IM 𝓘(𝕜, 𝕜) M 𝕜 x =
    smoothSheafCommRing.evalHom IN 𝓘(𝕜, 𝕜) N 𝕜 (f x)

Tactic:
stalkMap_locallyRingedSpaceMapAux f hf x

Premises used: ChartedSpace.stalkMap_locallyRingedSpaceMapAux, ChartedSpace.locallyRingedSpaceMapAux
-- 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
⊢ locallyRingedSpaceMap id ⋯ = 𝟙 (locallyRingedSpace IM M)

Tactic:
rfl

Premises used: Set.restrictPreimage, Subtype.map, smoothPresheafCommRing, Set.Mem, AlgebraicGeometry.PresheafedSpace.id, setOf, CategoryTheory.Functor.comp, ChartedSpace.locallyRingedSpaceMap, ContinuousMap.id, Set.preimage, CategoryTheory.NatTrans.id, Set.MapsTo.restrict, AlgebraicGeometry.LocallyRingedSpace.id, rfl, ChartedSpace.locallyRingedSpaceMapAux
-- 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
f : M → N
hf : ContMDiff IM IN ∞ f
g : N → P
hg : ContMDiff IN IP ∞ g
⊢ locallyRingedSpaceMap (g ∘ f) ⋯ = locallyRingedSpaceMap f hf ≫ locallyRingedSpaceMap g hg

Tactic:
rfl

Premises used: Set.restrictPreimage, CategoryTheory.NatTrans.vcomp, Subtype.map, Set.Mem, setOf, ContinuousMap.comp, CategoryTheory.Functor.comp, ChartedSpace.locallyRingedSpaceMap, Set.preimage, AlgebraicGeometry.PresheafedSpace.comp, AlgebraicGeometry.LocallyRingedSpace.comp, Set.MapsTo.restrict, rfl, ChartedSpace.locallyRingedSpaceMapAux
-- 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
U : Opens M
V : Opens (↑(↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat) : Type u)
x :
  (↑((Functor.obj
            (TopCat.Presheaf.pushforward CommRingCat
              (PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom
                  (LocallyRingedSpace.Hom.toShHom
                    (ChartedSpace.locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)))))
            (ChartedSpace.locallyRingedSpace IM ↥U).presheaf).obj
        (Opposite.op
          (Functor.obj
            (⋯.functor (f :=
              PresheafedSpace.Hom.base
                (InducedCategory.Hom.hom
                  (LocallyRingedSpace.Hom.toShHom
                    (ChartedSpace.locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)))))
            V))) :
    Type u)
g :
  (x :
      ↥(Opposite.unop
            (Functor.obj
              (Functor.op
                (Opens.map
                  (PresheafedSpace.Hom.base
                    (InducedCategory.Hom.hom
                      (LocallyRingedSpace.Hom.toShHom
                        (ChartedSpace.locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯))))))
              (Opposite.op
                (Functor.obj
                  (⋯.functor (f :=
                    PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom
                        (LocallyRingedSpace.Hom.toShHom
                          (ChartedSpace.locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)))))
                  V))) :
          Opens (↑(TopCat.of ↥U) : Type u))) →
    (fun (x : (↑(TopCat.of ↥U) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of ↥U) : Type u))
hg :
  TopCat.PrelocalPredicate.pred (T := fun (x : (↑(TopCat.of ↥U) : Type u)) ↦ 𝕜)
    (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(TopCat.of ↥U) : Type u)) ↦ 𝕜)
      (StructureGroupoid.LocalInvariantProp.localPredicate (P := ContDiffWithinAtProp IM 𝓘(𝕜, 𝕜) ∞) (↥U) 𝕜 ⋯))
    g
a : TopCat.of ↥U ⟶ TopCat.of M :=
  TopCat.ofHom { toFun := Subtype.val (p := fun (x : M) ↦ x ∈ U), continuous_toFun := ⋯ }
⊢ IsOpenEmbedding (X := (↑(TopCat.of ↥U) : Type u)) (Y := (↑(TopCat.of M) : Type u))
    (⇑(TopCat.Hom.hom a) : (a : (↑(TopCat.of ↥U) : Type u)) → (↑(TopCat.of M) : Type u))

Tactic:
have ha : IsOpenEmbedding a.hom := U.isOpenEmbedding'
-- 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
U : Opens M
⊢ Subset (α := Set (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι :=
      (↑(↑((locallyRingedSpace IM M).restrict (U := Functor.obj (Opens.toTopCat (locallyRingedSpace IM M).toTopCat) U)
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X :=
            (↑((locallyRingedSpace IM M).restrict (U :=
                    Functor.obj (Opens.toTopCat (locallyRingedSpace IM M).toTopCat) U) ⋯).toPresheafedSpace :
              TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom ((locallyRingedSpace IM M).ofRestrict ⋯)))) :
        (a : (↑(↑((locallyRingedSpace IM M).restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)))
    (Set.range (ι :=
      (↑(↑((locallyRingedSpace IM M).restrict (U := Functor.obj (Opens.toTopCat (locallyRingedSpace IM M).toTopCat) U)
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X :=
            (↑((locallyRingedSpace IM M).restrict (U :=
                    Functor.obj (Opens.toTopCat (locallyRingedSpace IM M).toTopCat) U) ⋯).toPresheafedSpace :
              TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom ((locallyRingedSpace IM M).ofRestrict ⋯)))) :
        (a : (↑(↑((locallyRingedSpace IM M).restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)))

Tactic:
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
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
U : Opens M
⊢ Subset (α := Set (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u))
    (Set.range (ι := (↑(↑(locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom (locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)))) :
        (a : (↑(↑(locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)))
    (Set.range (ι := (↑(↑(locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom (locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)))) :
        (a : (↑(↑(locallyRingedSpace IM ↥U).toPresheafedSpace : TopCat) : Type u)) →
          (↑(↑(locallyRingedSpace IM M).toPresheafedSpace : TopCat) : Type u)))

Tactic:
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
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
U : Opens M
⊢ LocallyRingedSpace.IsOpenImmersion.lift (locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)
        ((locallyRingedSpace IM M).ofRestrict ⋯) ⋯ ≫
      LocallyRingedSpace.IsOpenImmersion.lift ((locallyRingedSpace IM M).ofRestrict ⋯)
        (locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯) ⋯ =
    𝟙 ((locallyRingedSpace IM M).restrict (U := Functor.obj (Opens.toTopCat (locallyRingedSpace IM M).toTopCat) U) ⋯)

Tactic:
simp [← cancel_mono ((locallyRingedSpace IM M).ofRestrict U.isOpenEmbedding)]

Premises used: TopologicalSpace.Opens.isOpenEmbedding, CategoryTheory.cancel_mono, ChartedSpace.locallyRingedSpace, AlgebraicGeometry.LocallyRingedSpace.ofRestrict
-- 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
U : Opens M
⊢ LocallyRingedSpace.IsOpenImmersion.lift ((locallyRingedSpace IM M).ofRestrict ⋯)
        (locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯) ⋯ ≫
      LocallyRingedSpace.IsOpenImmersion.lift (locallyRingedSpaceMap (Subtype.val (p := fun (x : M) ↦ x ∈ U)) ⋯)
        ((locallyRingedSpace IM M).ofRestrict ⋯) ⋯ =
    𝟙 (locallyRingedSpace IM ↥U)

Tactic:
simp [← cancel_mono (locallyRingedSpaceMap _ contMDiff_subtype_val)]

Premises used: ChartedSpace.locallyRingedSpaceMap, CategoryTheory.cancel_mono, contMDiff_subtype_val
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
U : (Opens (↑(TopCat.of M) : Type u))ᵒᵖ
⊢ CategoryTheory.Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)) U = C^∞⟮IM, ↥(unop U); I, N⟯

Tactic:
rfl

Premises used: ChartedSpace.LiftProp, ContMDiffWithinAt, Set.Mem, ContMDiff, ContMDiffMap, ContMDiffAt, ChartedSpace.LiftPropAt, rfl