no goals
R : Type u_2
R₁ : Type ?u.1239960
R₂ : Type ?u.1239963
R₃ : Type ?u.1239966
R₄ : Type ?u.1239969
S : Type ?u.1239972
K : Type ?u.1239975
K₂ : Type ?u.1239978
M : Type u_3
M' : Type ?u.1239984
M₁ : Type u_1
M₂ : Type ?u.1239990
M₃ : Type ?u.1239993
M₄ : Type ?u.1239996
N : Type ?u.1239999
N₂ : Type ?u.1240002
ι : Type ?u.1240005
V : Type ?u.1240008
V₂ : Type ?u.1240011
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁶ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₂₁ : R₂ →+* R
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
F : Type ?u.1240421
sc : SemilinearMapClass F τ₁₂ M M₂
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
p : Submodule R M
q : Submodule R M₁
f : M →ₗ[R] M₁
hf : ∀ (x : M), x ∈ p → ↑f x ∈ q
⊢ ker (restrict f hf) = ker (domRestrict f p)
rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict]