Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
          ⊤ p trivial))
      0
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r
hrU : (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r ⊆ U.carrier
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            i₁.op))
        ((CommRingCat.ofHom
              (algebraMap (↑S)
                ((structureSheafInType ↑S ↑S).obj.obj
                  (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
          x)) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            i₂.op))
        0)
this :
  (algebraMap ↑S
        ↑((structureSheaf ↑S).presheaf.obj
            ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj
              (op { carrier := {x | r ∉ x.asIdeal}, is_open' := ⋯ }))))
      x =
    0
⊢ ∃ m, m • x = 0

Tactic:
have :=
      (@IsLocalization.mk'_one _ _ _ _ _ _
            (StructureSheaf.IsLocalization.to_basicOpen S <| algebraMap R S r) x).trans
        this

Goal state after:
case h₃
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
x : ↑S
hx :
  (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          ⊤ p trivial).hom'
      ((CommRingCat.ofHom
            (algebraMap (↑S)
              ((structureSheafInType ↑S ↑S).obj.obj
                (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
        x) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑(CommRingCat.of ↑S)).obj).germ
          ⊤ p trivial))
      0
U : TopologicalSpace.Opens ↑(Spec.topObj (CommRingCat.of ↑R))
hpU : p ∈ U
i₁ : U ⟶ ⊤
i₂ : U ⟶ ⊤
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r
hrU : (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r ⊆ U.carrier
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            i₁.op))
        ((CommRingCat.ofHom
              (algebraMap (↑S)
                ((structureSheafInType ↑S ↑S).obj.obj
                  (op ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj ⊤))))).hom'
          x)) =
    (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).map
          (homOfLE hrU).op))
      ((ConcreteCategory.hom
          (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
                (structureSheaf ↑S).obj).map
            i₂.op))
        0)
this✝ :
  (algebraMap ↑S
        ↑((structureSheaf ↑S).presheaf.obj
            ((TopologicalSpace.Opens.map (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).op.obj
              (op { carrier := {x | r ∉ x.asIdeal}, is_open' := ⋯ }))))
      x =
    0
this : IsLocalization.mk' (↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r))))) x 1 = 0
⊢ ∃ m, m • x = 0