Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case refine_2.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
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 : TopCat.of ↥U ⟶ TopCat.of M := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }
ha : IsOpenEmbedding ⇑(TopCat.Hom.hom a)
V' : Opens ↥U := (Opens.map a).obj (⋯.functor.obj V)
b : ↥V' ≃ₜ ↥(⋯.functor.obj V) := ⋯.homeomorphOfSubsetRange ⋯
⊢ ContMDiff IM IM ∞ ⇑b.symm

pp: case refine_2.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 : TopCat.of ↥U ⟶ TopCat.of M := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }
ha : IsOpenEmbedding ⇑(TopCat.Hom.hom a)
V' : Opens ↥U := (Opens.map a).obj (⋯.functor.obj V)
b : ↥V' ≃ₜ ↥(⋯.functor.obj V) := ⋯.homeomorphOfSubsetRange ⋯
x✝ :
  ↥(Opposite.unop
      ((Opens.map (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
        (Opposite.op (⋯.functor.obj V))))
⊢ ↑((ConcreteCategory.hom
            ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
              (Opposite.op (⋯.functor.obj V))))
          ⟨g ∘ ⇑b.symm, ⋯⟩)
      x✝ =
    ↑⟨g, hg⟩ x✝

Tactic:
· refine (ContMDiff.subtypeVal_comp_iff V' _).mp ?_
        rw [← ContMDiff.subtypeVal_comp_iff]
        convert! contMDiff_subtype_val
        ext x
        exact congr($(b.apply_symm_apply x).1)

Goal state after:
case refine_2.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 : TopCat.of ↥U ⟶ TopCat.of M := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ }
ha : IsOpenEmbedding ⇑(TopCat.Hom.hom a)
V' : Opens ↥U := (Opens.map a).obj (⋯.functor.obj V)
b : ↥V' ≃ₜ ↥(⋯.functor.obj V) := ⋯.homeomorphOfSubsetRange ⋯
x✝ :
  ↥(Opposite.unop
      ((Opens.map (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base).op.obj
        (Opposite.op (⋯.functor.obj V))))
⊢ ↑((ConcreteCategory.hom
            ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
              (Opposite.op (⋯.functor.obj V))))
          ⟨g ∘ ⇑b.symm, ⋯⟩)
      x✝ =
    ↑⟨g, hg⟩ x✝