no goals
R : Type u_2
R₁ : Type ?u.1010618
R₂ : Type u_1
R₃ : Type ?u.1010624
R₄ : Type ?u.1010627
S : Type ?u.1010630
K : Type ?u.1010633
K₂ : Type ?u.1010636
M : Type u_3
M' : Type ?u.1010642
M₁ : Type ?u.1010645
M₂ : Type u_4
M₃ : Type ?u.1010651
M₄ : Type ?u.1010654
N : Type ?u.1010657
N₂ : Type ?u.1010660
ι : Type ?u.1010663
V : Type ?u.1010666
V₂ : Type ?u.1010669
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 τ₁₂ τ₂₃ τ₁₃
inst✝ : RingHomSurjective σ₂₁
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ (c : M₂), ↑f c ∈ p
p' : Submodule R₂ M₂
x✝ : { x // x ∈ p }
x : M
hx : x ∈ p
⊢ { val := x, property := hx } ∈ map (codRestrict p f h) p' ↔
    { val := x, property := hx } ∈ comap (Submodule.subtype p) (map f p')
simp [Subtype.ext_iff_val]