no goals
ι : Type u'
ι' : Type ?u.203055
R : Type u_2
K : Type ?u.203061
M : Type u_1
M' : Type ?u.203067
M'' : Type ?u.203070
V : Type u
V' : Type ?u.203075
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
s : Set M
⊢ (LinearIndependent R fun x => ↑x) ↔ LinearMap.ker (Finsupp.totalOn M M R id s) = ⊥
rw [Finsupp.totalOn, LinearMap.ker, LinearMap.comap_codRestrict, Submodule.map_bot, comap_bot,
  LinearMap.ker_comp, linearIndependent_subtype_disjoint, disjoint_iff_inf_le, ←
  map_comap_subtype, map_le_iff_le_comap, comap_bot, ker_subtype, le_bot_iff]