[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : { x // x ∈ (Opens.map α.base).obj U }
⊢ germ Y.presheaf { val := ↑α.base ↑x, property := (_ : ↑x ∈ (Opens.map α.base).obj U) } ≫ stalkMap α ↑x =
    NatTrans.app α.c (op U) ≫ germ X.presheaf x
[PROOFSTEP]
rw [stalkMap, stalkFunctor_map_germ_assoc, stalkPushforward_germ]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ germ X.presheaf { val := ↑f x, property := (_ : ↑f x ∈ (IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) } ≫
      (restrictStalkIso X h x).inv =
    germ (restrict X h).presheaf { val := x, property := hx }
[PROOFSTEP]
rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
⊢ (restrictStalkIso X h x).inv = stalkMap (ofRestrict X h) x
[PROOFSTEP]
refine colimit.hom_ext fun V => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : (OpenNhds (↑f x))ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
induction V with
| h V => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : (OpenNhds (↑f x))ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        V ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
induction V with
| h V => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE (Set.image_preimage_subset f _)
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      (restrictStalkIso X h x).inv =
    colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
        (op V) ≫
      stalkMap (ofRestrict X h) x
[PROOFSTEP]
erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    (NatTrans.app
          (((whiskeringLeft (OpenNhds (↑(ofRestrict X h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion (↑(ofRestrict X h).base x)).op).map
            (ofRestrict X h).c)
          (op V) ≫
        NatTrans.app
            (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (restrict X h).presheaf)
            (op V) ≫
          colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(restrict X h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (restrict X h).presheaf)
            ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V))) ≫
      (restrictStalkIso X h x).hom
[PROOFSTEP]
simp_rw [Category.assoc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    NatTrans.app
        (((whiskeringLeft (OpenNhds (↑(ofRestrict X h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(ofRestrict X h).base x)).op).map
          (ofRestrict X h).c)
        (op V) ≫
      NatTrans.app
          (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (restrict X h).presheaf)
          (op V) ≫
        colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(restrict X h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (restrict X h).presheaf)
            ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V)) ≫
          (restrictStalkIso X h x).hom
[PROOFSTEP]
erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) (h.isOpenMap.functorNhds x).op]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    NatTrans.app
        (((whiskeringLeft (OpenNhds (↑(ofRestrict X h).base x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(ofRestrict X h).base x)).op).map
          (ofRestrict X h).c)
        (op V) ≫
      NatTrans.app
          (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (restrict X h).presheaf)
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion (↑f x)).op ⋙ X.presheaf)
          ((IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).op.obj ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V)))
[PROOFSTEP]
erw [← X.presheaf.map_comp_assoc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
V : OpenNhds (↑f x)
i : (IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (_ : ↑f '' (↑f ⁻¹' V.obj.1) ⊆ V.obj.1)
⊢ colimit.ι (((whiskeringLeft (OpenNhds (↑f x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj (OpenNhds.inclusion (↑f x)).op).obj X.presheaf)
      (op V) =
    X.presheaf.map
        ((NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
              ((OpenNhds.inclusion (↑(ofRestrict X h).base x)).op.obj (op V)).unop).op ≫
          (IsOpenMap.functor (_ : IsOpenMap ↑f)).op.map
            (NatTrans.app (NatTrans.op (OpenNhds.inclusionMapIso (ofRestrict X h).base x).inv) (op V))) ≫
      colimit.ι ((OpenNhds.inclusion (↑f x)).op ⋙ X.presheaf)
        ((IsOpenMap.functorNhds (_ : IsOpenMap ↑f) x).op.obj ((OpenNhds.map (ofRestrict X h).base x).op.obj (op V)))
[PROOFSTEP]
exact (colimit.w ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
⊢ IsIso (stalkMap (ofRestrict X h) x)
[PROOFSTEP]
rw [← restrictStalkIso_inv_eq_ofRestrict]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ↑f
x : ↑U
⊢ IsIso (restrictStalkIso X h x).inv
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ stalkMap (𝟙 X) x = 𝟙 (stalk X x)
[PROOFSTEP]
dsimp [stalkMap]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C (↑(𝟙 ↑X) x)).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x = 𝟙 (stalk X x)
[PROOFSTEP]
simp only [stalkPushforward.id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C (↑(𝟙 ↑X) x)).map (𝟙 X).c ≫ (stalkFunctor C x).map (Pushforward.id X.presheaf).hom = 𝟙 (stalk X x)
[PROOFSTEP]
erw [← map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C (↑(𝟙 ↑X) x)).map ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) = 𝟙 (stalk X x)
[PROOFSTEP]
convert (stalkFunctor C x).map_id X.presheaf
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ : (stalk X (↑(𝟙 ↑X) x) ⟶ stalk X x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
⊢ (𝟙 X).c ≫ (Pushforward.id X.presheaf).hom = 𝟙 X.presheaf
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ : (stalk X (↑(𝟙 ↑X) x) ⟶ stalk X x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ NatTrans.app ((𝟙 X).c ≫ (Pushforward.id X.presheaf).hom) (op U✝) = NatTrans.app (𝟙 X.presheaf) (op U✝)
[PROOFSTEP]
simp only [id_c, id_comp, Pushforward.id_hom_app, op_obj, eqToHom_refl, map_id]
[GOAL]
case h.e'_2.h.h.e'_8.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
e_1✝ : (stalk X (↑(𝟙 ↑X) x) ⟶ stalk X x) = ((stalkFunctor C x).obj X.presheaf ⟶ (stalkFunctor C x).obj X.presheaf)
U✝ : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op ((Opens.map (𝟙 ↑X)).obj (op U✝).unop))) = NatTrans.app (𝟙 X.presheaf) (op U✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ stalkMap (α ≫ β) x = stalkMap β (↑α.base x) ≫ stalkMap α x
[PROOFSTEP]
dsimp [stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
⊢ colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
      colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
        colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
refine colimit.hom_ext fun U => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
induction U with
| h U => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        U ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
induction U with
| h U => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
U : OpenNhds (↑(α.base ≫ β.base) x)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op U) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op U) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
cases U
[GOAL]
case h.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y Z : PresheafedSpace C
α : X ⟶ Y
β : Y ⟶ Z
x : ↑↑X
obj✝ : Opens ↑↑Z
property✝ : ↑(α.base ≫ β.base) x ∈ obj✝
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op { obj := obj✝, property := property✝ }) ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op (α ≫ β).c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map (α.base ≫ β.base) x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map (α.base ≫ β.base) x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑(α.base ≫ β.base) x))ᵒᵖ (Opens ↑↑Z)ᵒᵖ C).obj
              (OpenNhds.inclusion (↑(α.base ≫ β.base) x)).op).obj
          Z.presheaf)
        (op { obj := obj✝, property := property✝ }) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑β.base (↑α.base x))).op β.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map β.base (↑α.base x) ⋙ OpenNhds.inclusion (↑α.base x)).op) Y.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion (↑α.base x)).op ⋙ Y.presheaf) (OpenNhds.map β.base (↑α.base x)).op) ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑α.base x)).op α.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map α.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map α.base x).op
[PROOFSTEP]
simp only [whiskeringLeft_obj_obj, comp_obj, op_obj, unop_op, OpenNhds.inclusion_obj, ι_colimMap_assoc,
  pushforwardObj_obj, Opens.map_comp_obj, whiskerLeft_app, comp_c_app, OpenNhds.map_obj, whiskerRight_app,
  NatTrans.id_app, map_id, colimit.ι_pre, id_comp, assoc, colimit.ι_pre_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalk X x = stalk X x'
[PROOFSTEP]
rw [h₂]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalk Y (↑α.base x) = stalk Y (↑β.base x')
[PROOFSTEP]
rw [h₁, h₂]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑β.base x')) ≫ stalkMap β x'
[PROOFSTEP]
ext
[GOAL]
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
U✝ : Opens ↑↑Y
hxU✝ : ↑α.base x ∈ U✝
⊢ germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫
      eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑β.base x')) ≫ stalkMap β x'
[PROOFSTEP]
substs h₁ h₂
[GOAL]
case ih
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x : ↑↑X
U✝ : Opens ↑↑Y
hxU✝ : ↑α.base x ∈ U✝
⊢ germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x) =
    germ Y.presheaf { val := ↑α.base x, property := hxU✝ } ≫
      eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base x)) ≫ stalkMap α x
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ stalk Y (↑α.base x) = stalk Y (↑β.base x)
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ stalkMap α x = eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑β.base x)) ≫ stalkMap β x
[PROOFSTEP]
rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalk X x = stalk X x'
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalk Y (↑α.base x) = stalk Y (↑α.base x')
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X x') =
    eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base x')) ≫ stalkMap α x'
[PROOFSTEP]
rw [stalkMap.congr α α rfl x x' h]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
⊢ ∃ inv, stalkMap α x ≫ inv = 𝟙 (stalk Y (↑α.base x)) ∧ inv ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
let β : Y ⟶ X := CategoryTheory.inv α
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ ∃ inv, stalkMap α x ≫ inv = 𝟙 (stalk Y (↑α.base x)) ∧ inv ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
have h_eq : (α ≫ β).base x = x := by
  rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
    -- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
        -- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
        -- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
        -- type for an inverse.
        -- To get a proper inverse, we need to compose with the `eq_to_hom` arrow
        -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
⊢ ↑(α ≫ β).base x = x
[PROOFSTEP]
rw [IsIso.hom_inv_id α, id_base, TopCat.id_app]
  -- Intuitively, the inverse of the stalk map of `α` at `x` should just be the stalk map of `β`
      -- at `α x`. Unfortunately, we have a problem with dependent type theory here: Because `x`
      -- is not *definitionally* equal to `β (α x)`, the map `stalk_map β (α x)` has not the correct
      -- type for an inverse.
      -- To get a proper inverse, we need to compose with the `eq_to_hom` arrow
      -- `X.stalk x ⟶ X.stalk ((α ≫ β).base x)`.
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ ∃ inv, stalkMap α x ≫ inv = 𝟙 (stalk Y (↑α.base x)) ∧ inv ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
refine' ⟨eqToHom (show X.stalk x = X.stalk ((α ≫ β).base x) by rw [h_eq]) ≫ (stalkMap β (α.base x) : _), _, _⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ stalk X x = stalk X (↑(α ≫ β).base x)
[PROOFSTEP]
rw [h_eq]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ stalkMap α x ≫ eqToHom (_ : stalk X x = stalk X (↑(α ≫ β).base x)) ≫ stalkMap β (↑α.base x) = 𝟙 (stalk Y (↑α.base x))
[PROOFSTEP]
rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base (↑(α ≫ β).base x))) ≫
      stalkMap α (↑(α ≫ β).base x) ≫ stalkMap β (↑α.base x) =
    𝟙 (stalk Y (↑α.base x))
[PROOFSTEP]
erw [← stalkMap.comp β α (α.base x)]
[GOAL]
case refine'_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ eqToHom (_ : stalk Y (↑α.base x) = stalk Y (↑α.base (↑(α ≫ β).base x))) ≫ stalkMap (β ≫ α) (↑α.base x) =
    𝟙 (stalk Y (↑α.base x))
[PROOFSTEP]
rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp]
[GOAL]
case refine'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : ↑(α ≫ β).base x = x
⊢ (eqToHom (_ : stalk X x = stalk X (↑(α ≫ β).base x)) ≫ stalkMap β (↑α.base x)) ≫ stalkMap α x = 𝟙 (stalk X x)
[PROOFSTEP]
rw [Category.assoc, ← stalkMap.comp, congr_hom _ _ (IsIso.hom_inv_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl,
  Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ stalkSpecializes Y.presheaf (_ : ↑f.base x ⤳ ↑f.base y) ≫ stalkMap f x = stalkMap f y ≫ stalkSpecializes X.presheaf h
[PROOFSTEP]
dsimp [stalkSpecializes, stalkMap, stalkFunctor, stalkPushforward]
  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
⊢ colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
        { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
          ι :=
            NatTrans.mk fun U =>
              colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
      colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
        colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
          colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
      colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
        { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
          ι :=
            NatTrans.mk fun U =>
              colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
refine colimit.hom_ext fun j => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : (OpenNhds (↑f.base y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
induction j with
| h j => ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : (OpenNhds (↑f.base y))ᵒᵖ
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        j ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
induction j with
| h j => ?_
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        (op j) ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι
        (((whiskeringLeft (OpenNhds (↑f.base y))ᵒᵖ (Opens ↑↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (↑f.base y)).op).obj
          Y.presheaf)
        (op j) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ colimit.ι ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf) (op j) ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
          { pt := colimit ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion (↑f.base x)).op ⋙ Y.presheaf)
                  (op { obj := U.unop.obj, property := (_ : ↑f.base x ∈ U.unop.obj.carrier) }) } ≫
        colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base x)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base x ⋙ OpenNhds.inclusion x).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion x).op ⋙ X.presheaf) (OpenNhds.map f.base x).op =
    colimit.ι ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf) (op j) ≫
      (colimMap (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c) ≫
          colimMap (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf) ≫
            colimit.pre ((OpenNhds.inclusion y).op ⋙ X.presheaf) (OpenNhds.map f.base y).op) ≫
        colimit.desc ((OpenNhds.inclusion y).op ⋙ X.presheaf)
          { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
            ι :=
              NatTrans.mk fun U =>
                colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                  (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }
[PROOFSTEP]
simp only [colimit.ι_desc_assoc, comp_obj, op_obj, unop_op, ι_colimMap_assoc, colimit.map_desc, OpenNhds.inclusion_obj,
  pushforwardObj_obj, whiskerLeft_app, OpenNhds.map_obj, whiskerRight_app, NatTrans.id_app, map_id, colimit.ι_pre,
  id_comp, assoc, colimit.pre_desc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    colimit.ι ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf) (op j) ≫
      colimit.desc ((OpenNhds.inclusion (↑f.base y)).op ⋙ Y.presheaf)
        ((Cocones.precompose (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c)).obj
          ((Cocones.precompose (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf)).obj
            (Cocone.whisker (OpenNhds.map f.base y).op
              { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                ι :=
                  NatTrans.mk fun U =>
                    colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                      (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) })))
[PROOFSTEP]
erw [colimit.ι_desc]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    NatTrans.app
      ((Cocones.precompose (whiskerLeft (OpenNhds.inclusion (↑f.base y)).op f.c)).obj
          ((Cocones.precompose (whiskerRight (𝟙 (OpenNhds.map f.base y ⋙ OpenNhds.inclusion y).op) X.presheaf)).obj
            (Cocone.whisker (OpenNhds.map f.base y).op
              { pt := colimit ((OpenNhds.inclusion x).op ⋙ X.presheaf),
                ι :=
                  NatTrans.mk fun U =>
                    colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
                      (op { obj := U.unop.obj, property := (_ : x ∈ U.unop.obj.carrier) }) }))).ι
      (op j)
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    NatTrans.app f.c (op ((OpenNhds.inclusion (↑f.base y)).obj j)) ≫
      X.presheaf.map (𝟙 (op ((OpenNhds.inclusion y).obj ((OpenNhds.map f.base y).obj j)))) ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
          (op
            { obj := ((OpenNhds.map f.base y).obj j).obj,
              property := (_ : x ∈ (op ((OpenNhds.map f.base y).obj j)).unop.obj.carrier) })
[PROOFSTEP]
erw [X.presheaf.map_id, id_comp]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
f : X ⟶ Y
x y : ↑↑X
h : x ⤳ y
j : OpenNhds (↑f.base y)
⊢ NatTrans.app f.c (op j.obj) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op { obj := (Opens.map f.base).obj j.obj, property := (_ : ↑f.base x ∈ (op j).unop.obj.carrier) }) =
    NatTrans.app f.c (op ((OpenNhds.inclusion (↑f.base y)).obj j)) ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf)
        (op
          { obj := ((OpenNhds.map f.base y).obj j).obj,
            property := (_ : x ∈ (op ((OpenNhds.map f.base y).obj j)).unop.obj.carrier) })
[PROOFSTEP]
rfl


[GOAL]
k : Type u
inst✝⁹ : CommRing k
G : Type u
inst✝⁸ : Group G
V : Type v
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
g : G
v : V
⊢ ↑(conjugate π g) (↑i v) = v
[PROOFSTEP]
rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, mul_left_inv, ← one_def, one_smul]
[GOAL]
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝ : Fintype G
g : G
v : W
⊢ ↑(sumOfConjugates G π) (MonoidAlgebra.single g 1 • v) = MonoidAlgebra.single g 1 • ↑(sumOfConjugates G π) v
[PROOFSTEP]
simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
[GOAL]
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝ : Fintype G
g : G
v : W
⊢ ∑ x : G, MonoidAlgebra.single x⁻¹ 1 • ↑π (MonoidAlgebra.single x 1 • MonoidAlgebra.single g 1 • v) =
    ∑ x : G, MonoidAlgebra.single g 1 • MonoidAlgebra.single x⁻¹ 1 • ↑π (MonoidAlgebra.single x 1 • v)
[PROOFSTEP]
refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
[GOAL]
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i✝ : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i✝ v) = v
inst✝ : Fintype G
g : G
v : W
i : G
⊢ MonoidAlgebra.single i⁻¹ 1 • ↑π (MonoidAlgebra.single i 1 • MonoidAlgebra.single g 1 • v) =
    MonoidAlgebra.single g 1 •
      MonoidAlgebra.single ((fun x => x * g) i)⁻¹ 1 • ↑π (MonoidAlgebra.single ((fun x => x * g) i) 1 • v)
[PROOFSTEP]
simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : W
⊢ ↑(equivariantProjection G π) v = ⅟↑(Fintype.card G) • ∑ g : G, ↑(conjugate π g) v
[PROOFSTEP]
simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
⊢ ↑(equivariantProjection G π) (↑i v) = v
[PROOFSTEP]
rw [equivariantProjection_apply]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
⊢ ⅟↑(Fintype.card G) • ∑ g : G, ↑(conjugate π g) (↑i v) = v
[PROOFSTEP]
simp only [conjugate_i π i h]
[GOAL]
k : Type u
inst✝¹¹ : CommRing k
G : Type u
inst✝¹⁰ : Group G
V : Type v
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module k V
inst✝⁷ : Module (MonoidAlgebra k G) V
inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
inst✝³ : Module (MonoidAlgebra k G) W
inst✝² : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
⊢ ⅟↑(Fintype.card G) • ∑ x : G, v = v
[PROOFSTEP]
rw [Finset.sum_const, Finset.card_univ, nsmul_eq_smul_cast k, smul_smul, Invertible.invOf_mul_self, one_smul]
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
⊢ ∃ g, LinearMap.comp g f = LinearMap.id
[PROOFSTEP]
obtain ⟨φ, hφ⟩ :=
  (f.restrictScalars k).exists_leftInverse_of_injective <| by
    simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
⊢ LinearMap.ker (↑k f) = ⊥
[PROOFSTEP]
simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
φ : W →ₗ[k] V
hφ : LinearMap.comp φ (↑k f) = LinearMap.id
⊢ ∃ g, LinearMap.comp g f = LinearMap.id
[PROOFSTEP]
refine ⟨φ.equivariantProjection G, FunLike.ext _ _ ?_⟩
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
φ : W →ₗ[k] V
hφ : LinearMap.comp φ (↑k f) = LinearMap.id
⊢ ∀ (x : V), ↑(LinearMap.comp (LinearMap.equivariantProjection G φ) f) x = ↑LinearMap.id x
[PROOFSTEP]
exact φ.equivariantProjection_condition G _ <| FunLike.congr_fun hφ
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
⊢ ∃ q, IsCompl p q
[PROOFSTEP]
have : IsScalarTower k (MonoidAlgebra k G) p := p.isScalarTower'
[GOAL]
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
this : IsScalarTower k (MonoidAlgebra k G) { x // x ∈ p }
⊢ ∃ q, IsCompl p q
[PROOFSTEP]
rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
this : IsScalarTower k (MonoidAlgebra k G) { x // x ∈ p }
f : V →ₗ[MonoidAlgebra k G] { x // x ∈ p }
hf : LinearMap.comp f (Submodule.subtype p) = LinearMap.id
⊢ ∃ q, IsCompl p q
[PROOFSTEP]
refine ⟨LinearMap.ker f, LinearMap.isCompl_of_proj ?_⟩
[GOAL]
case intro
k : Type u
inst✝¹¹ : Field k
G : Type u
inst✝¹⁰ : Fintype G
inst✝⁹ : Invertible ↑(Fintype.card G)
inst✝⁸ : Group G
V : Type u
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type u
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
p : Submodule (MonoidAlgebra k G) V
this : IsScalarTower k (MonoidAlgebra k G) { x // x ∈ p }
f : V →ₗ[MonoidAlgebra k G] { x // x ∈ p }
hf : LinearMap.comp f (Submodule.subtype p) = LinearMap.id
⊢ ∀ (x : { x // x ∈ p }), ↑f ↑x = x
[PROOFSTEP]
exact FunLike.congr_fun hf


[GOAL]
R : Type u
inst✝ : CommRing R
x✝¹ x✝ : MaximalSpectrum R
asIdeal✝¹ : Ideal R
IsMaximal✝¹ : Ideal.IsMaximal asIdeal✝¹
asIdeal✝ : Ideal R
IsMaximal✝ : Ideal.IsMaximal asIdeal✝
h :
  toPrimeSpectrum { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } =
    toPrimeSpectrum { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
⊢ { asIdeal := asIdeal✝¹, IsMaximal := IsMaximal✝¹ } = { asIdeal := asIdeal✝, IsMaximal := IsMaximal✝ }
[PROOFSTEP]
simpa only [MaximalSpectrum.mk.injEq] using (PrimeSpectrum.ext_iff _ _).mp h
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}
[PROOFSTEP]
simp only [isClosed_singleton_iff_isMaximal]
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | Ideal.IsMaximal x.asIdeal}
[PROOFSTEP]
ext ⟨x, _⟩
[GOAL]
case h.mk
R : Type u
inst✝ : CommRing R
x : Ideal R
IsPrime✝ : Ideal.IsPrime x
⊢ { asIdeal := x, IsPrime := IsPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, IsPrime := IsPrime✝ } ∈ {x | Ideal.IsMaximal x.asIdeal}
[PROOFSTEP]
exact ⟨fun ⟨y, hy⟩ => hy ▸ y.IsMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩
[GOAL]
R : Type u
inst✝ : CommRing R
x : MaximalSpectrum R
⊢ toPrimeSpectrum ⁻¹' {toPrimeSpectrum x} = {x}
[PROOFSTEP]
simpa only [← image_singleton] using preimage_image_eq { x } toPrimeSpectrum_injective
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ (v : MaximalSpectrum R),
      Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
        (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) =
    ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈
      ⨅ (v : MaximalSpectrum R),
        Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
          (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) ↔
    x ∈ ⊥
[PROOFSTEP]
rw [Algebra.mem_bot, Algebra.mem_iInf]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) ↔
    x ∈ range ↑(algebraMap R K)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) →
    x ∈ range ↑(algebraMap R K)
[PROOFSTEP]
contrapose
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ ¬x ∈ range ↑(algebraMap R K) →
    ¬∀ (i : MaximalSpectrum R),
        x ∈
          Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
            (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
intro hrange hlocal
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
⊢ False
[PROOFSTEP]
let denom : Ideal R := (Submodule.span R {1} : Submodule R K).colon (Submodule.span R { x })
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
⊢ False
[PROOFSTEP]
have hdenom : (1 : R) ∉ denom := by
  intro hdenom
  rcases Submodule.mem_span_singleton.mp (Submodule.mem_colon.mp hdenom x <| Submodule.mem_span_singleton_self x) with
    ⟨y, hy⟩
  exact hrange ⟨y, by rw [← mul_one <| algebraMap R K y, ← Algebra.smul_def, hy, one_smul]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
⊢ ¬1 ∈ denom
[PROOFSTEP]
intro hdenom
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : 1 ∈ denom
⊢ False
[PROOFSTEP]
rcases Submodule.mem_span_singleton.mp (Submodule.mem_colon.mp hdenom x <| Submodule.mem_span_singleton_self x) with
  ⟨y, hy⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : 1 ∈ denom
y : R
hy : y • 1 = 1 • x
⊢ False
[PROOFSTEP]
exact hrange ⟨y, by rw [← mul_one <| algebraMap R K y, ← Algebra.smul_def, hy, one_smul]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : 1 ∈ denom
y : R
hy : y • 1 = 1 • x
⊢ ↑(algebraMap R K) y = x
[PROOFSTEP]
rw [← mul_one <| algebraMap R K y, ← Algebra.smul_def, hy, one_smul]
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : ¬1 ∈ denom
⊢ False
[PROOFSTEP]
rcases denom.exists_le_maximal fun h => (h ▸ hdenom) Submodule.mem_top with ⟨max, hmax, hle⟩
[GOAL]
case h.mp.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hrange : ¬x ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    x ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R := Submodule.colon (Submodule.span R {1}) (Submodule.span R {x})
hdenom : ¬1 ∈ denom
max : Ideal R
hmax : Ideal.IsMaximal max
hle : denom ≤ max
⊢ False
[PROOFSTEP]
rcases hlocal ⟨max, hmax⟩ with ⟨n, d, hd, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
⊢ False
[PROOFSTEP]
apply hd (hle <| Submodule.mem_colon.mpr fun _ hy => _)
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
⊢ ∀ (x : K), x ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹} → d • x ∈ Submodule.span R {1}
[PROOFSTEP]
intro _ hy
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
x✝ : K
hy : x✝ ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹}
⊢ d • x✝ ∈ Submodule.span R {1}
[PROOFSTEP]
rcases Submodule.mem_span_singleton.mp hy with ⟨y, rfl⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
y : R
hy :
  y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹) ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹}
⊢ d • y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹) ∈ Submodule.span R {1}
[PROOFSTEP]
exact
  Submodule.mem_span_singleton.mpr
    ⟨y * n, by
      rw [Algebra.smul_def, mul_one, map_mul, smul_comm, Algebra.smul_def, Algebra.smul_def,
        mul_comm <| algebraMap R K d,
        inv_mul_cancel_right₀ <|
          (map_ne_zero_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K).mpr fun h => (h ▸ hd) max.zero_mem]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
max : Ideal R
hmax : Ideal.IsMaximal max
n d : R
hd : d ∈ Ideal.primeCompl { asIdeal := max, IsMaximal := hmax }.asIdeal
hrange : ¬↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈ range ↑(algebraMap R K)
hlocal :
  ∀ (i : MaximalSpectrum R),
    ↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹ ∈
      Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
        (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
denom : Ideal R :=
  Submodule.colon (Submodule.span R {1}) (Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹})
hdenom : ¬1 ∈ denom
hle : denom ≤ max
y : R
hy :
  y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹) ∈ Submodule.span R {↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹}
⊢ (y * n) • 1 = d • y • (↑(algebraMap R K) n * (↑(algebraMap R K) d)⁻¹)
[PROOFSTEP]
rw [Algebra.smul_def, mul_one, map_mul, smul_comm, Algebra.smul_def, Algebra.smul_def, mul_comm <| algebraMap R K d,
  inv_mul_cancel_right₀ <|
    (map_ne_zero_iff _ <| NoZeroSMulDivisors.algebraMap_injective R K).mpr fun h => (h ▸ hd) max.zero_mem]
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ range ↑(algebraMap R K) →
    ∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
rintro ⟨y, rfl⟩ ⟨v, hv⟩
[GOAL]
case h.mpr.intro.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsMaximal v
⊢ ↑(algebraMap R K) y ∈
    Localization.subalgebra.ofField K (Ideal.primeCompl { asIdeal := v, IsMaximal := hv }.asIdeal)
      (_ : Ideal.primeCompl { asIdeal := v, IsMaximal := hv }.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsMaximal v
⊢ ↑(algebraMap R K) y = ↑(algebraMap R K) y * (↑(algebraMap R K) 1)⁻¹
[PROOFSTEP]
rw [map_one, inv_one, mul_one]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ ⨅ (v : PrimeSpectrum R),
      Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
        (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) =
    ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈
      ⨅ (v : PrimeSpectrum R),
        Localization.subalgebra.ofField K (Ideal.primeCompl v.asIdeal)
          (_ : Ideal.primeCompl v.asIdeal ≤ nonZeroDivisors R) ↔
    x ∈ ⊥
[PROOFSTEP]
rw [Algebra.mem_iInf]
[GOAL]
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) ↔
    x ∈ ⊥
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) →
    x ∈ ⊥
[PROOFSTEP]
rw [← MaximalSpectrum.iInf_localization_eq_bot, Algebra.mem_iInf]
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ (∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)) →
    ∀ (i : MaximalSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
exact fun hx ⟨v, hv⟩ => hx ⟨v, hv.isPrime⟩
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ ⊥ →
    ∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
rw [Algebra.mem_bot]
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
⊢ x ∈ Set.range ↑(algebraMap R K) →
    ∀ (i : PrimeSpectrum R),
      x ∈
        Localization.subalgebra.ofField K (Ideal.primeCompl i.asIdeal)
          (_ : Ideal.primeCompl i.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
rintro ⟨y, rfl⟩ ⟨v, hv⟩
[GOAL]
case h.mpr.intro.mk
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsPrime v
⊢ ↑(algebraMap R K) y ∈
    Localization.subalgebra.ofField K (Ideal.primeCompl { asIdeal := v, IsPrime := hv }.asIdeal)
      (_ : Ideal.primeCompl { asIdeal := v, IsPrime := hv }.asIdeal ≤ nonZeroDivisors R)
[PROOFSTEP]
exact ⟨y, 1, v.ne_top_iff_one.mp hv.ne_top, by rw [map_one, inv_one, mul_one]⟩
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
y : R
v : Ideal R
hv : Ideal.IsPrime v
⊢ ↑(algebraMap R K) y = ↑(algebraMap R K) y * (↑(algebraMap R K) 1)⁻¹
[PROOFSTEP]
rw [map_one, inv_one, mul_one]