[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U
[PROOFSTEP]
rw [SModEq.def, Submodule.Quotient.eq]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ y [SMOD ⊥] ↔ x = y
[PROOFSTEP]
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
[PROOFSTEP]
rw [SModEq.def] at hxy₁ hxy₂ ⊢
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk (x₁ + x₂) = Submodule.Quotient.mk (y₁ + y₂)
[PROOFSTEP]
simp_rw [Quotient.mk_add, hxy₁, hxy₂]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy : x ≡ y [SMOD U]
c : R
⊢ c • x ≡ c • y [SMOD U]
[PROOFSTEP]
rw [SModEq.def] at hxy ⊢
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y
c : R
⊢ Submodule.Quotient.mk (c • x) = Submodule.Quotient.mk (c • y)
[PROOFSTEP]
simp_rw [Quotient.mk_smul, hxy]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
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_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U
[PROOFSTEP]
rw [SModEq.def, Submodule.Quotient.eq, sub_zero]
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
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_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
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]
[PROOFSTEP]
rw [SModEq.def] at h ⊢
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
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_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
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)
[PROOFSTEP]
show Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y)
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
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_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
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)
[PROOFSTEP]
replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h
[GOAL]
R✝ : Type u_1
inst✝⁵ : Ring R✝
M : Type u_2
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_3
inst✝² : AddCommGroup N
inst✝¹ : Module R✝ N
V V₁ V₂ : Submodule R✝ N
R : Type u_4
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)
[PROOFSTEP]
rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h]
