ι✝ : Type u'
ι'✝ : Type ?u.248228
R : Type u_3
K : Type ?u.248234
M : Type u_4
M' : Type ?u.248240
M'' : Type ?u.248243
V : Type u
V' : Type ?u.248248
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → M
hs : LinearIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
⊢ LinearIndependent R fun x => g ↑x
ι✝ : Type u'
ι'✝ : Type ?u.248228
R : Type u_3
K : Type ?u.248234
M : Type u_4
M' : Type ?u.248240
M'' : Type ?u.248243
V : Type u
V' : Type ?u.248248
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → M
hs : LinearIndependent R fun x => g (f ↑x)
⊢ LinearIndependent R fun x => g ↑x
nontriviality R
ι✝ : Type u'
ι'✝ : Type ?u.248228
R : Type u_3
K : Type ?u.248234
M : Type u_4
M' : Type ?u.248240
M'' : Type ?u.248243
V : Type u
V' : Type ?u.248248
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → M
hs : LinearIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
this : InjOn f s
⊢ LinearIndependent R fun x => g ↑x
ι✝ : Type u'
ι'✝ : Type ?u.248228
R : Type u_3
K : Type ?u.248234
M : Type u_4
M' : Type ?u.248240
M'' : Type ?u.248243
V : Type u
V' : Type ?u.248248
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → M
hs : LinearIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
⊢ LinearIndependent R fun x => g ↑x
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
no goals
ι✝ : Type u'
ι'✝ : Type ?u.248228
R : Type u_3
K : Type ?u.248234
M : Type u_4
M' : Type ?u.248240
M'' : Type ?u.248243
V : Type u
V' : Type ?u.248248
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → M
hs : LinearIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
this : InjOn f s
⊢ LinearIndependent R fun x => g ↑x
exact (linearIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs