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
R₂ : Type ?u.216815
M₂ : Type ?u.216818
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M ⧸ p
x : M
⊢ Quot.mk Setoid.r x ∈ range (mkQ p)
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
R₂ : Type ?u.216815
M₂ : Type ?u.216818
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ ∀ (x : M ⧸ p), x ∈ range (mkQ p)
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
R₂ : Type ?u.216815
M₂ : Type ?u.216818
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M ⧸ p
x : M
⊢ Quot.mk Setoid.r x ∈ range (mkQ p)
exact ⟨x, rfl⟩