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
h : f₁ * g₂ = f₂ * g₁
x : { x // x ∈ U.op.unop }
⊢ ↑{ val := g₁, property := (_ : g₁ ∈ Ideal.primeCompl (↑x).asIdeal) } * f₂ =
    ↑{ val := g₂, property := (_ : g₂ ∈ Ideal.primeCompl (↑x).asIdeal) } * f₁
rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk]