no goals
R : Type u
inst✝ : CommRing R
f₁ f₂ g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → g₁ ∈ Ideal.primeCompl x.asIdeal
hu₂ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → g₂ ∈ Ideal.primeCompl x.asIdeal
x : { x // x ∈ U.op.unop }
⊢ ↑(const R (f₁ * f₂) (g₁ * g₂) U (_ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → g₁ * g₂ ∈ Ideal.primeCompl x.asIdeal))
      x =
    ↑(const R f₁ g₁ U hu₁ * const R f₂ g₂ U hu₂) x
convert IsLocalization.mk'_mul _ f₁ f₂ ⟨g₁, hu₁ x x.2⟩ ⟨g₂, hu₂ x x.2⟩