[GOAL]
R : CommRingCatᵒᵖ
⊢ { obj := fun R => topObj R.unop, map := fun {R S} f => topMap f.unop }.map (𝟙 R) =
    𝟙 ({ obj := fun R => topObj R.unop, map := fun {R S} f => topMap f.unop }.obj R)
[PROOFSTEP]
dsimp
[GOAL]
R : CommRingCatᵒᵖ
⊢ topMap (𝟙 R.unop) = 𝟙 (topObj R.unop)
[PROOFSTEP]
rw [Spec.topMap_id]
[GOAL]
R S T : CommRingCatᵒᵖ
f : R ⟶ S
g : S ⟶ T
⊢ { obj := fun R => topObj R.unop, map := fun {R S} f => topMap f.unop }.map (f ≫ g) =
    { obj := fun R => topObj R.unop, map := fun {R S} f => topMap f.unop }.map f ≫
      { obj := fun R => topObj R.unop, map := fun {R S} f => topMap f.unop }.map g
[PROOFSTEP]
dsimp
[GOAL]
R S T : CommRingCatᵒᵖ
f : R ⟶ S
g : S ⟶ T
⊢ topMap (g.unop ≫ f.unop) = topMap f.unop ≫ topMap g.unop
[PROOFSTEP]
rw [Spec.topMap_comp]
[GOAL]
R : CommRingCat
⊢ (sheafedSpaceMap (𝟙 R)).c ≫
      whiskerRight
        (eqToHom
          (_ :
            (TopologicalSpace.Opens.map (sheafedSpaceMap (𝟙 R)).base).op =
              (TopologicalSpace.Opens.map (𝟙 (sheafedSpaceObj R)).base).op))
        (sheafedSpaceObj R).toPresheafedSpace.presheaf =
    (𝟙 (sheafedSpaceObj R)).c
[PROOFSTEP]
ext U
[GOAL]
case w.w
R : CommRingCat
U : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑(NatTrans.app
          ((sheafedSpaceMap (𝟙 R)).c ≫
            whiskerRight
              (eqToHom
                (_ :
                  (TopologicalSpace.Opens.map (sheafedSpaceMap (𝟙 R)).base).op =
                    (TopologicalSpace.Opens.map (𝟙 (sheafedSpaceObj R)).base).op))
              (sheafedSpaceObj R).toPresheafedSpace.presheaf)
          (op U))
      x✝ =
    ↑(NatTrans.app (𝟙 (sheafedSpaceObj R)).c (op U)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.w
R : CommRingCat
U : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑(NatTrans.app
          ((sheafedSpaceMap (𝟙 R)).c ≫
            whiskerRight (𝟙 (TopologicalSpace.Opens.map (topMap (𝟙 R))).op) (structureSheaf ↑R).val)
          (op U))
      x✝ =
    ↑(NatTrans.app (𝟙 (sheafedSpaceObj R)).c (op U)) x✝
[PROOFSTEP]
erw [NatTrans.comp_app, sheafedSpaceMap_c_app, PresheafedSpace.id_c_app, comap_id]
[GOAL]
case w.w
R : CommRingCat
U : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑(eqToHom
            (_ :
              (structureSheaf ↑R).val.obj (op (op U).unop) =
                (structureSheaf ↑R).val.obj (op ((TopologicalSpace.Opens.map (topMap (𝟙 R))).obj (op U).unop))) ≫
          NatTrans.app (whiskerRight (𝟙 (TopologicalSpace.Opens.map (topMap (𝟙 R))).op) (structureSheaf ↑R).val) (op U))
      x✝ =
    ↑((sheafedSpaceObj R).toPresheafedSpace.presheaf.map (𝟙 (op U))) x✝
case w.w.hUV
R : CommRingCat
U : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U))
⊢ (op U).unop = (TopologicalSpace.Opens.map (topMap (𝟙 R))).obj (op U).unop
[PROOFSTEP]
swap
[GOAL]
case w.w.hUV
R : CommRingCat
U : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U))
⊢ (op U).unop = (TopologicalSpace.Opens.map (topMap (𝟙 R))).obj (op U).unop
[PROOFSTEP]
rw [Spec.topMap_id, TopologicalSpace.Opens.map_id_obj_unop]
[GOAL]
case w.w
R : CommRingCat
U : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U))
⊢ ↑(eqToHom
            (_ :
              (structureSheaf ↑R).val.obj (op (op U).unop) =
                (structureSheaf ↑R).val.obj (op ((TopologicalSpace.Opens.map (topMap (𝟙 R))).obj (op U).unop))) ≫
          NatTrans.app (whiskerRight (𝟙 (TopologicalSpace.Opens.map (topMap (𝟙 R))).op) (structureSheaf ↑R).val) (op U))
      x✝ =
    ↑((sheafedSpaceObj R).toPresheafedSpace.presheaf.map (𝟙 (op U))) x✝
[PROOFSTEP]
simp [eqToHom_map]
[GOAL]
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).c ≫
      whiskerRight
        (eqToHom
          (_ :
            (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op =
              (TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).base).op))
        (sheafedSpaceObj T).toPresheafedSpace.presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).c
[PROOFSTEP]
ext
  -- Porting note : was one liner
      -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
[GOAL]
case w.w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U✝))
⊢ ↑(NatTrans.app
          ((sheafedSpaceMap (f ≫ g)).c ≫
            whiskerRight
              (eqToHom
                (_ :
                  (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op =
                    (TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).base).op))
              (sheafedSpaceObj T).toPresheafedSpace.presheaf)
          (op U✝))
      x✝ =
    ↑(NatTrans.app (sheafedSpaceMap g ≫ sheafedSpaceMap f).c (op U✝)) x✝
[PROOFSTEP]
rw [NatTrans.comp_app, sheafedSpaceMap_c_app, whiskerRight_app, eqToHom_refl]
[GOAL]
case w.w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U✝))
⊢ ↑(comap (f ≫ g) (op U✝).unop ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (op U✝).unop)
            (_ :
              ∀ (x : ↑(PrimeSpectrum.Top ↑T)),
                x ∈ ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (op U✝).unop).carrier →
                  x ∈ ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (op U✝).unop).carrier) ≫
          (sheafedSpaceObj T).toPresheafedSpace.presheaf.map
            (NatTrans.app (𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op) (op U✝)))
      x✝ =
    ↑(NatTrans.app (sheafedSpaceMap g ≫ sheafedSpaceMap f).c (op U✝)) x✝
[PROOFSTEP]
erw [(sheafedSpaceObj T).presheaf.map_id, Category.comp_id, comap_comp]
[GOAL]
case w.w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U✝))
⊢ ↑(RingHom.comp (comap g ?w.w.V ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (op U✝).unop) ?w.w.hVW)
          (comap f (op U✝).unop ?w.w.V ?w.w.hUV))
      x✝ =
    ↑(NatTrans.app (sheafedSpaceMap g ≫ sheafedSpaceMap f).c (op U✝)) x✝
case w.w.V
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U✝))
⊢ TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑S)
case w.w.hUV
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U✝))
⊢ ∀ (p : ↑(PrimeSpectrum.Top ↑S)), p ∈ ?w.w.V → ↑(PrimeSpectrum.comap f) p ∈ (op U✝).unop
case w.w.hVW
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : (forget CommRingCat).obj ((sheafedSpaceObj R).toPresheafedSpace.presheaf.obj (op U✝))
⊢ ∀ (p : ↑(PrimeSpectrum.Top ↑T)),
    p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (op U✝).unop → ↑(PrimeSpectrum.comap g) p ∈ ?w.w.V
[PROOFSTEP]
rfl
[GOAL]
R : CommRingCatᵒᵖ
⊢ { obj := fun R => sheafedSpaceObj R.unop, map := fun {X Y} f => sheafedSpaceMap f.unop }.map (𝟙 R) =
    𝟙 ({ obj := fun R => sheafedSpaceObj R.unop, map := fun {X Y} f => sheafedSpaceMap f.unop }.obj R)
[PROOFSTEP]
dsimp
[GOAL]
R : CommRingCatᵒᵖ
⊢ sheafedSpaceMap (𝟙 R.unop) = 𝟙 (sheafedSpaceObj R.unop)
[PROOFSTEP]
rw [Spec.sheafedSpaceMap_id]
[GOAL]
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun R => sheafedSpaceObj R.unop, map := fun {X Y} f => sheafedSpaceMap f.unop }.map (f ≫ g) =
    { obj := fun R => sheafedSpaceObj R.unop, map := fun {X Y} f => sheafedSpaceMap f.unop }.map f ≫
      { obj := fun R => sheafedSpaceObj R.unop, map := fun {X Y} f => sheafedSpaceMap f.unop }.map g
[PROOFSTEP]
dsimp
[GOAL]
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ sheafedSpaceMap (g.unop ≫ f.unop) = sheafedSpaceMap f.unop ≫ sheafedSpaceMap g.unop
[PROOFSTEP]
rw [Spec.sheafedSpaceMap_comp]
[GOAL]
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
r : ↑R
U : TopologicalSpace.Opens (PrimeSpectrum ↑R) := PrimeSpectrum.basicOpen r
⊢ (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U)
[PROOFSTEP]
rw [w]
[GOAL]
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
      toOpen (↑R) U ≫ NatTrans.app β.c (op U)
⊢ α = β
[PROOFSTEP]
ext : 1
[GOAL]
case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
      toOpen (↑R) U ≫ NatTrans.app β.c (op U)
⊢ α.base = β.base
[PROOFSTEP]
exact w
[GOAL]
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
      toOpen (↑R) U ≫ NatTrans.app β.c (op U)
⊢ α.c ≫
      whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
        X.presheaf =
    β.c
[PROOFSTEP]
apply ((TopCat.Sheaf.pushforward β.base).obj X.sheaf).hom_ext _ PrimeSpectrum.isBasis_basic_opens
[GOAL]
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
      toOpen (↑R) U ≫ NatTrans.app β.c (op U)
⊢ ∀ (i : ↑R),
    NatTrans.app
        (α.c ≫
          whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
            X.presheaf)
        (op (PrimeSpectrum.basicOpen i)) =
      NatTrans.app β.c (op (PrimeSpectrum.basicOpen i))
[PROOFSTEP]
intro r
[GOAL]
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
      toOpen (↑R) U ≫ NatTrans.app β.c (op U)
r : ↑R
⊢ NatTrans.app
      (α.c ≫
        whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
          X.presheaf)
      (op (PrimeSpectrum.basicOpen r)) =
    NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
[PROOFSTEP]
apply
  (StructureSheaf.to_basicOpen_epi R r).1
    -- Porting note : was a one-liner `simpa using h r`
[GOAL]
case h.a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
      toOpen (↑R) U ≫ NatTrans.app β.c (op U)
r : ↑R
⊢ toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app
        (α.c ≫
          whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
            X.presheaf)
        (op (PrimeSpectrum.basicOpen r)) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
[PROOFSTEP]
specialize h r
[GOAL]
case h.a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
r : ↑R
h :
  let U := PrimeSpectrum.basicOpen r;
  (toOpen (↑R) U ≫ NatTrans.app α.c (op U)) ≫
      X.presheaf.map
        (eqToHom
          (_ : (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U))) =
    toOpen (↑R) U ≫ NatTrans.app β.c (op U)
⊢ toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app
        (α.c ≫
          whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
            X.presheaf)
        (op (PrimeSpectrum.basicOpen r)) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
[PROOFSTEP]
simp only [sheafedSpaceObj_carrier, Functor.op_obj, unop_op, TopCat.Presheaf.pushforwardObj_obj,
  sheafedSpaceObj_presheaf, Category.assoc] at h
[GOAL]
case h.a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
r : ↑R
h :
  toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app α.c (op (PrimeSpectrum.basicOpen r)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op (PrimeSpectrum.basicOpen r)) =
                (TopologicalSpace.Opens.map β.base).op.obj (op (PrimeSpectrum.basicOpen r)))) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
⊢ toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app
        (α.c ≫
          whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
            X.presheaf)
        (op (PrimeSpectrum.basicOpen r)) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
[PROOFSTEP]
rw [NatTrans.comp_app, ← h]
[GOAL]
case h.a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
r : ↑R
h :
  toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app α.c (op (PrimeSpectrum.basicOpen r)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op (PrimeSpectrum.basicOpen r)) =
                (TopologicalSpace.Opens.map β.base).op.obj (op (PrimeSpectrum.basicOpen r)))) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
⊢ toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app α.c (op (PrimeSpectrum.basicOpen r)) ≫
        NatTrans.app
          (whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
            X.presheaf)
          (op (PrimeSpectrum.basicOpen r)) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app α.c (op (PrimeSpectrum.basicOpen r)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op (PrimeSpectrum.basicOpen r)) =
                (TopologicalSpace.Opens.map β.base).op.obj (op (PrimeSpectrum.basicOpen r))))
[PROOFSTEP]
congr
[GOAL]
case h.a.e_a.e_a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
r : ↑R
h :
  toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      NatTrans.app α.c (op (PrimeSpectrum.basicOpen r)) ≫
        X.presheaf.map
          (eqToHom
            (_ :
              (TopologicalSpace.Opens.map α.base).op.obj (op (PrimeSpectrum.basicOpen r)) =
                (TopologicalSpace.Opens.map β.base).op.obj (op (PrimeSpectrum.basicOpen r)))) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ NatTrans.app β.c (op (PrimeSpectrum.basicOpen r))
⊢ NatTrans.app
      (whiskerRight (eqToHom (_ : (TopologicalSpace.Opens.map α.base).op = (TopologicalSpace.Opens.map β.base).op))
        X.presheaf)
      (op (PrimeSpectrum.basicOpen r)) =
    X.presheaf.map
      (eqToHom
        (_ :
          (TopologicalSpace.Opens.map α.base).op.obj (op (PrimeSpectrum.basicOpen r)) =
            (TopologicalSpace.Opens.map β.base).op.obj (op (PrimeSpectrum.basicOpen r))))
[PROOFSTEP]
simp
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ toStalk (↑R) (↑(PrimeSpectrum.comap f) p) ≫ PresheafedSpace.stalkMap (Spec.sheafedSpaceMap f) p = f ≫ toStalk (↑S) p
[PROOFSTEP]
erw [← toOpen_germ S ⊤ ⟨p, trivial⟩, ← toOpen_germ R ⊤ ⟨PrimeSpectrum.comap f p, trivial⟩, Category.assoc,
  PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f) ⊤ ⟨p, trivial⟩, Spec.sheafedSpaceMap_c_app,
  toOpen_comp_comap_assoc]
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom f ≫
      toOpen (↑S) (↑(TopologicalSpace.Opens.comap (PrimeSpectrum.comap f)) ⊤) ≫
        TopCat.Presheaf.germ (Spec.sheafedSpaceObj S).toPresheafedSpace.presheaf { val := p, property := trivial } =
    f ≫ toOpen ↑S ⊤ ≫ TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (structureSheaf ↑S)) { val := p, property := trivial }
[PROOFSTEP]
rfl
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ ↑(((stalkIso (↑R) (↑(PrimeSpectrum.comap f) p)).inv ≫ PresheafedSpace.stalkMap (Spec.sheafedSpaceMap f) p) ≫
          (stalkIso (↑S) p).hom)
      (↑(algebraMap (↑R) (Localization.AtPrime (↑(PrimeSpectrum.comap f) p).asIdeal)) x) =
    ↑(algebraMap ((fun x => ↑S) x) (Localization.AtPrime p.asIdeal)) (↑f x)
[PROOFSTEP]
rw [stalkIso_hom, stalkIso_inv, comp_apply, comp_apply, localizationToStalk_of]
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
x : ↑R
⊢ ↑(stalkToFiberRingHom (↑S) p)
      (↑(PresheafedSpace.stalkMap (Spec.sheafedSpaceMap f) p) (↑(toStalk (↑R) (↑(PrimeSpectrum.comap f) p)) x)) =
    ↑(algebraMap ((fun x => ↑S) x) (Localization.AtPrime p.asIdeal)) (↑f x)
[PROOFSTEP]
erw [stalkMap_toStalk_apply f p x, stalkToFiberRingHom_toStalk]
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toSheafedSpace.toPresheafedSpace
a : ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p))
ha : IsUnit (↑(PresheafedSpace.stalkMap (sheafedSpaceMap f) p) a)
⊢ IsUnit a
[PROOFSTEP]
erw [← localRingHom_comp_stalkIso_apply] at ha
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toSheafedSpace.toPresheafedSpace
a : ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p))
ha :
  IsUnit
    (↑(localizationToStalk (↑S) p)
      (↑(Localization.localRingHom (↑(PrimeSpectrum.comap f) p).asIdeal p.asIdeal f
            (_ : (↑(PrimeSpectrum.comap f) p).asIdeal = (↑(PrimeSpectrum.comap f) p).asIdeal))
        (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a)))
⊢ IsUnit a
[PROOFSTEP]
replace ha := (stalkIso S p).hom.isUnit_map ha
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toSheafedSpace.toPresheafedSpace
a : ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p))
ha :
  IsUnit
    (↑(stalkIso (↑S) p).hom
      (↑(localizationToStalk (↑S) p)
        (↑(Localization.localRingHom (↑(PrimeSpectrum.comap f) p).asIdeal p.asIdeal f
              (_ : (↑(PrimeSpectrum.comap f) p).asIdeal = (↑(PrimeSpectrum.comap f) p).asIdeal))
          (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a))))
⊢ IsUnit a
[PROOFSTEP]
rw [← comp_apply, show localizationToStalk S p = (stalkIso S p).inv from rfl, Iso.inv_hom_id, id_apply] at ha
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toSheafedSpace.toPresheafedSpace
a : ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p))
ha :
  IsUnit
    (↑(Localization.localRingHom (↑(PrimeSpectrum.comap f) p).asIdeal p.asIdeal f
          (_ : (↑(PrimeSpectrum.comap f) p).asIdeal = (↑(PrimeSpectrum.comap f) p).asIdeal))
      (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a))
⊢ IsUnit a
[PROOFSTEP]
replace ha := IsLocalRingHom.map_nonunit (R := Localization.AtPrime (PrimeSpectrum.comap f p).asIdeal) _ ha
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toSheafedSpace.toPresheafedSpace
a : ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p))
ha : IsUnit (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a)
⊢ IsUnit a
[PROOFSTEP]
convert RingHom.isUnit_map (stalkIso R (PrimeSpectrum.comap f p)).inv ha
[GOAL]
case h.e'_3.h
R S : CommRingCat
f : R ⟶ S
p : ↑↑(locallyRingedSpaceObj S).toSheafedSpace.toPresheafedSpace
a : ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p))
ha : IsUnit (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a)
e_1✝ :
  ↑(PresheafedSpace.stalk (locallyRingedSpaceObj R).toSheafedSpace.toPresheafedSpace (↑(sheafedSpaceMap f).base p)) =
    (fun x => ↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf ↑R)) (↑(PrimeSpectrum.comap f) p)))
      (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a)
⊢ a = ↑(stalkIso (↑R) (↑(PrimeSpectrum.comap f) p)).inv (↑(stalkToFiberRingHom (↑R) (↑(PrimeSpectrum.comap f) p)) a)
[PROOFSTEP]
erw [← comp_apply, show stalkToFiberRingHom R _ = (stalkIso _ _).hom from rfl, Iso.hom_inv_id, id_apply]
[GOAL]
R : CommRingCat
⊢ (locallyRingedSpaceMap (𝟙 R)).val = (𝟙 (locallyRingedSpaceObj R)).val
[PROOFSTEP]
rw [Spec.locallyRingedSpaceMap_val, Spec.sheafedSpaceMap_id]
[GOAL]
R : CommRingCat
⊢ 𝟙 (sheafedSpaceObj R) = (𝟙 (locallyRingedSpaceObj R)).val
[PROOFSTEP]
rfl
[GOAL]
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (locallyRingedSpaceMap (f ≫ g)).val = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).val
[PROOFSTEP]
rw [Spec.locallyRingedSpaceMap_val, Spec.sheafedSpaceMap_comp]
[GOAL]
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ sheafedSpaceMap g ≫ sheafedSpaceMap f = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).val
[PROOFSTEP]
rfl
[GOAL]
R : CommRingCatᵒᵖ
⊢ { obj := fun R => locallyRingedSpaceObj R.unop, map := fun {X Y} f => locallyRingedSpaceMap f.unop }.map (𝟙 R) =
    𝟙 ({ obj := fun R => locallyRingedSpaceObj R.unop, map := fun {X Y} f => locallyRingedSpaceMap f.unop }.obj R)
[PROOFSTEP]
dsimp
[GOAL]
R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 R.unop) = 𝟙 (locallyRingedSpaceObj R.unop)
[PROOFSTEP]
rw [Spec.locallyRingedSpaceMap_id]
[GOAL]
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun R => locallyRingedSpaceObj R.unop, map := fun {X Y} f => locallyRingedSpaceMap f.unop }.map (f ≫ g) =
    { obj := fun R => locallyRingedSpaceObj R.unop, map := fun {X Y} f => locallyRingedSpaceMap f.unop }.map f ≫
      { obj := fun R => locallyRingedSpaceObj R.unop, map := fun {X Y} f => locallyRingedSpaceMap f.unop }.map g
[PROOFSTEP]
dsimp
[GOAL]
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
[PROOFSTEP]
rw [Spec.locallyRingedSpaceMap_comp]
[GOAL]
R : CommRingCat
⊢ IsIso (toSpecΓ R)
[PROOFSTEP]
cases R
[GOAL]
case mk
α✝ : Type ?u.412830
str✝ : CommRing α✝
⊢ IsIso (toSpecΓ (Bundled.mk α✝))
[PROOFSTEP]
apply StructureSheaf.isIso_to_global
[GOAL]
R S : CommRingCat
f : R ⟶ S
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op
[PROOFSTEP]
refine RingHom.ext fun x => Subtype.ext <| funext fun x' => ?_
[GOAL]
R S : CommRingCat
f : R ⟶ S
x : ↑R
x' : { x // x ∈ (op ⊤).unop }
⊢ ↑(↑(f ≫ toSpecΓ S) x) x' = ↑(↑(toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) x) x'
[PROOFSTEP]
symm
[GOAL]
R S : CommRingCat
f : R ⟶ S
x : ↑R
x' : { x // x ∈ (op ⊤).unop }
⊢ ↑(↑(toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) x) x' = ↑(↑(f ≫ toSpecΓ S) x) x'
[PROOFSTEP]
apply Localization.localRingHom_to_map
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
⊢ (𝟭 CommRingCat).map f ≫ ((fun R => asIso (toSpecΓ R)) Y).hom =
    ((fun R => asIso (toSpecΓ R)) X).hom ≫ (Spec.toLocallyRingedSpace.rightOp ⋙ Γ).map f
