Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))

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

Goal state after:
case refine_1
𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
a b : ↑((ChartedSpace.locallyRingedSpace IM M).presheaf.obj (Opposite.op (⋯.functor.obj V)))
hab :
  (ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))
      a =
    (ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))
      b
⊢ ↑a = ↑b

case refine_2
𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
x✝ :
  ↑(((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)))
g :
  (x :
      ↥(Opposite.unop
          ((Opens.map
                  (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
            (Opposite.op (⋯.functor.obj V))))) →
    (fun x ↦ 𝕜) ↑x
hg : (StructureGroupoid.LocalInvariantProp.localPredicate (↥U) 𝕜 ⋯).pred g
⊢ ∃ a,
    (ConcreteCategory.hom
          ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
            (Opposite.op (⋯.functor.obj V))))
        a =
      ⟨g, hg⟩