no goals
ι✝ : Type u'
ι' : Type ?u.254205
R : Type u_2
K : Type ?u.254211
M : Type u_3
M' : Type ?u.254217
M'' : Type ?u.254220
V : Type u
V' : Type ?u.254225
v : ι✝ → M
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
ι : Type u_1
s : Set ι
f : ι → M
hs : LinearIndependent R fun x => f ↑x
⊢ LinearIndependent R fun x => ↑x
convert LinearIndependent.image_of_comp s f id hs