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
⊢ const R f₁ g₁ U hu = const R f₁ g₁ U (_ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → g₁ ∈ Ideal.primeCompl x.asIdeal)
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
hf : f₁ = f₂
hg : g₁ = g₂
⊢ const R f₁ g₁ U hu = const R f₂ g₂ U (_ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → g₂ ∈ Ideal.primeCompl x.asIdeal)
substs hf hg
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
⊢ const R f₁ g₁ U hu = const R f₁ g₁ U (_ : ∀ (x : ↑(PrimeSpectrum.Top R)), x ∈ U → g₁ ∈ Ideal.primeCompl x.asIdeal)
rfl