no goals
ι : Type ?u.1210879
ι' : Type ?u.1210882
R : Type ?u.1210885
R₂ : Type ?u.1210888
K : Type u_1
M : Type ?u.1210894
M' : Type ?u.1210897
M'' : Type ?u.1210900
V : Type u
V' : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
p : Submodule K V
f : { x // x ∈ p } →ₗ[K] V'
g : V →ₗ[K] { x // x ∈ p }
hg : comp g (Submodule.subtype p) = id
⊢ comp (comp f g) (Submodule.subtype p) = f
rw [LinearMap.comp_assoc, hg, f.comp_id]