case intro.mk.intro.refl
R : Type u_1
R₁ : Type ?u.1019468
R₂ : Type u_3
R₃ : Type ?u.1019474
R₄ : Type ?u.1019477
S : Type ?u.1019480
K : Type ?u.1019483
K₂ : Type ?u.1019486
M : Type u_2
M' : Type ?u.1019492
M₁ : Type ?u.1019495
M₂ : Type u_4
M₃ : Type ?u.1019501
M₄ : Type ?u.1019504
N : Type ?u.1019507
N₂ : Type ?u.1019510
ι : Type ?u.1019513
V : Type ?u.1019516
V₂ : Type ?u.1019519
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 τ₁₂ τ₂₃ τ₁₃
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), ↑f c ∈ p
p' : Submodule R { x // x ∈ p }
x : M₂
property✝ : f.toAddHom.1 x ∈ p
h : { val := f.toAddHom.1 x, property := property✝ } ∈ ↑p'
⊢ x ∈ comap (codRestrict p f hf) p'
R : Type u_1
R₁ : Type ?u.1019468
R₂ : Type u_3
R₃ : Type ?u.1019474
R₄ : Type ?u.1019477
S : Type ?u.1019480
K : Type ?u.1019483
K₂ : Type ?u.1019486
M : Type u_2
M' : Type ?u.1019492
M₁ : Type ?u.1019495
M₂ : Type u_4
M₃ : Type ?u.1019501
M₄ : Type ?u.1019504
N : Type ?u.1019507
N₂ : Type ?u.1019510
ι : Type ?u.1019513
V : Type ?u.1019516
V₂ : Type ?u.1019519
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 τ₁₂ τ₂₃ τ₁₃
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), ↑f c ∈ p
p' : Submodule R { x // x ∈ p }
x : M₂
⊢ x ∈ comap f (map (Submodule.subtype p) p') → x ∈ comap (codRestrict p f hf) p'
rintro ⟨⟨_, _⟩, h, ⟨⟩⟩
no goals
case intro.mk.intro.refl
R : Type u_1
R₁ : Type ?u.1019468
R₂ : Type u_3
R₃ : Type ?u.1019474
R₄ : Type ?u.1019477
S : Type ?u.1019480
K : Type ?u.1019483
K₂ : Type ?u.1019486
M : Type u_2
M' : Type ?u.1019492
M₁ : Type ?u.1019495
M₂ : Type u_4
M₃ : Type ?u.1019501
M₄ : Type ?u.1019504
N : Type ?u.1019507
N₂ : Type ?u.1019510
ι : Type ?u.1019513
V : Type ?u.1019516
V₂ : Type ?u.1019519
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 τ₁₂ τ₂₃ τ₁₃
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
hf : ∀ (c : M₂), ↑f c ∈ p
p' : Submodule R { x // x ∈ p }
x : M₂
property✝ : f.toAddHom.1 x ∈ p
h : { val := f.toAddHom.1 x, property := property✝ } ∈ ↑p'
⊢ x ∈ comap (codRestrict p f hf) p'
exact h