-- Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
@[simp, reassoc, elementwise] lemma smoothSheafCommRing.forgetStalk_inv_comp_eval
    (x : TopCat.of M) :
    (smoothSheafCommRing.forgetStalk IM I M R x).inv ≫
     (DFunLike.coe (smoothSheafCommRing.evalHom IM I M R x).hom) =
    smoothSheaf.evalHom _ _ _ _

Proof state:
case w.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x✝ : ↑(TopCat.of M)
U : (OpenNhds x✝)ᵒᵖ
x : (smoothSheaf IM I M R).presheaf.obj ((OpenNhds.inclusion x✝).op.obj U)
⊢ (⇑(ConcreteCategory.hom (colimit.ι ((OpenNhds.inclusion x✝).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
        ⇑(CommRingCat.Hom.hom (evalHom IM I M R x✝)))
      x =
    smoothSheaf.evalAt IM I (↑(CommRingCat.of R)) x✝ (unop U) x

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

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ (forgetStalk IM I M R x).inv ≫ ⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) = smoothSheaf.evalHom IM I R x

Tactic:
apply Limits.colimit.hom_ext

Result:
case w
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ ∀ (j : (OpenNhds x)ᵒᵖ),
    colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
            (smoothSheaf IM I M R).presheaf)
          j ≫
        (forgetStalk IM I M R x).inv ≫ ⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
      colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
            (smoothSheaf IM I M R).presheaf)
          j ≫
        smoothSheaf.evalHom IM I R x

Proof state:
case w
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ ⇑(ConcreteCategory.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
      ⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    smoothSheaf.evalAt IM I (↑(CommRingCat.of R)) x (unop U)

Tactic:
ext x

Result:
case w.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x✝ : ↑(TopCat.of M)
U : (OpenNhds x✝)ᵒᵖ
x : (smoothSheaf IM I M R).presheaf.obj ((OpenNhds.inclusion x✝).op.obj U)
⊢ (⇑(ConcreteCategory.hom (colimit.ι ((OpenNhds.inclusion x✝).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U)) ≫
        ⇑(CommRingCat.Hom.hom (evalHom IM I M R x✝)))
      x =
    smoothSheaf.evalAt IM I (↑(CommRingCat.of R)) x✝ (unop U) x

Proof state:
case w
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ ∀ (j : (OpenNhds x)ᵒᵖ),
    colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
            (smoothSheaf IM I M R).presheaf)
          j ≫
        (forgetStalk IM I M R x).inv ≫ ⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
      colimit.ι
          (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
            (smoothSheaf IM I M R).presheaf)
          j ≫
        smoothSheaf.evalHom IM I R x

Tactic:
intro U

Result:
case w
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
          (smoothSheaf IM I M R).presheaf)
        U ≫
      (forgetStalk IM I M R x).inv ≫ ⇑(CommRingCat.Hom.hom (evalHom IM I M R x)) =
    colimit.ι
        (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj
          (smoothSheaf IM I M R).presheaf)
        U ≫
      smoothSheaf.evalHom IM I R x