R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
x y : R ⧸ ⨅ (i : ι), f i
r s : R
hrs : ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) = ↑(quotientInfToPiQuotient f) (Quotient.mk'' s)
i : ι
⊢ ↑(quotientInfToPiQuotient f) (Quotient.mk'' s) i = ↑(Quotient.mk (f i)) s
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
x y : R ⧸ ⨅ (i : ι), f i
r s : R
hrs : ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) = ↑(quotientInfToPiQuotient f) (Quotient.mk'' s)
i : ι
⊢ ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) i = ↑(Quotient.mk (f i)) s
rw [hrs]
no goals
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
x y : R ⧸ ⨅ (i : ι), f i
r s : R
hrs : ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) = ↑(quotientInfToPiQuotient f) (Quotient.mk'' s)
i : ι
⊢ ↑(quotientInfToPiQuotient f) (Quotient.mk'' s) i = ↑(Quotient.mk (f i)) s
rfl