case mk
R : Type u_2
M : Type u_1
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, mk a = Quot.mk Setoid.r x
R : Type u_2
M : Type u_1
r : R
x y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Surjective mk
rintro ⟨x⟩
no goals
case mk
R : Type u_2
M : Type u_1
r : R
x✝ y : M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, mk a = Quot.mk Setoid.r x
exact ⟨x, rfl⟩