[PROOFSTEP]
exact Spec_Γ_naturality (R := X) (S := Y) f
[GOAL]
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (PresheafedSpace.stalkMap (Spec.toPresheafedSpace.map (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op) x)
[PROOFSTEP]
erw [← localRingHom_comp_stalkIso]
  -- Porting note: replaced `apply (config := { instances := false })`.
    -- See https://github.com/leanprover/lean4/issues/2273
[GOAL]
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    ((stalkIso (↑(op (CommRingCat.of ↑R)).unop)
          (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x)).hom ≫
      Localization.localRingHom
          (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal x.asIdeal
          (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop
          (_ :
            (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal =
              (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal) ≫
        (stalkIso (↑(op (CommRingCat.of (Localization M))).unop) x).inv)
[PROOFSTEP]
refine @IsIso.comp_isIso _ _ _ _ _ _ _ _ (?_)
[GOAL]
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (Localization.localRingHom
        (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal x.asIdeal
        (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop
        (_ :
          (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal =
            (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal) ≫
      (stalkIso (↑(op (CommRingCat.of (Localization M))).unop) x).inv)
[PROOFSTEP]
refine
  @IsIso.comp_isIso _ _ _ _ _ _ _ (?_)
    _
      /- I do not know why this is defeq to the goal, but I'm happy to accept that it is. -/
[GOAL]
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (Localization.localRingHom
      (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal x.asIdeal
      (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop
      (_ :
        (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal =
          (↑(PrimeSpectrum.comap (CommRingCat.ofHom (algebraMap (↑R) (Localization M))).op.unop) x).asIdeal))
[PROOFSTEP]
show IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom
[GOAL]
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (RingEquiv.toCommRingCatIso
        (AlgEquiv.toRingEquiv (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal))).hom
[PROOFSTEP]
infer_instance
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toStalk (↑R) p ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c
[PROOFSTEP]
rw [StructureSheaf.toStalk]
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    (toOpen ↑R ⊤ ≫
        TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (structureSheaf ↑R)) { val := p, property := True.intro }) ≫
      (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c
[PROOFSTEP]
erw [Category.assoc]
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toOpen ↑R ⊤ ≫
      TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (structureSheaf ↑R)) { val := p, property := True.intro } ≫
        (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap f).c
[PROOFSTEP]
rw [TopCat.Presheaf.stalkFunctor_map_germ]
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
⊢ f ≫ toPushforwardStalk f p =
    toOpen ↑R ⊤ ≫
      NatTrans.app (Spec.sheafedSpaceMap f).c (op ⊤) ≫
        TopCat.Presheaf.germ ((Spec.sheafedSpaceMap f).base _* (Spec.sheafedSpaceObj S).toPresheafedSpace.presheaf)
          { val := p, property := True.intro }
[PROOFSTEP]
exact Spec_Γ_naturality_assoc f _
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.germ_exist (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf S).val) _ y
[GOAL]
case intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hp }) s = y
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
obtain ⟨_, ⟨r, rfl⟩, hpr : p ∈ PrimeSpectrum.basicOpen r, hrU : PrimeSpectrum.basicOpen r ≤ U⟩ :=
  PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U from hp) U.2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hp }) s = y
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
change PrimeSpectrum.basicOpen r ≤ U at hrU
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hp }) s = y
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
replace e := ((Spec.topMap (algebraMap R S) _* (structureSheaf S).1).germ_res_apply (homOfLE hrU) ⟨p, hpr⟩ _).trans e
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s) =
    y
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
set s' := (Spec.topMap (algebraMap R S) _* (structureSheaf S).1).map (homOfLE hrU).op s with h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' : (forget CommRingCat).obj
  ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r))) :=
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
h : s' = ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
replace e : ((Spec.topMap (algebraMap R S) _* (structureSheaf S).val).germ ⟨p, hpr⟩) s' = y
[GOAL]
case e
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' : (forget CommRingCat).obj
  ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r))) :=
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
h : s' = ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
[PROOFSTEP]
rw [h]
[GOAL]
case e
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' : (forget CommRingCat).obj
  ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r))) :=
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
h : s' = ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s) =
    y
[PROOFSTEP]
exact e
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' : (forget CommRingCat).obj
  ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r))) :=
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
h : s' = ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
clear_value s'
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hp : p ∈ U
s : (forget CommRingCat).obj ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op U))
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
hrU : PrimeSpectrum.basicOpen r ≤ U
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
h : s' = ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op) s
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
clear! U
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
obtain ⟨⟨s, ⟨_, n, rfl⟩⟩, hsn⟩ :=
  @IsLocalization.surj _ _ _ _ _ _ (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) s'
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
refine' ⟨⟨s, ⟨r, hpr⟩ ^ n⟩, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ (s, { val := r, property := hpr } ^ n).snd • y =
    ↑(toPushforwardStalkAlgHom R S p) (s, { val := r, property := hpr } ^ n).fst
[PROOFSTEP]
rw [Submonoid.smul_def, Algebra.smul_def, algebraMap_pushforward_stalk, toPushforwardStalk, comp_apply, comp_apply]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := trivial })
        (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd)) *
      y =
    ↑(toPushforwardStalkAlgHom R S p) (s, { val := r, property := hpr } ^ n).fst
[PROOFSTEP]
iterate 2 erw [← (Spec.topMap (algebraMap R S) _* (structureSheaf S).1).germ_res_apply (homOfLE le_top) ⟨p, hpr⟩]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := trivial })
        (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd)) *
      y =
    ↑(toPushforwardStalkAlgHom R S p) (s, { val := r, property := hpr } ^ n).fst
[PROOFSTEP]
erw [← (Spec.topMap (algebraMap R S) _* (structureSheaf S).1).germ_res_apply (homOfLE le_top) ⟨p, hpr⟩]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
        (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) *
      y =
    ↑(toPushforwardStalkAlgHom R S p) (s, { val := r, property := hpr } ^ n).fst
[PROOFSTEP]
erw [← (Spec.topMap (algebraMap R S) _* (structureSheaf S).1).germ_res_apply (homOfLE le_top) ⟨p, hpr⟩]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
        (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) *
      y =
    ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
rw [← e]
  -- Porting note : without this `change`, Lean doesn't know how to rewrite `map_mul`
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
        (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) *
      ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
        s' =
    ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
let f := TopCat.Presheaf.germ (Spec.topMap (algebraMap R S) _* (structureSheaf S).val) ⟨p, hpr⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f✝ : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
f : (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶
  TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) ↑{ val := p, property := hpr } :=
  TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }
⊢ ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
        (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) *
      ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
        s' =
    ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr })
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
change f _ * f _ = f _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f✝ : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
f : (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶
  TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) ↑{ val := p, property := hpr } :=
  TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }
⊢ ↑f
        (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) *
      ↑f s' =
    ↑f
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
rw [← map_mul, mul_comm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f✝ : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        ↑(s,
              { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
                property :=
                  (_ :
                    ∃ y,
                      (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                        (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).snd =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
      (s,
          { val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
            property :=
              (_ :
                ∃ y,
                  (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y =
                    (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) }).fst
f : (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶
  TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) ↑{ val := p, property := hpr } :=
  TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }
⊢ ↑f
      (s' *
        ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) =
    ↑f
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
dsimp only [Subtype.coe_mk] at hsn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f✝ : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        (↑(algebraMap ↑R ↑S) r ^ n) =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) s
f : (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶
  TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) ↑{ val := p, property := hpr } :=
  TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }
⊢ ↑f
      (s' *
        ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) =
    ↑f
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
rw [← map_pow (algebraMap R S)] at hsn
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.mk.mk.intro
R S : CommRingCat
f✝ : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)
r : ↑R
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  (forget CommRingCat).obj
    ((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)))
e :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }) s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r)))))
        (↑(algebraMap ↑R ↑S) (r ^ n)) =
    ↑(algebraMap ↑S ↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) s
f : (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).obj (op (PrimeSpectrum.basicOpen r)) ⟶
  TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) ↑{ val := p, property := hpr } :=
  TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := hpr }
⊢ ↑f
      (s' *
        ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
              (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
          (↑(toOpen ↑S ⊤) (↑(algebraMap ↑R ↑S) ↑(s, { val := r, property := hpr } ^ n).snd))) =
    ↑f
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map
            (homOfLE (_ : PrimeSpectrum.basicOpen r ≤ ⊤)).op)
        (↑(toOpen ↑S ⊤) (s, { val := r, property := hpr } ^ n).fst))
[PROOFSTEP]
congr 1
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ IsLocalizedModule (Ideal.primeCompl p.asIdeal) (AlgHom.toLinearMap (toPushforwardStalkAlgHom R S p))
[PROOFSTEP]
apply IsLocalizedModule.mkOfAlgebra
[GOAL]
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑R),
    x ∈ Ideal.primeCompl p.asIdeal →
      IsUnit (↑(algebraMap ↑R ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)) x)
[PROOFSTEP]
intro x hx
[GOAL]
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ Ideal.primeCompl p.asIdeal
⊢ IsUnit (↑(algebraMap ↑R ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)) x)
[PROOFSTEP]
rw [algebraMap_pushforward_stalk, toPushforwardStalk_comp]
[GOAL]
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ Ideal.primeCompl p.asIdeal
⊢ IsUnit
    (↑(toStalk (↑R) p ≫ (TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap (algebraMap ↑R ↑S)).c) x)
[PROOFSTEP]
change IsUnit ((TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap (algebraMap ↑R ↑S)).c _)
[GOAL]
case h₁
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑R
hx : x ∈ Ideal.primeCompl p.asIdeal
⊢ IsUnit
    (↑((TopCat.Presheaf.stalkFunctor CommRingCat p).map (Spec.sheafedSpaceMap (algebraMap ↑R ↑S)).c)
      (↑(toStalk (↑R) p) x))
[PROOFSTEP]
exact (IsLocalization.map_units ((structureSheaf R).presheaf.stalk p) ⟨x, hx⟩).map _
[GOAL]
case h₂
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (y : ↑(TopCat.Presheaf.stalk (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) p)),
    ∃ x, x.snd • y = ↑(toPushforwardStalkAlgHom R S p) x.fst
[PROOFSTEP]
apply isLocalizedModule_toPushforwardStalkAlgHom_aux
[GOAL]
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
⊢ ∀ (x : ↑S), ↑(toPushforwardStalkAlgHom R S p) x = 0 → ∃ m, m • x = 0
[PROOFSTEP]
intro x hx
[GOAL]
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx : ↑(toPushforwardStalkAlgHom R S p) x = 0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
rw [toPushforwardStalkAlgHom_apply, ← (toPushforwardStalk (algebraMap R S) p).map_zero, toPushforwardStalk] at hx
[GOAL]
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    ↑(toOpen ↑S ⊤ ≫
          TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
            { val := p, property := trivial })
      0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
change
  _ =
    (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
      (⟨p, trivial⟩ : (⊤ : TopologicalSpace.Opens (PrimeSpectrum R))) (toOpen S ⊤ 0)) at
  hx
[GOAL]
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
          { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) 0)
⊢ ∃ m, m • x = 0
[PROOFSTEP]
rw [map_zero] at hx
[GOAL]
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val) { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    ↑(TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
          { val := p, property := trivial })
      0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
change (forget CommRingCat).map _ _ = (forget _).map _ _ at hx
[GOAL]
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq _ _ _ _ _ _ hx
[GOAL]
case h₃.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
e :
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₁.op) (↑(toOpen ↑S ⊤) x) =
    ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₂.op) 0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
  PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU) U.2
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
e :
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₁.op) (↑(toOpen ↑S ⊤) x) =
    ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₂.op) 0
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : (fun r => ↑(PrimeSpectrum.basicOpen r)) r ⊆ U.carrier
⊢ ∃ m, m • x = 0
[PROOFSTEP]
change PrimeSpectrum.basicOpen r ≤ U at hrU
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
e :
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₁.op) (↑(toOpen ↑S ⊤) x) =
    ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₂.op) 0
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
⊢ ∃ m, m • x = 0
[PROOFSTEP]
apply_fun (Spec.topMap (algebraMap R S) _* (structureSheaf S).1).map (homOfLE hrU).op at e
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op)
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₁.op) (↑(toOpen ↑S ⊤) x)) =
    ↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map (homOfLE hrU).op)
      (↑((Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val).map i₂.op) 0)
