case h.mk
R : Type u_1
R₁ : Type ?u.394963
R₂ : Type ?u.394966
R₃ : Type ?u.394969
R₄ : Type ?u.394972
S : Type ?u.394975
K : Type ?u.394978
K₂ : Type ?u.394981
M : Type u_2
M' : Type ?u.394987
M₁ : Type ?u.394990
M₂ : Type ?u.394993
M₃ : Type ?u.394996
M₄ : Type ?u.394999
N : Type ?u.395002
N₂ : Type ?u.395005
ι : Type ?u.395008
V : Type ?u.395011
V₂ : Type ?u.395014
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q✝ q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
p q : Submodule R M
h : p ≤ q
b : M
hb : b ∈ p
⊢ ↑(LinearMap.comp (Submodule.subtype q) (ofLe h)) { val := b, property := hb } =
    ↑(Submodule.subtype p) { val := b, property := hb }
R : Type u_1
R₁ : Type ?u.394963
R₂ : Type ?u.394966
R₃ : Type ?u.394969
R₄ : Type ?u.394972
S : Type ?u.394975
K : Type ?u.394978
K₂ : Type ?u.394981
M : Type u_2
M' : Type ?u.394987
M₁ : Type ?u.394990
M₂ : Type ?u.394993
M₃ : Type ?u.394996
M₄ : Type ?u.394999
N : Type ?u.395002
N₂ : Type ?u.395005
ι : Type ?u.395008
V : Type ?u.395011
V₂ : Type ?u.395014
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q✝ q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
p q : Submodule R M
h : p ≤ q
⊢ LinearMap.comp (Submodule.subtype q) (ofLe h) = Submodule.subtype p
ext ⟨b, hb⟩
no goals
case h.mk
R : Type u_1
R₁ : Type ?u.394963
R₂ : Type ?u.394966
R₃ : Type ?u.394969
R₄ : Type ?u.394972
S : Type ?u.394975
K : Type ?u.394978
K₂ : Type ?u.394981
M : Type u_2
M' : Type ?u.394987
M₁ : Type ?u.394990
M₂ : Type ?u.394993
M₃ : Type ?u.394996
M₄ : Type ?u.394999
N : Type ?u.395002
N₂ : Type ?u.395005
ι : Type ?u.395008
V : Type ?u.395011
V₂ : Type ?u.395014
inst✝¹³ : Semiring R
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝² : RingHomInvPair σ₁₂ σ₂₁
inst✝¹ : RingHomInvPair σ₂₁ σ₁₂
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q✝ q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
p q : Submodule R M
h : p ≤ q
b : M
hb : b ∈ p
⊢ ↑(LinearMap.comp (Submodule.subtype q) (ofLe h)) { val := b, property := hb } =
    ↑(Submodule.subtype p) { val := b, property := hb }
rfl