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 ⟶ ⊤
e :
  (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
          i₂.op))
      0
⊢ ∃ m, m • x = 0

Tactic:
obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
      PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU)
        U.2

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 ⟶ ⊤
e :
  (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
          i₂.op))
      0
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r
hrU : (fun r ↦ ↑(PrimeSpectrum.basicOpen r)) r ⊆ U.carrier
⊢ ∃ m, m • x = 0