case intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
f : (x : { x // x ∈ U }) → Localizations R ↑x
r s : R
h :
  ∀ (x : { x // x ∈ U }),
    ¬s ∈ (↑x).asIdeal ∧ f x * ↑(algebraMap R (Localizations R ↑x)) s = ↑(algebraMap R (Localizations R ↑x)) r
⊢ ∃ r s,
    ∀ (x : { x // x ∈ U }),
      ∃ hs, f x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) r { val := s, property := hs }
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
f : (x : { x // x ∈ U }) → Localizations R ↑x
hf : IsFraction f
⊢ ∃ r s,
    ∀ (x : { x // x ∈ U }),
      ∃ hs, f x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) r { val := s, property := hs }
rcases hf with ⟨r, s, h⟩
case intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
f : (x : { x // x ∈ U }) → Localizations R ↑x
r s : R
h :
  ∀ (x : { x // x ∈ U }),
    ¬s ∈ (↑x).asIdeal ∧ f x * ↑(algebraMap R (Localizations R ↑x)) s = ↑(algebraMap R (Localizations R ↑x)) r
x : { x // x ∈ U }
⊢ ↑(algebraMap R (Localizations R ↑x)) r =
    f x * ↑(algebraMap R (Localizations R ↑x)) ↑{ val := s, property := (_ : ¬s ∈ (↑x).asIdeal) }
case intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
f : (x : { x // x ∈ U }) → Localizations R ↑x
r s : R
h :
  ∀ (x : { x // x ∈ U }),
    ¬s ∈ (↑x).asIdeal ∧ f x * ↑(algebraMap R (Localizations R ↑x)) s = ↑(algebraMap R (Localizations R ↑x)) r
⊢ ∃ r s,
    ∀ (x : { x // x ∈ U }),
      ∃ hs, f x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) r { val := s, property := hs }
refine' ⟨r, s, fun x => ⟨(h x).1, (IsLocalization.mk'_eq_iff_eq_mul.mpr _).symm⟩⟩
no goals
case intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
f : (x : { x // x ∈ U }) → Localizations R ↑x
r s : R
h :
  ∀ (x : { x // x ∈ U }),
    ¬s ∈ (↑x).asIdeal ∧ f x * ↑(algebraMap R (Localizations R ↑x)) s = ↑(algebraMap R (Localizations R ↑x)) r
x : { x // x ∈ U }
⊢ ↑(algebraMap R (Localizations R ↑x)) r =
    f x * ↑(algebraMap R (Localizations R ↑x)) ↑{ val := s, property := (_ : ¬s ∈ (↑x).asIdeal) }
exact (h x).2.symm