awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommGroup A
inst_26 : CommGroup A'
inst_27 : LieGroup I ∞ A
inst_28 : LieGroup I' ∞ A'
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafCommGroup IM I M A)
      (CategoryTheory.forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        CommGrpCat.carrier)))

Tactic:
exact (smoothSheaf IM I M A).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, smoothSheaf
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Ring R
inst_26 : ContMDiffRing I ∞ R
rw :
  CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafRing IM I M R)
      (CategoryTheory.forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        RingCat.carrier)))
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u)) (smoothPresheafRing IM I M R)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget RingCat)]

Premises used: RingCat, CategoryTheory.forget, CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Ring R
inst_26 : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafRing IM I M R)
      (CategoryTheory.forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        RingCat.carrier)))

Tactic:
(smoothSheaf IM I M R).property

Premises used: TopCat.subpresheafToTypes, ChartedSpace.LiftProp, ContMDiffWithinAt, Set.Mem, ContMDiff, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, smoothSheaf, ContMDiffAt, ChartedSpace.LiftPropAt
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Ring R
inst_26 : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafRing IM I M R)
      (CategoryTheory.forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        RingCat.carrier)))

Tactic:
exact (smoothSheaf IM I M R).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, smoothSheaf
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommRing R
inst_26 : ContMDiffRing I ∞ R
rw :
  CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafCommRing IM I M R)
      (CategoryTheory.forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)))
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u)) (smoothPresheafCommRing IM I M R)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _
      (CategoryTheory.forget CommRingCat)]

Premises used: CommRingCat, CategoryTheory.forget, CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommRing R
inst_26 : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafCommRing IM I M R)
      (CategoryTheory.forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)))

Tactic:
(smoothSheaf IM I M R).property

Premises used: TopCat.subpresheafToTypes, ChartedSpace.LiftProp, ContMDiffWithinAt, Set.Mem, ContMDiff, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, smoothSheaf, ContMDiffAt, ChartedSpace.LiftPropAt
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommRing R
inst_26 : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafCommRing IM I M R)
      (CategoryTheory.forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier)))

Tactic:
exact (smoothSheaf IM I M R).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, smoothSheaf
-- 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
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommRing R
inst_26 : ContMDiffRing I ∞ R
⊢ Eq (α :=
    CategoryTheory.Sheaf (C := Opens (↑(TopCat.of M) : Type u)) (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
      (Type u))
    (CategoryTheory.Functor.obj
      (CategoryTheory.sheafCompose (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
        (CategoryTheory.forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)))
      (smoothSheafCommRing IM I M R))
    (smoothSheaf IM I M R)

Tactic:
rfl

Premises used: TopCat.subpresheafToTypes, ChartedSpace.LiftProp, ContMDiffWithinAt, StructureGroupoid.LocalInvariantProp.sheaf, Set.Mem, ContMDiff, CategoryTheory.Functor.comp, smoothSheaf, ContMDiffAt, TopCat.subsheafToTypes, ChartedSpace.LiftPropAt, rfl
-- 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
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
x : (↑(TopCat.of M) : Type u)
U : (OpenNhds x)ᵒᵖ
⊢ CategoryStruct.comp (Y :=
      (↑(colimit ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))) : Type u))
      (↾(⇑(CommRingCat.Hom.hom
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (Iso.hom (forgetStalk IM I M R x)) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) U

Tactic:
ι_preservesColimitIso_hom (forget CommRingCat) _ _

Premises used: ChartedSpace.LiftProp, CategoryTheory.Functor.op, ContMDiffWithinAt, Set.Mem, CommRingCat, ContMDiff, CategoryTheory.Functor.comp, TopCat.Presheaf.stalk, CategoryTheory.Limits.colimit, CategoryTheory.ι_preservesColimitIso_hom, CategoryTheory.forget, ContMDiffAt, ChartedSpace.LiftPropAt
-- 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
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
x : (↑(TopCat.of M) : Type u)
U : (OpenNhds x)ᵒᵖ
dsimp :
  Eq (α :=
    Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) (op ((OpenNhds.inclusion x).obj (unop U))) ⟶
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
    (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) U ≫
      Iso.inv (forgetStalk IM I M R x))
    (↾(⇑(CommRingCat.Hom.hom
            (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
          (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
⊢ Eq (α :=
    ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)).obj U ⟶
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
    (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) U ≫
      Iso.inv (forgetStalk IM I M R x))
    (↾(⇑(CommRingCat.Hom.hom
            (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
        (a : (↑(((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf).obj U) : Type u)) →
          (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))

Tactic:
dsimp
-- 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
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
x : (↑(TopCat.of M) : Type u)
U : (OpenNhds x)ᵒᵖ
rw :
  Eq (α :=
    Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) (op ((OpenNhds.inclusion x).obj (unop U))) ⟶
      colimit ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)))
    (CategoryStruct.comp (Y :=
      (↑(colimit ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))) : Type u))
      (↾(⇑(CommRingCat.Hom.hom
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (Iso.hom (forgetStalk IM I M R x)))
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (↾(⇑(CommRingCat.Hom.hom
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (Iso.hom (forgetStalk IM I M R x)))
⊢ Eq (α :=
    Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) (op ((OpenNhds.inclusion x).obj (unop U))) ⟶
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
    (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) U ≫
      Iso.inv (forgetStalk IM I M R x))
    (↾(⇑(CommRingCat.Hom.hom
            (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
          (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))

Tactic:
rw [Iso.comp_inv_eq, ← smoothSheafCommRing.ι_forgetStalk_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, smoothSheafCommRing.ι_forgetStalk_hom
-- 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
R : Type u
inst_9 : TopologicalSpace R
inst_10 : ChartedSpace H R
inst_11 : CommRing R
inst_12 : ContMDiffRing I ∞ R
x : (↑(TopCat.of M) : Type u)
U : (OpenNhds x)ᵒᵖ
⊢ Eq (α :=
    Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) (op ((OpenNhds.inclusion x).obj (unop U))) ⟶
      colimit ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)))
    (CategoryStruct.comp (Y :=
      (↑(colimit ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))) : Type u))
      (↾(⇑(CommRingCat.Hom.hom
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (Iso.hom (forgetStalk IM I M R x)))
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (↾(⇑(CommRingCat.Hom.hom
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj (unop U)))) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (Iso.hom (forgetStalk IM I M R x)))

Tactic:
rfl