no goals
R : Type u
inst✝ : CommRing R
f 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 → f ∈ Ideal.primeCompl x.asIdeal
⊢ const R f g U hu₁ * const R g f U hu₂ = 1
rw [const_mul, const_congr R rfl (mul_comm g f), const_self]