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 : CommRing R
inst_26 : ContMDiffRing I ∞ R
x : (↑(TopCat.of M) : Type u)
refine_1 :
  (U : (OpenNhds x)ᵒᵖ) →
    (Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑(TopCat.of M) : Type u))ᵒᵖ CommRingCat)
              (OpenNhds.inclusion x).op)
            (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))).obj
        U ⟶
      Functor.obj (Functor.obj (Functor.const (OpenNhds x)ᵒᵖ) (CommRingCat.of R)) U
refine_2 :
  ∀ ⦃X Y : (OpenNhds x)ᵒᵖ⦄ (f : X ⟶ Y),
    Eq (α :=
      (Functor.obj
              (Functor.obj (Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑(TopCat.of M) : Type u))ᵒᵖ CommRingCat)
                (OpenNhds.inclusion x).op)
              (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))).obj
          X ⟶
        Functor.obj (Functor.obj (Functor.const (OpenNhds x)ᵒᵖ) (CommRingCat.of R)) Y)
      ((Functor.obj
              (Functor.obj (Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑(TopCat.of M) : Type u))ᵒᵖ CommRingCat)
                (OpenNhds.inclusion x).op)
              (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))).map
          f ≫
        (fun (U : (OpenNhds x)ᵒᵖ) ↦
            (evalAt IM I M R x (unop U) :
              Functor.obj (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))
                  (op (↑(unop U) : Opens (↑(TopCat.of M) : Type u))) ⟶
                CommRingCat.of R))
          Y)
      ((fun (U : (OpenNhds x)ᵒᵖ) ↦
            (evalAt IM I M R x (unop U) :
              Functor.obj (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))
                  (op (↑(unop U) : Opens (↑(TopCat.of M) : Type u))) ⟶
                CommRingCat.of R))
          X ≫
        CategoryTheory.Functor.map (Functor.obj (Functor.const (OpenNhds x)ᵒᵖ) (CommRingCat.of R)) f)
⊢ TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x ⟶ CommRingCat.of R

Tactic:
refine CategoryTheory.Limits.colimit.desc _ ⟨_, ⟨fun U ↦ ?_, ?_⟩⟩

Premises used: CategoryTheory.Limits.Cocone.mk, CategoryTheory.NatTrans.mk, CategoryTheory.Limits.colimit.desc
-- 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
x : (↑(TopCat.of M) : Type u)
U : (OpenNhds x)ᵒᵖ
⊢ (Functor.obj
          (Functor.obj (Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑(TopCat.of M) : Type u))ᵒᵖ CommRingCat)
            (OpenNhds.inclusion x).op)
          (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R))).obj
      U ⟶
    Functor.obj (Functor.obj (Functor.const (OpenNhds x)ᵒᵖ) (CommRingCat.of R)) U

Tactic:
apply smoothSheafCommRing.evalAt

Premises used: smoothSheafCommRing.evalAt
-- 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)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U ≫ evalHom IM I M R x =
    evalAt IM I M R x (unop U)

Tactic:
colimit.ι_desc _ _

Premises used: CategoryTheory.Functor.comp, smoothSheafCommRing.evalAt, CategoryTheory.Limits.colimit.ι_desc
-- 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
U : Opens (↑(TopCat.of M) : Type u)
x : M
hx : x ∈ U
f : (↑(Functor.obj (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) (op U)) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X :=
          TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
          (evalHom IM I M R x) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Functor.obj (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) (op U))
              (Y := TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
              (TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U x hx) :
            (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj (op U)) : Type u)) →
              (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u))
          f :
        (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) :
          Type u)) =
    (↑f : (x : ↥(unop (op U))) → (fun (x : (↑(TopCat.of M) : Type u)) ↦ R) (↑x : (↑(TopCat.of M) : Type u)))
      (Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ unop (op U)) x hx)

Tactic:
congr_arg (fun a ↦ a f) <| smoothSheafCommRing.ι_evalHom IM I M R x ⟨U, hx⟩

Premises used: Set.Mem, smoothSheafCommRing.ι_evalHom, Subtype.mk, congr_arg, Opposite.op
-- 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)
w :
  ∀ (j : (OpenNhds x)ᵒᵖ),
    colimit.ι
          (Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑(TopCat.of M) : Type u))ᵒᵖ (Type u))
              (OpenNhds.inclusion x).op)
            (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)))
          j ≫
        CategoryStruct.comp (Y :=
          (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
          (Iso.inv (forgetStalk IM I M R x))
          (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
              (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))) =
      colimit.ι
          (Functor.obj
            (Functor.obj (Functor.whiskeringLeft (OpenNhds x)ᵒᵖ (Opens (↑(TopCat.of M) : Type u))ᵒᵖ (Type u))
              (OpenNhds.inclusion x).op)
            (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)))
          j ≫
        smoothSheaf.evalHom IM I R x
⊢ Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ (↑(CommRingCat.of R) : Type u))
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (Iso.inv (forgetStalk IM I M R x))
      (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))))
    (smoothSheaf.evalHom IM I R x)

