awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
rw : (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom
⊢ (locallyRingedSpaceMap (f ≫ g)).toHom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom

Tactic:
rw [Spec.locallyRingedSpaceMap_toHom, Spec.sheafedSpaceMap_comp]

Premises used: AlgebraicGeometry.Spec.sheafedSpaceMap_comp, AlgebraicGeometry.Spec.locallyRingedSpaceMap_toHom
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom = (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f).toHom

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCatᵒᵖ
rw rw₁ : 𝟙 (locallyRingedSpaceObj (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
⊢ locallyRingedSpaceMap (𝟙 (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))

Tactic:
rw [Spec.locallyRingedSpaceMap_id]

Premises used: AlgebraicGeometry.Spec.locallyRingedSpaceMap_id
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X Y Z : CommRingCatᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
rw rw₁ :
  locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop =
    locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
⊢ locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop

Tactic:
rw [Spec.locallyRingedSpaceMap_comp]

Premises used: AlgebraicGeometry.Spec.locallyRingedSpaceMap_comp
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
⊢ IsIso (toSpecΓ R)

Tactic:
(ConcreteCategory.isIso_iff_bijective _).mpr algebraMap_obj_top_bijective

Premises used: Iff.mpr, AlgebraicGeometry.StructureSheaf.algebraMap_obj_top_bijective, CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
hf :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
      ((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
            (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
          x :
        (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
      ((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
            (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
          x :
        (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
⊢ f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Tactic:
ext : 2
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
⊢ Eq (α := (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))

Tactic:
Subtype.ext <| funext fun x' => ?_

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
hf :
  ∀ (x' : ↥(unop (op ⊤))),
    Eq.{u + 1} (α :=
      Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
                (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
              x) :
          (x : ↥(unop (op ⊤))) →
            Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
        x')
      ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
                (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
              x) :
          (x : ↥(unop (op ⊤))) →
            Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
        x')
⊢ Eq (α := (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
    ((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
          (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
        x :
      (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))

Tactic:
refine Subtype.ext <| funext fun x' => ?_

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
x' : ↥(unop (op ⊤))
hf :
  Eq.{u + 1} (α :=
    Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
⊢ Eq.{u + 1} (α :=
    Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
    ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
x' : ↥(unop (op ⊤))
hf :
  Eq (α := Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((Localization.localRingHom
          (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
              (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u))).asIdeal
          (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)).asIdeal (CommRingCat.Hom.hom f.op.unop) ⋯ :
        (a :
            Localization.AtPrime
              (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
                  (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u))).asIdeal) →
          Localization.AtPrime (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)).asIdeal)
      ((↑(((toSpecΓ R).hom' : (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op R)))) : Type u))
              x) :
          (x : ↥(unop (op (unop (op ⊤))))) →
            Localizations (↑(unop (op R)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u)) ↦
          Membership.mem (γ := TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u))
            (unop (op (unop (op ⊤)))) x)
          (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
            (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
          ⋯)))
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
⊢ Eq.{u + 1} (α :=
    Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((↑((CommRingCat.Hom.hom (toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')

Tactic:
erw [comap_apply]

Premises used: AlgebraicGeometry.StructureSheaf.comap_apply
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R S : CommRingCat
f : R ⟶ S
x : (↑R : Type u)
x' : ↥(unop (op ⊤))
⊢ Eq (α := Localizations (↑(unop (op S)) : Type u) (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
    ((Localization.localRingHom
          (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
              (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u))).asIdeal
          (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)).asIdeal (CommRingCat.Hom.hom f.op.unop) ⋯ :
        (a :
            Localization.AtPrime
              (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
                  (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u))).asIdeal) →
          Localization.AtPrime (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)).asIdeal)
      ((↑(((toSpecΓ R).hom' : (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op R)))) : Type u))
              x) :
          (x : ↥(unop (op (unop (op ⊤))))) →
            Localizations (↑(unop (op R)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u)))
        (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u)) ↦
          Membership.mem (γ := TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑(unop (op R)) : Type u)) : Type u))
            (unop (op (unop (op ⊤)))) x)
          (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop)
            (↑x' : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
          ⋯)))
    ((↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S) :
              (a : (↑R : Type u)) → (↑(Γ.obj (op (Spec.toLocallyRingedSpace.obj (op S)))) : Type u))
            x) :
        (x : ↥(unop (op ⊤))) →
          Localizations (↑(unop (op S)) : Type u) (↑x : (↑(PrimeSpectrum.Top (↑(unop (op S)) : Type u)) : Type u)))
      x')

Tactic:
apply Localization.localRingHom_to_map

Premises used: Localization.localRingHom_to_map
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X Y : CommRingCat
f : X ⟶ Y
⊢ f ≫ toSpecΓ Y = toSpecΓ X ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op

Tactic:
Spec_Γ_naturality (R := X) (S := Y) f

Premises used: AlgebraicGeometry.Spec_Γ_naturality
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
X Y : CommRingCat
f : X ⟶ Y
⊢ Eq (α := Functor.obj (𝟭 CommRingCat) X ⟶ (Spec.toLocallyRingedSpace.rightOp ⋙ Γ).obj Y)
    (CategoryTheory.Functor.map (𝟭 CommRingCat) f ≫ Iso.hom ((fun (R : CommRingCat.{u}) ↦ asIso (toSpecΓ R)) Y))
    (Iso.hom ((fun (R : CommRingCat.{u}) ↦ asIso (toSpecΓ R)) X) ≫ (Spec.toLocallyRingedSpace.rightOp ⋙ Γ).map f)

Tactic:
convert! Spec_Γ_naturality (R := X) (S := Y) f

Premises used: AlgebraicGeometry.Spec_Γ_naturality
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
dsimp :
  IsIso.{u, u + 1} (X :=
    (Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat)) (Y :=
            (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat))
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))) :
          (a : (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat) : Type u)) →
            (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat) : Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      (InducedCategory.Hom.hom (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))
      x)
⊢ IsIso (X :=
    (Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat)) (Y :=
            (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat))
            (PresheafedSpace.Hom.base
              (Spec.toPresheafedSpace.map
                (Quiver.Hom.op (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))) :
          (a : (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat) : Type u)) →
            (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat) : Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      (Spec.toPresheafedSpace.map (Quiver.Hom.op (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M))))) x)

Tactic:
dsimp only [Spec.toPresheafedSpace_map, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, AlgebraicGeometry.Spec.toPresheafedSpace_map
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsIso.{u, u + 1} (X :=
    (Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat)) (Y :=
            (↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat))
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))) :
          (a : (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (Localization M)))) : TopCat) : Type u)) →
            (↑(↑(Spec.toPresheafedSpace.obj (op (CommRingCat.of (↑R : Type u)))) : TopCat) : Type u))
        x))
    (PresheafedSpace.Hom.stalkMap
      (InducedCategory.Hom.hom (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))))
      x)

Tactic:
rw [← localRingHom_comp_stalkIso, ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective, AlgebraicGeometry.localRingHom_comp_stalkIso
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
dsimp :
  Function.Bijective (α :=
    (↑(TopCat.Presheaf.stalk (X := Spec.topObj (CommRingCat.of (↑R : Type u)))
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
            (structureSheaf (↑R : Type u)))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := Spec.topObj (CommRingCat.of (Localization M))) (Y := Spec.topObj (CommRingCat.of (↑R : Type u)))
                (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))) :
              (a : PrimeSpectrum (Localization M)) → PrimeSpectrum (↑R : Type u))
            x)) :
      Type u))
    (β :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (Localization M)) : Type u)))
            (structureSheaf (Localization M)))
          x) :
      Type u))
    (Function.comp (β :=
      Localization.AtPrime
        (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
      (Function.comp (β := Localization.AtPrime x.asIdeal)
        (⇑(↑(stalkIso (Localization M) x) :
              Localization.AtPrime x.asIdeal →+*
                (↑((structurePresheafInCommRingCat (Localization M)).stalk x) : Type u)) :
          (a : Localization.AtPrime x.asIdeal) →
            (↑(TopCat.Presheaf.stalk (structureSheaf (Localization M)).obj x) : Type u))
        (⇑(Localization.localRingHom
              (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M))
                x.asIdeal)
              x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
          (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
            Localization.AtPrime x.asIdeal))
      (⇑(AlgEquiv.symm (stalkIso (↑R : Type u) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (Localization M)) x))) :
        (a :
            (↑(TopCat.Presheaf.stalk (structureSheaf (↑R : Type u)).obj
                  ((ConcreteCategory.hom (Spec.topMap (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization M)))) :
                      (a : PrimeSpectrum (Localization M)) → PrimeSpectrum (↑R : Type u))
                    x)) :
              Type u)) →
          Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective (α :=
    Localization.AtPrime
      (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
    (β :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (Localization M)) : Type u)))
            (structureSheaf (Localization M)))
          x) :
      Type u))
    (Function.comp (β := Localization.AtPrime x.asIdeal)
      (⇑(↑(stalkIso (Localization M) x) :
            Localization.AtPrime x.asIdeal →+*
              (↑((structurePresheafInCommRingCat (Localization M)).stalk x) : Type u)) :
        (a : Localization.AtPrime x.asIdeal) →
          (↑(TopCat.Presheaf.stalk (structureSheaf (Localization M)).obj x) : Type u))
      (⇑(Localization.localRingHom
            (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
            x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
        (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
          Localization.AtPrime x.asIdeal))

Tactic:
(stalkIso (Localization M) x).bijective.comp ?_

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, OreLocalization, setOf, Localization, AlgebraicGeometry.StructureSheaf.stalkIso, Quotient, Function.Bijective.comp, AlgebraicGeometry.structurePresheafInCommRingCat, AlgEquiv.bijective
-- Module: Mathlib.AlgebraicGeometry.Spec
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u)
x : PrimeSpectrum (Localization M)
refine :
  Function.Bijective (α :=
    Localization.AtPrime
      (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
    (β := Localization.AtPrime x.asIdeal)
    (⇑(Localization.localRingHom
          (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
          x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
      (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
        Localization.AtPrime x.asIdeal)
⊢ Function.Bijective (α :=
    Localization.AtPrime
      (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal))
    (β :=
    (↑(TopCat.Presheaf.stalk
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (Localization M)) : Type u)))
            (structureSheaf (Localization M)))
          x) :
      Type u))
    (Function.comp (β := Localization.AtPrime x.asIdeal)
      (⇑(↑(stalkIso (Localization M) x) :
            Localization.AtPrime x.asIdeal →+*
              (↑((structurePresheafInCommRingCat (Localization M)).stalk x) : Type u)) :
        (a : Localization.AtPrime x.asIdeal) →
          (↑(TopCat.Presheaf.stalk (structureSheaf (Localization M)).obj x) : Type u))
      (⇑(Localization.localRingHom
            (Ideal.comap (F := (↑R : Type u) →+* Localization M) (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)
            x.asIdeal (algebraMap (↑R : Type u) (Localization M)) ⋯) :
        (a : Localization.AtPrime (Ideal.comap (algebraMap (↑R : Type u) (Localization M)) x.asIdeal)) →
          Localization.AtPrime x.asIdeal))

Tactic:
refine (stalkIso (Localization M) x).bijective.comp ?_

Premises used: Localization, AlgebraicGeometry.StructureSheaf.stalkIso, Function.Bijective.comp, AlgEquiv.bijective