case h
R : Type u
inst✝ : CommRing R
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
⊢ f * g₁ * g₂ = f * (g₁ * g₂)
R : Type u
inst✝ : CommRing R
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
⊢ const R f g₁ U hu₁ * const R g₁ g₂ U hu₂ = const R f g₂ U hu₂
rw [const_mul, const_ext]
no goals
case h
R : Type u
inst✝ : CommRing R
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
⊢ f * g₁ * g₂ = f * (g₁ * g₂)
rw [mul_assoc]