-- 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)
refine_1 :
  ∀
    (a b :
      (↑((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))
    (hab :
      Eq (α :=
        (↑((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))
        ((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 :
          (↑((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))
        ((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))
            b :
          (↑((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))),
    (↑a :
        (x : ↥(Opposite.unop (Opposite.op (⋯.functor.obj V)))) →
          (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u))) =
      (↑b :
        (x : ↥(Opposite.unop (Opposite.op (⋯.functor.obj V)))) →
          (fun (x : (↑(TopCat.of M) : Type u)) ↦ 𝕜) (↑x : (↑(TopCat.of M) : Type u)))
refine_2 :
  ∀
    (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 :
      (↑((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
⊢ Function.Bijective (α :=
    (↑((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))
    (β :=
    (↑((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))
    (⇑(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))

Tactic:
refine ⟨fun a b hab ↦ Subtype.ext ?_, fun ⟨g, hg⟩ ↦ ?_⟩