case mk
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type ?u.182338
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
b✝ : M ⧸ A
x : M
⊢ ∃ a, ↑(mkQ A) a = Quot.mk Setoid.r x
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type ?u.182338
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
⊢ Function.Surjective ↑(mkQ A)
rintro ⟨x⟩
no goals
case mk
R : Type u_1
M : Type u_2
r : R
x✝ y : M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
p p' : Submodule R M
M₂ : Type ?u.182338
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
A : Submodule R M
b✝ : M ⧸ A
x : M
⊢ ∃ a, ↑(mkQ A) a = Quot.mk Setoid.r x
exact ⟨x, rfl⟩