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.37082
inst✝¹ : AddCommGroup N
inst✝ : Module R N
V V₁ V₂ : Submodule R N
⊢ x ≡ y [SMOD ⊥] ↔ x = y
rw [SModEq.def, Submodule.Quotient.eq, mem_bot, sub_eq_zero]