R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    (CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ toBasicOpen R 1) ≫
      (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫
      toBasicOpen R 1 ≫ (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
rw [← Category.assoc]
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    CommRingCat.ofHom (RingHom.comp (toBasicOpen R 1) (algebraMap R (Localization.Away 1))) ≫
      (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    (CommRingCat.ofHom (algebraMap R (Localization.Away 1)) ≫ toBasicOpen R 1) ≫
      (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
change toOpen R ⊤ =
  (CommRingCat.ofHom <| (toBasicOpen R 1).comp (algebraMap R (Localization.Away 1))) ≫
  (structureSheaf R).1.map (eqToHom _).op
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    RingHom.comp (toBasicOpen R 1) (algebraMap R (Localization.Away 1)) ≫
      (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    CommRingCat.ofHom (RingHom.comp (toBasicOpen R 1) (algebraMap R (Localization.Away 1))) ≫
      (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
unfold CommRingCat.ofHom
no goals
R : Type u
inst✝ : CommRing R
⊢ toOpen R ⊤ =
    RingHom.comp (toBasicOpen R 1) (algebraMap R (Localization.Away 1)) ≫
      (structureSheaf R).val.map (eqToHom (_ : ⊤ = PrimeSpectrum.basicOpen 1)).op
rw [localization_toBasicOpen R, toOpen_res]