Tactic:
apply Limits.colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- 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)ᵒᵖ
w :
  Eq (α :=
    ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)).obj U ⟶ (↑(CommRingCat.of R) : Type u))
    (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 ((OpenNhds.inclusion x).op.obj U)) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))))
    (↾smoothSheaf.evalAt IM I (↑(CommRingCat.of R) : Type u) x (unop U))
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) U ≫
      CategoryStruct.comp (Y :=
        (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
        (Iso.inv (forgetStalk IM I M R x))
        (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
            (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) U ≫
      smoothSheaf.evalHom IM I R x

Tactic:
rw [smoothSheafCommRing.ι_forgetStalk_inv_assoc, smoothSheaf.ι_evalHom]

Premises used: smoothSheafCommRing.ι_forgetStalk_inv_assoc, smoothSheaf.ι_evalHom
-- 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)ᵒᵖ
w :
  ∀ (x_1 : Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) ((OpenNhds.inclusion x).op.obj U)),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (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 ((OpenNhds.inclusion x).op.obj U)) : Type u)) →
                  (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
            (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
                (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u)))))
        x_1 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun) (↾smoothSheaf.evalAt IM I (↑(CommRingCat.of R) : Type u) x (unop U)))
        x_1
⊢ Eq (α :=
    ((OpenNhds.inclusion x).op ⋙ TopCat.Sheaf.presheaf (smoothSheaf IM I M R)).obj U ⟶ (↑(CommRingCat.of R) : Type u))
    (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 ((OpenNhds.inclusion x).op.obj U)) : Type u)) →
            (↑(colimit ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
      (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))))
    (↾smoothSheaf.evalAt IM I (↑(CommRingCat.of R) : Type u) x (unop U))

Tactic:
ext x
-- 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_1 : (↑(TopCat.of M) : Type u)
U : (OpenNhds x_1)ᵒᵖ
x : Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) ((OpenNhds.inclusion x_1).op.obj U)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x_1) : Type u))
          (↾(⇑(CommRingCat.Hom.hom
                  (colimit.ι ((OpenNhds.inclusion x_1).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
              (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj ((OpenNhds.inclusion x_1).op.obj U)) : Type u)) →
                (↑(colimit ((OpenNhds.inclusion x_1).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
          (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x_1)) :
              (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x_1) : Type u)) → (↑(CommRingCat.of R) : Type u)))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾smoothSheaf.evalAt IM I (↑(CommRingCat.of R) : Type u) x_1 (unop U)))
      x

Tactic:
CategoryTheory.congr_fun (smoothSheafCommRing.ι_evalHom ..) x

Premises used: smoothSheafCommRing.ι_evalHom, CategoryTheory.congr_fun, smoothSheaf.evalAt
-- 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_1 : (↑(TopCat.of M) : Type u)
U : (OpenNhds x_1)ᵒᵖ
x : Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) ((OpenNhds.inclusion x_1).op.obj U)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x_1) : Type u))
          (↾(⇑(CommRingCat.Hom.hom
                  (colimit.ι ((OpenNhds.inclusion x_1).op ⋙ TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) U)) :
              (a : (↑((smoothSheafCommRing IM I M R).presheaf.obj ((OpenNhds.inclusion x_1).op.obj U)) : Type u)) →
                (↑(colimit ((OpenNhds.inclusion x_1).op ⋙ (smoothSheafCommRing IM I M R).presheaf)) : Type u)))
          (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x_1)) :
              (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x_1) : Type u)) → (↑(CommRingCat.of R) : Type u)))))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾smoothSheaf.evalAt IM I (↑(CommRingCat.of R) : Type u) x_1 (unop U)))
      x

Tactic:
exact CategoryTheory.congr_fun (smoothSheafCommRing.ι_evalHom ..) x

Premises used: smoothSheafCommRing.ι_evalHom, CategoryTheory.congr_fun
-- 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)
simp_rw :
  Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ R) (smoothSheaf.evalHom IM I R x)
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (Iso.inv (forgetStalk IM I M R x))
      (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
              (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)))
⊢ Eq (α := (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u) ⟶ R)
    (Iso.hom (forgetStalk IM I M R x) ≫ smoothSheaf.evalHom IM I R x)
    (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
            (evalHom IM I M R x)) :
        (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u)))

Tactic:
simp_rw [← CategoryTheory.Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- 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)
rw rw₁ :
  Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ R)
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (Iso.inv (forgetStalk IM I M R x))
      (↾(⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → (↑(CommRingCat.of R) : Type u))))
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (Iso.inv (forgetStalk IM I M R x))
      (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
              (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)))
⊢ Eq (α := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x ⟶ R) (smoothSheaf.evalHom IM I R x)
    (CategoryStruct.comp (Y :=
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u))
      (Iso.inv (forgetStalk IM I M R x))
      (↾(⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x)
              (evalHom IM I M R x)) :
          (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R)))

Tactic:
rw [← smoothSheafCommRing.forgetStalk_inv_comp_eval]

Premises used: smoothSheafCommRing.forgetStalk_inv_comp_eval
-- 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 : M
r : R
obtain :
  ∀ (y : TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheaf IM I M R)) x),
    ∃ (a :
      (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u)),
      (eval IM I M R x : (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R) a =
        smoothSheaf.eval IM I R x y
⊢ ∃ (a :
    (↑(TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheafCommRing IM I M R)) x) : Type u)),
    (eval IM I M R x : (a : (↑((smoothSheafCommRing IM I M R).presheaf.stalk x) : Type u)) → R) a = r

Tactic:
obtain ⟨y, rfl⟩ := smoothSheaf.eval_surjective IM I R x r

Premises used: smoothSheaf.eval_surjective, rfl