-- 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 := ⋯ }
ha :
  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))
V' : Opens ↥U := (Opens.map a).obj (⋯.functor.obj V)
b : ↥V' ≃ₜ ↥(⋯.functor.obj V) := ⋯.homeomorphOfSubsetRange (s := Subtype.val (p := fun (x : M) ↦ x ∈ U) '' V.carrier) ⋯
refine_2 :
  ContMDiff IM (M :=
    ↥(Opposite.unop
        (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))))
    IM (M' :=
    ↥(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)))
    ∞ (⇑b.symm : (a : ↥(⋯.functor.obj V)) → ↥V')
refine_2₁ :
  ∀
    (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))),
    (↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X :=
                  (ChartedSpace.locallyRingedSpace IM M).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)))
                  (Y :=
                  (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)))
                  (NatTrans.app
                    (PresheafedSpace.Hom.c
                      (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))) :
                (a :
                    (↑((ChartedSpace.locallyRingedSpace IM M).presheaf.obj (Opposite.op (⋯.functor.obj V))) : Type u)) →
                  (↑(((TopCat.Presheaf.pushforward CommRingCat
                                (LocallyRingedSpace.Hom.toShHom
                                      (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).obj
                            (ChartedSpace.locallyRingedSpace IM ↥U).presheaf).obj
                        (Opposite.op (⋯.functor.obj V))) :
                    Type u))
              (Subtype.mk (p :=
                fun
                  (f :
                    (x :
                        ↥(Opposite.unop
                            (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)))) →
                      (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u))) ↦
                TopCat.PrelocalPredicate.pred (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜)
                  (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜)
                    (StructureGroupoid.LocalInvariantProp.localPredicate (P := ContDiffWithinAtProp IM 𝓘(𝕜, 𝕜) ∞) M 𝕜
                      ⋯))
                  f)
                (g ∘ (⇑b.symm : (a : ↥(⋯.functor.obj V)) → ↥V')) ⋯)) :
          (x :
              ↥(Opposite.unop
                  ((Opens.map
                          (LocallyRingedSpace.Hom.toShHom
                                (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
                    (Opposite.op (⋯.functor.obj V))))) →
            (fun (x : (↑(TopCat.of ↥U) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of ↥U) : Type u)))
        x =
      (↑(Subtype.mk (p :=
              fun
                (f :
                  (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))) ↦
              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) 𝕜
                    ⋯))
                f)
              g hg) :
          (x :
              ↥(Opposite.unop
                  ((Opens.map
                          (LocallyRingedSpace.Hom.toShHom
                                (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
                    (Opposite.op (⋯.functor.obj V))))) →
            (fun (x : (↑(TopCat.of ↥U) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of ↥U) : Type u)))
        x
⊢ ∃ (a :
    (↑((ChartedSpace.locallyRingedSpace IM M).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)),
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            (ChartedSpace.locallyRingedSpace IM M).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)))
            (Y :=
            (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)))
            (NatTrans.app
              (PresheafedSpace.Hom.c
                (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))) :
          (a : (↑((ChartedSpace.locallyRingedSpace IM M).presheaf.obj (Opposite.op (⋯.functor.obj V))) : Type u)) →
            (↑(((TopCat.Presheaf.pushforward CommRingCat
                          (LocallyRingedSpace.Hom.toShHom
                                (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).obj
                      (ChartedSpace.locallyRingedSpace IM ↥U).presheaf).obj
                  (Opposite.op (⋯.functor.obj V))) :
              Type u))
        a =
      Subtype.mk (p :=
        fun
          (f :
            (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))) ↦
        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) 𝕜 ⋯))
          f)
        g hg

Tactic:
refine ⟨⟨g ∘ b.symm, ContMDiff.comp hg ?_⟩, Subtype.ext <| funext fun _ ↦ ?_⟩