case h
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.220917
M₂ : Type ?u.220920
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M
⊢ x✝ ∈ ker (mkQ p) ↔ x✝ ∈ 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.220917
M₂ : Type ?u.220920
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
⊢ ker (mkQ p) = p
ext
no goals
case h
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.220917
M₂ : Type ?u.220920
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
x✝ : M
⊢ x✝ ∈ ker (mkQ p) ↔ x✝ ∈ p
simp