R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ Submodule.Quotient.mk (Polynomial.eval x f) = Submodule.Quotient.mk (Polynomial.eval y f)
R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
h : x ≡ y [SMOD I]
f : R[X]
⊢ Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]
rw [SModEq.def] at h⊢
R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval x f) = ↑(Ideal.Quotient.mk I) (Polynomial.eval y f)
R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ Submodule.Quotient.mk (Polynomial.eval x f) = Submodule.Quotient.mk (Polynomial.eval y f)
show Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y)
R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
f : R[X]
h : ↑(Ideal.Quotient.mk I) x = ↑(Ideal.Quotient.mk I) y
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval x f) = ↑(Ideal.Quotient.mk I) (Polynomial.eval y f)
R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval x f) = ↑(Ideal.Quotient.mk I) (Polynomial.eval y f)
replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h
no goals
R✝ : Type ?u.82108
inst✝⁵ : Ring R✝
M : Type ?u.82114
inst✝⁴ : AddCommGroup M
inst✝³ : Module R✝ M
U U₁ U₂ : Submodule R✝ M
x✝ x₁ x₂ y✝ y₁ y₂ z z₁ z₂ : M
N : Type ?u.83145
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x y : R
f : R[X]
h : ↑(Ideal.Quotient.mk I) x = ↑(Ideal.Quotient.mk I) y
⊢ ↑(Ideal.Quotient.mk I) (Polynomial.eval x f) = ↑(Ideal.Quotient.mk I) (Polynomial.eval y f)
rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h]