case h.a
R : Type u_1
R₁ : Type ?u.1872963
R₂ : Type u_3
R₃ : Type ?u.1872969
R₄ : Type ?u.1872972
S : Type ?u.1872975
K : Type ?u.1872978
K₂ : Type ?u.1872981
M : Type u_2
M' : Type ?u.1872987
M₁ : Type ?u.1872990
M₂ : Type u_4
M₃ : Type ?u.1872996
M₄ : Type ?u.1872999
N : Type ?u.1873002
N₂ : Type ?u.1873005
ι : Type ?u.1873008
V : Type ?u.1873011
V₂ : Type ?u.1873014
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M₄
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x✝ : { x // x ∈ Submodule.comap (↑f) U }
⊢ ↑(↑↑(ofSubmodule' f U) x✝) =
    ↑(↑(LinearMap.codRestrict U (LinearMap.domRestrict (↑f) (Submodule.comap (↑f) U))
            (_ : ∀ (x : { x // x ∈ Submodule.comap (↑f) U }), ↑x ∈ Submodule.comap (↑f) U))
        x✝)
R : Type u_1
R₁ : Type ?u.1872963
R₂ : Type u_3
R₃ : Type ?u.1872969
R₄ : Type ?u.1872972
S : Type ?u.1872975
K : Type ?u.1872978
K₂ : Type ?u.1872981
M : Type u_2
M' : Type ?u.1872987
M₁ : Type ?u.1872990
M₂ : Type u_4
M₃ : Type ?u.1872996
M₄ : Type ?u.1872999
N : Type ?u.1873002
N₂ : Type ?u.1873005
ι : Type ?u.1873008
V : Type ?u.1873011
V₂ : Type ?u.1873014
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M₄
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
⊢ ↑(ofSubmodule' f U) =
    LinearMap.codRestrict U (LinearMap.domRestrict (↑f) (Submodule.comap (↑f) U))
      (_ : ∀ (x : { x // x ∈ Submodule.comap (↑f) U }), ↑x ∈ Submodule.comap (↑f) U)
ext
no goals
case h.a
R : Type u_1
R₁ : Type ?u.1872963
R₂ : Type u_3
R₃ : Type ?u.1872969
R₄ : Type ?u.1872972
S : Type ?u.1872975
K : Type ?u.1872978
K₂ : Type ?u.1872981
M : Type u_2
M' : Type ?u.1872987
M₁ : Type ?u.1872990
M₂ : Type u_4
M₃ : Type ?u.1872996
M₄ : Type ?u.1872999
N : Type ?u.1873002
N₂ : Type ?u.1873005
ι : Type ?u.1873008
V : Type ?u.1873011
V₂ : Type ?u.1873014
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring R₃
inst✝⁷ : Semiring R₄
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : AddCommMonoid M₄
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
f✝ : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
e : M ≃ₛₗ[σ₁₂] M₂
h : M₂ →ₛₗ[σ₂₃] M₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
p q : Submodule R M
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
f : M ≃ₛₗ[σ₁₂] M₂
U : Submodule R₂ M₂
x✝ : { x // x ∈ Submodule.comap (↑f) U }
⊢ ↑(↑↑(ofSubmodule' f U) x✝) =
    ↑(↑(LinearMap.codRestrict U (LinearMap.domRestrict (↑f) (Submodule.comap (↑f) U))
            (_ : ∀ (x : { x // x ∈ Submodule.comap (↑f) U }), ↑x ∈ Submodule.comap (↑f) U))
        x✝)
rfl