⊢ ∃ m, m • x = 0
[PROOFSTEP]
simp only [TopCat.Presheaf.pushforwardObj_map, Functor.op_map, map_zero, ← comp_apply, toOpen_res] at e
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
⊢ ∃ m, m • x = 0
[PROOFSTEP]
have : toOpen S (PrimeSpectrum.basicOpen <| algebraMap R S r) x = 0 := by refine' Eq.trans _ e; rfl
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
⊢ ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
[PROOFSTEP]
refine' Eq.trans _ e
[GOAL]
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
⊢ ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x))
[PROOFSTEP]
rfl
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
have :=
  (@IsLocalization.mk'_one _ _ _ _ _ _ (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans this
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this✝ : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
this :
  IsLocalization.mk' (↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) x 1 = 0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
obtain ⟨⟨_, n, rfl⟩, e⟩ := (IsLocalization.mk'_eq_zero_iff _ _).mp this
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e✝ :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this✝ : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
this :
  IsLocalization.mk' (↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) x 1 = 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
          property :=
            (_ :
              ∃ y,
                (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y = (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) } *
      x =
    0
⊢ ∃ m, m • x = 0
[PROOFSTEP]
refine' ⟨⟨r, hpr⟩ ^ n, _⟩
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e✝ :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this✝ : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
this :
  IsLocalization.mk' (↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) x 1 = 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
          property :=
            (_ :
              ∃ y,
                (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y = (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) } *
      x =
    0
⊢ { val := r, property := hpr } ^ n • x = 0
[PROOFSTEP]
rw [Submonoid.smul_def, Algebra.smul_def]
  -- Porting note : manually rewrite `Submonoid.coe_pow`
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e✝ :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this✝ : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
this :
  IsLocalization.mk' (↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) x 1 = 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
          property :=
            (_ :
              ∃ y,
                (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y = (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) } *
      x =
    0
⊢ ↑(algebraMap ↑R ↑S) ↑({ val := r, property := hpr } ^ n) * x = 0
[PROOFSTEP]
change (algebraMap R S) (r ^ n) * x = 0
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e✝ :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this✝ : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
this :
  IsLocalization.mk' (↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) x 1 = 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
          property :=
            (_ :
              ∃ y,
                (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y = (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) } *
      x =
    0
⊢ ↑(algebraMap ↑R ↑S) (r ^ n) * x = 0
[PROOFSTEP]
rw [map_pow]
[GOAL]
case h₃.intro.intro.intro.intro.intro.intro.intro.intro.intro.mk.intro
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      (↑(toOpen ↑S ⊤) x) =
    (forget CommRingCat).map
      (TopCat.Presheaf.germ (Spec.topMap (algebraMap ↑R ↑S) _* (structureSheaf ↑S).val)
        { val := p, property := trivial })
      0
U : TopologicalSpace.Opens ↑(Spec.topObj R)
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑R
hpr : p ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) r
hrU : PrimeSpectrum.basicOpen r ≤ U
e✝ :
  ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₁.op.unop).op)
        (↑(toOpen ↑S ⊤) x)) =
    ↑((structureSheaf ↑S).val.map
          ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map (homOfLE hrU).op.unop).op)
      (↑((structureSheaf ↑S).val.map ((TopologicalSpace.Opens.map (Spec.topMap (algebraMap ↑R ↑S))).map i₂.op.unop).op)
        0)
this✝ : ↑(toOpen (↑S) (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))) x = 0
this :
  IsLocalization.mk' (↑((structureSheaf ↑S).val.obj (op (PrimeSpectrum.basicOpen (↑(algebraMap ↑R ↑S) r))))) x 1 = 0
n : ℕ
e :
  ↑{ val := (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n,
          property :=
            (_ :
              ∃ y,
                (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) y = (fun x x_1 => x ^ x_1) (↑(algebraMap ↑R ↑S) r) n) } *
      x =
    0
⊢ ↑(algebraMap ↑R ↑S) r ^ n * x = 0
[PROOFSTEP]
exact e


[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB (↑f '' s) x
⊢ ∀ {x y : α}, ↑f x ≤ ↑f y ↔ x ≤ y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB s (↑(symm f) x)
⊢ ∀ {x y : β}, ↑(symm f) x ≤ ↑(symm f) y ↔ x ≤ y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB (↑f '' s) (↑f x) ↔ IsLUB s x
[PROOFSTEP]
rw [isLUB_image, f.symm_apply_apply]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB (↑f ⁻¹' s) x ↔ IsLUB s (↑f x)
[PROOFSTEP]
rw [← f.symm_symm, ← image_eq_preimage, isLUB_image]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB (↑f ⁻¹' s) (↑(symm f) x) ↔ IsLUB s x
[PROOFSTEP]
rw [isLUB_preimage, f.apply_symm_apply]


[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsProper IF.I
[PROOFSTEP]
cases' IF.F.nonempty with w h
[GOAL]
case intro
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ IsProper IF.I
[PROOFSTEP]
apply isProper_of_not_mem (_ : w ∉ IF.I)
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ ¬w ∈ IF.I
[PROOFSTEP]
rwa [← IF.compl_I_eq_F] at h
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter (↑IF.I)ᶜ
[PROOFSTEP]
rw [IF.compl_I_eq_F]
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
src✝ : IsProper IF.I := I_isProper IF
⊢ IsPFilter ↑IF.F
[PROOFSTEP]
exact IF.F.isPFilter
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
contrapose!
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
[PROOFSTEP]
let F := hI.compl_filter.toPFilter
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑I)ᶜ)
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
[PROOFSTEP]
show x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
[GOAL]
P : Type u_1
inst✝ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
hI : IsPrime I
x y : P
F : PFilter P := IsPFilter.toPFilter (_ : IsPFilter (↑I)ᶜ)
⊢ x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
[PROOFSTEP]
exact fun h => inf_mem h.1 h.2
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPrime I
[PROOFSTEP]
rw [IsPrime_iff]
[GOAL]
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsProper I ∧ IsPFilter (↑I)ᶜ
[PROOFSTEP]
use‹_›
[GOAL]
case right
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑I)ᶜ
[PROOFSTEP]
refine .of_def ?_ ?_ ?_
[GOAL]
case right.refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ Set.Nonempty (↑I)ᶜ
[PROOFSTEP]
exact Set.nonempty_compl.2 (I.IsProper_iff.1 ‹_›)
[GOAL]
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x x_1 => x ≥ x_1) (↑I)ᶜ
[PROOFSTEP]
intro x hx y hy
[GOAL]
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
x✝ y✝ : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
x : P
hx : x ∈ (↑I)ᶜ
y : P
hy : y ∈ (↑I)ᶜ
⊢ ∃ z, z ∈ (↑I)ᶜ ∧ (fun x x_1 => x ≥ x_1) x z ∧ (fun x x_1 => x ≥ x_1) y z
[PROOFSTEP]
exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩
[GOAL]
case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
x y : P
I : Ideal P
inst✝ : IsProper I
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
[PROOFSTEP]
exact @mem_compl_of_ge _ _ _
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
⊢ IsPrime I
[PROOFSTEP]
rw [isPrime_iff_mem_or_mem]
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
intro x y
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
contrapose!
[GOAL]
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
⊢ ¬x ∈ I ∧ ¬y ∈ I → ¬x ⊓ y ∈ I
[PROOFSTEP]
rintro ⟨hx, hynI⟩ hxy
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
⊢ False
[PROOFSTEP]
apply hynI
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
⊢ y ∈ I
[PROOFSTEP]
let J := I ⊔ principal x
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
⊢ y ∈ I
[PROOFSTEP]
have hJuniv : (J : Set P) = Set.univ := IsMaximal.maximal_proper (lt_sup_principal_of_not_mem ‹_›)
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
⊢ y ∈ I
[PROOFSTEP]
have hyJ : y ∈ ↑J := Set.eq_univ_iff_forall.mp hJuniv y
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ ↑J
⊢ y ∈ I
[PROOFSTEP]
rw [coe_sup_eq] at hyJ
[GOAL]
case intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
hyJ : y ∈ {x_1 | ∃ i, i ∈ I ∧ ∃ j, j ∈ principal x ∧ x_1 = i ⊔ j}
⊢ y ∈ I
[PROOFSTEP]
rcases hyJ with ⟨a, ha, b, hb, hy⟩
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ y ∈ I
[PROOFSTEP]
rw [hy]
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ a ⊔ b ∈ I
[PROOFSTEP]
refine' sup_mem ha (I.lower (le_inf hb _) hxy)
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ y
[PROOFSTEP]
rw [hy]
[GOAL]
case intro.intro.intro.intro.intro
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : IsMaximal I
x y : P
hx : ¬x ∈ I
hynI : ¬y ∈ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ a ⊔ b
[PROOFSTEP]
exact le_sup_right
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ∈ I ∨ xᶜ ∈ I
[PROOFSTEP]
apply hI.mem_or_mem
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ x ⊓ xᶜ ∈ I
[PROOFSTEP]
rw [inf_compl_eq_bot]
[GOAL]
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : IsPrime I
⊢ ⊥ ∈ I
[PROOFSTEP]
exact I.bot_mem
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ IsPrime I
[PROOFSTEP]
simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → ¬x ∈ I → y ∈ I
[PROOFSTEP]
intro x y hxy hxI
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
⊢ y ∈ I
[PROOFSTEP]
have hxcI : xᶜ ∈ I := h.resolve_left hxI
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
[PROOFSTEP]
have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsProper I
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : ¬x ∈ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I
[PROOFSTEP]
rwa [inf_comm, sup_inf_inf_compl] at ass
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsPrime I
⊢ IsMaximal I
[PROOFSTEP]
simp only [IsMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : IsPrime I
⊢ ∀ ⦃J : Ideal P⦄, I < J → ∀ (x : P), x ∈ ↑J
[PROOFSTEP]
intro J hIJ x
[GOAL]
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x : P
⊢ x ∈ ↑J
[PROOFSTEP]
rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
[GOAL]
case intro.intro
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : ¬y ∈ ↑I
⊢ x ∈ ↑J
[PROOFSTEP]
suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
[GOAL]
case intro.intro
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : ¬y ∈ ↑I
ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
⊢ x ∈ ↑J
[PROOFSTEP]
rwa [sup_inf_inf_compl] at ass
[GOAL]
case ass
P : Type u_1
inst✝¹ : BooleanAlgebra P
x✝ : P
I : Ideal P
inst✝ : IsPrime I
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ ↑J
hyI : ¬y ∈ ↑I
⊢ x ⊓ y ⊔ x ⊓ yᶜ ∈ J
[PROOFSTEP]
exact sup_mem (J.lower inf_le_right hyJ) (hIJ.le <| I.lower inf_le_right <| IsPrime.mem_compl_of_not_mem ‹_› hyI)
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.F)ᶜ
[PROOFSTEP]
rw [IF.compl_F_eq_I]
[GOAL]
P : Type u_1
inst✝ : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal ↑IF.I
[PROOFSTEP]
exact IF.I.isIdeal