no goals
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.30171
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ y [SMOD U] ↔ x - y ∈ U
rw [SModEq.def, Submodule.Quotient.eq]