[Merged by Bors] - refactor(LinearIndependent): refactor to use LinearIndepOn

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -535,8 +535,8 @@ theorem ZLattice.rank [hs : IsZLattice K L] : finrank ℤ L = finrank K E := by
     -- `e` is a `K`-basis of `E` formed of vectors of `b`
     let e : Basis t K E := Basis.mk ht_lin (by simp [ht_span, h_spanE])
     have : Fintype t := Set.Finite.fintype ((Set.range b).toFinite.subset ht_inc)
-    have h : LinearIndependent ℤ (fun x : (Set.range b) => (x : E)) := by
-      rwa [linearIndependent_subtype_range (Subtype.coe_injective.comp b₀.injective)]
+    have h : LinearIndepOn ℤ id (Set.range b) := by
+      rwa [linearIndepOn_id_range_iff (Subtype.coe_injective.comp b₀.injective)]
     contrapose! h
     -- Since `finrank ℤ L > finrank K E`, there exists a vector `v ∈ b` with `v ∉ e`
     obtain ⟨v, hv⟩ : (Set.range b \ Set.range e).Nonempty := by
@@ -548,14 +548,14 @@ theorem ZLattice.rank [hs : IsZLattice K L] : finrank ℤ L = finrank K E := by
       rwa [not_lt, h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span,
         finrank_span_set_eq_card ht_lin]
     -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction
-    suffices ¬ LinearIndependent ℤ (fun x : ↥(insert v (Set.range e)) => (x : E)) by
+    suffices ¬ LinearIndepOn ℤ id (insert v (Set.range e)) by
       contrapose! this
-      refine LinearIndependent.mono ?_ this
+      refine this.mono ?_
       exact Set.insert_subset (Set.mem_of_mem_diff hv) (by simp [e, ht_inc])
     -- We prove finally that `e ∪ {v}` is not ℤ-linear independent or, equivalently,
     -- not ℚ-linear independent by showing that `v ∈ span ℚ e`.
-    rw [LinearIndependent.iff_fractionRing ℤ ℚ,
-      linearIndependent_insert (Set.not_mem_of_mem_diff hv),  not_and, not_not]
+    rw [LinearIndepOn, LinearIndependent.iff_fractionRing ℤ ℚ, ← LinearIndepOn,
+      linearIndepOn_id_insert (Set.not_mem_of_mem_diff hv), not_and, not_not]
     intro _
     -- But that follows from the fact that there exist `n, m : ℕ`, `n ≠ m`
     -- such that `(n - m) • v ∈ span ℤ e` which is true since `n ↦ ZSpan.fract e (n • v)`

Mathlib/FieldTheory/Fixed.lean

@@ -111,22 +111,23 @@ theorem coe_algebraMap :
   rfl
 
 theorem linearIndependent_smul_of_linearIndependent {s : Finset F} :
-    (LinearIndependent (FixedPoints.subfield G F) fun i : (s : Set F) => (i : F)) →
-      LinearIndependent F fun i : (s : Set F) => MulAction.toFun G F i := by
+    (LinearIndepOn (FixedPoints.subfield G F) id (s : Set F)) →
+      LinearIndepOn F (MulAction.toFun G F) s := by
   classical
   have : IsEmpty ((∅ : Finset F) : Set F) := by simp
   refine Finset.induction_on s (fun _ => linearIndependent_empty_type) fun a s has ih hs => ?_
   rw [coe_insert] at hs ⊢
-  rw [linearIndependent_insert (mt mem_coe.1 has)] at hs
-  rw [linearIndependent_insert' (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
+  rw [linearIndepOn_insert (mt mem_coe.1 has)] at hs
+  rw [linearIndepOn_insert (mt mem_coe.1 has)]; refine ⟨ih hs.1, fun ha => ?_⟩
   rw [Finsupp.mem_span_image_iff_linearCombination] at ha; rcases ha with ⟨l, hl, hla⟩
   rw [Finsupp.linearCombination_apply_of_mem_supported F hl] at hla
   suffices ∀ i ∈ s, l i ∈ FixedPoints.subfield G F by
     replace hla := (sum_apply _ _ fun i => l i • toFun G F i).symm.trans (congr_fun hla 1)
     simp_rw [Pi.smul_apply, toFun_apply, one_smul] at hla
     refine hs.2 (hla ▸ Submodule.sum_mem _ fun c hcs => ?_)
     change (⟨l c, this c hcs⟩ : FixedPoints.subfield G F) • c ∈ _
-    exact Submodule.smul_mem _ _ (Submodule.subset_span <| mem_coe.2 hcs)
+    refine Submodule.smul_mem _ _ (Submodule.subset_span <| by simpa)
+
   intro i his g
   refine
     eq_of_sub_eq_zero

Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean

@@ -332,7 +332,7 @@ and is an intermediate result used to prove it. -/
 private theorem LinearIndependent.map_pow_expChar_pow_of_fd_isSeparable
     [FiniteDimensional F E] [Algebra.IsSeparable F E]
     (h : LinearIndependent F v) : LinearIndependent F (v · ^ q ^ n) := by
-  have h' := h.coe_range
+  have h' := h.linearIndepOn_id
   let ι' := h'.extend (Set.range v).subset_univ
   let b : Basis ι' F E := Basis.extend h'
   letI : Fintype ι' := FiniteDimensional.fintypeBasisIndex b

Mathlib/Geometry/Euclidean/MongePoint.lean

@@ -396,8 +396,7 @@ theorem affineSpan_pair_eq_altitude_iff {n : ℕ} (s : Simplex ℝ P (n + 1)) (i
       simpa using h
     · rw [finrank_direction_altitude, finrank_span_set_eq_card]
       · simp
-      · refine linearIndependent_singleton ?_
-        simpa using hne
+      · exact LinearIndepOn.id_singleton _ <| by simpa using hne
 
 end Simplex
 

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

@@ -571,11 +571,13 @@ theorem exists_subset_affineIndependent_affineSpan_eq_top {s : Set P}
     have hsvi := bsv.linearIndependent
     have hsvt := bsv.span_eq
     rw [Basis.coe_extend] at hsvi hsvt
+    rw [linearIndependent_subtype_iff] at hsvi h
     have hsv := h.subset_extend (Set.subset_univ _)
     have h0 : ∀ v : V, v ∈ h.extend (Set.subset_univ _) → v ≠ 0 := by
       intro v hv
       simpa [bsv] using bsv.ne_zero ⟨v, hv⟩
-    rw [linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
+    rw [← linearIndependent_subtype_iff,
+      linearIndependent_set_iff_affineIndependent_vadd_union_singleton k h0 p₁] at hsvi
     refine ⟨{p₁} ∪ (fun v => v +ᵥ p₁) '' h.extend (Set.subset_univ _), ?_, ?_⟩
     · refine Set.Subset.trans ?_ (Set.union_subset_union_right _ (Set.image_subset _ hsv))
       simp [Set.image_image]

Mathlib/LinearAlgebra/Basis/Cardinality.lean

@@ -98,8 +98,8 @@ theorem union_support_maximal_linearIndependent_eq_range_basis {ι : Type w} (b
   have r' : b i ∉ range v := fun ⟨k, p⟩ ↦ by simpa [w] using congr(b.repr $p i)
   have r'' : range v ≠ range v' := (r' <| · ▸ ⟨none, rfl⟩)
   -- The key step in the proof is checking that this strictly larger family is linearly independent.
-  have i' : LinearIndependent R ((↑) : range v' → M) := by
-    apply LinearIndependent.to_subtype_range
+  have i' : LinearIndepOn R id (range v') := by
+    apply LinearIndependent.linearIndepOn_id
     rw [linearIndependent_iffₛ]
     intro l l' z
     simp_rw [linearCombination_option, v', Option.elim'] at z

Mathlib/LinearAlgebra/Basis/VectorSpace.lean

@@ -43,21 +43,20 @@ namespace Basis
 section ExistsBasis
 
 /-- If `s` is a linear independent set of vectors, we can extend it to a basis. -/
-noncomputable def extend (hs : LinearIndependent K ((↑) : s → V)) :
+noncomputable def extend (hs : LinearIndepOn K id s) :
     Basis (hs.extend (subset_univ s)) K V :=
   Basis.mk
-    (@LinearIndependent.restrict_of_comp_subtype _ _ _ id _ _ _ _ (hs.linearIndependent_extend _))
+    (hs.linearIndepOn_extend _).linearIndependent_restrict
     (SetLike.coe_subset_coe.mp <| by simpa using hs.subset_span_extend (subset_univ s))
 
-theorem extend_apply_self (hs : LinearIndependent K ((↑) : s → V)) (x : hs.extend _) :
-    Basis.extend hs x = x :=
+theorem extend_apply_self (hs : LinearIndepOn K id s) (x : hs.extend _) : Basis.extend hs x = x :=
   Basis.mk_apply _ _ _
 
 @[simp]
-theorem coe_extend (hs : LinearIndependent K ((↑) : s → V)) : ⇑(Basis.extend hs) = ((↑) : _ → _) :=
+theorem coe_extend (hs : LinearIndepOn K id s) : ⇑(Basis.extend hs) = ((↑) : _ → _) :=
   funext (extend_apply_self hs)
 
-theorem range_extend (hs : LinearIndependent K ((↑) : s → V)) :
+theorem range_extend (hs : LinearIndepOn K id s) :
     range (Basis.extend hs) = hs.extend (subset_univ _) := by
   rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]
 
@@ -67,66 +66,60 @@ theorem range_extend (hs : LinearIndependent K ((↑) : s → V)) :
 The specific value of this definition should be considered an implementation detail.
 -/
 def sumExtendIndex (hs : LinearIndependent K v) : Set V :=
-  LinearIndependent.extend hs.to_subtype_range (subset_univ _) \ range v
+  LinearIndepOn.extend hs.linearIndepOn_id (subset_univ _) \ range v
 
 /-- If `v` is a linear independent family of vectors, extend it to a basis indexed by a sum type. -/
 noncomputable def sumExtend (hs : LinearIndependent K v) : Basis (ι ⊕ sumExtendIndex hs) K V :=
   let s := Set.range v
   let e : ι ≃ s := Equiv.ofInjective v hs.injective
-  let b := hs.to_subtype_range.extend (subset_univ (Set.range v))
-  (Basis.extend hs.to_subtype_range).reindex <|
+  let b := hs.linearIndepOn_id.extend (subset_univ (Set.range v))
+  (Basis.extend hs.linearIndepOn_id).reindex <|
     Equiv.symm <|
       calc
         ι ⊕ (b \ s : Set V) ≃ s ⊕ (b \ s : Set V) := Equiv.sumCongr e (Equiv.refl _)
         _ ≃ b :=
           haveI := Classical.decPred (· ∈ s)
-          Equiv.Set.sumDiffSubset (hs.to_subtype_range.subset_extend _)
+          Equiv.Set.sumDiffSubset (hs.linearIndepOn_id.subset_extend _)
 
-theorem subset_extend {s : Set V} (hs : LinearIndependent K ((↑) : s → V)) :
-    s ⊆ hs.extend (Set.subset_univ _) :=
+theorem subset_extend {s : Set V} (hs : LinearIndepOn K id s) : s ⊆ hs.extend (Set.subset_univ _) :=
   hs.subset_extend _
 
 /-- If `s` is a family of linearly independent vectors contained in a set `t` spanning `V`,
 then one can get a basis of `V` containing `s` and contained in `t`. -/
-noncomputable def extendLe (hs : LinearIndependent K ((↑) : s → V))
-    (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
+noncomputable def extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
     Basis (hs.extend hst) K V :=
   Basis.mk
-    (@LinearIndependent.restrict_of_comp_subtype _ _ _ id _ _ _ _ (hs.linearIndependent_extend _))
+    ((hs.linearIndepOn_extend _).linearIndependent ..)
     (le_trans ht <| Submodule.span_le.2 <| by simpa using hs.subset_span_extend hst)
 
-theorem extendLe_apply_self (hs : LinearIndependent K ((↑) : s → V))
-    (hst : s ⊆ t) (ht : ⊤ ≤ span K t) (x : hs.extend hst) :
-    Basis.extendLe hs hst ht x = x :=
+theorem extendLe_apply_self (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t)
+    (x : hs.extend hst) : Basis.extendLe hs hst ht x = x :=
   Basis.mk_apply _ _ _
 
 @[simp]
-theorem coe_extendLe (hs : LinearIndependent K ((↑) : s → V))
-    (hst : s ⊆ t) (ht : ⊤ ≤ span K t) : ⇑(Basis.extendLe hs hst ht) = ((↑) : _ → _) :=
+theorem coe_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
+    ⇑(Basis.extendLe hs hst ht) = ((↑) : _ → _) :=
   funext (extendLe_apply_self hs hst ht)
 
-theorem range_extendLe (hs : LinearIndependent K ((↑) : s → V))
-    (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
+theorem range_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
     range (Basis.extendLe hs hst ht) = hs.extend hst := by
   rw [coe_extendLe, Subtype.range_coe_subtype, setOf_mem_eq]
 
-theorem subset_extendLe (hs : LinearIndependent K ((↑) : s → V))
-    (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
+theorem subset_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
     s ⊆ range (Basis.extendLe hs hst ht) :=
   (range_extendLe hs hst ht).symm ▸ hs.subset_extend hst
 
-theorem extendLe_subset (hs : LinearIndependent K ((↑) : s → V))
-    (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
+theorem extendLe_subset (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
     range (Basis.extendLe hs hst ht) ⊆ t :=
   (range_extendLe hs hst ht).symm ▸ hs.extend_subset hst
 
 /-- If a set `s` spans the space, this is a basis contained in `s`. -/
 noncomputable def ofSpan (hs : ⊤ ≤ span K s) :
-    Basis ((linearIndependent_empty K V).extend (empty_subset s)) K V :=
+    Basis ((linearIndepOn_empty K id).extend (empty_subset s)) K V :=
   extendLe (linearIndependent_empty K V) (empty_subset s) hs
 
 theorem ofSpan_apply_self (hs : ⊤ ≤ span K s)
-    (x : (linearIndependent_empty K V).extend (empty_subset s)) :
+    (x : (linearIndepOn_empty K id).extend (empty_subset s)) :
     Basis.ofSpan hs x = x :=
   extendLe_apply_self (linearIndependent_empty K V) (empty_subset s) hs x
 
@@ -135,7 +128,7 @@ theorem coe_ofSpan (hs : ⊤ ≤ span K s) : ⇑(ofSpan hs) = ((↑) : _ → _)
   funext (ofSpan_apply_self hs)
 
 theorem range_ofSpan (hs : ⊤ ≤ span K s) :
-    range (ofSpan hs) = (linearIndependent_empty K V).extend (empty_subset s) := by
+    range (ofSpan hs) = (linearIndepOn_empty K id).extend (empty_subset s) := by
   rw [coe_ofSpan, Subtype.range_coe_subtype, setOf_mem_eq]
 
 theorem ofSpan_subset (hs : ⊤ ≤ span K s) : range (ofSpan hs) ⊆ s :=
@@ -147,7 +140,7 @@ variable (K V)
 
 /-- A set used to index `Basis.ofVectorSpace`. -/
 noncomputable def ofVectorSpaceIndex : Set V :=
-  (linearIndependent_empty K V).extend (subset_univ _)
+  (linearIndepOn_empty K id).extend (subset_univ _)
 
 /-- Each vector space has a basis. -/
 noncomputable def ofVectorSpace : Basis (ofVectorSpaceIndex K V) K V :=
@@ -242,10 +235,10 @@ theorem LinearMap.exists_leftInverse_of_injective (f : V →ₗ[K] V') (hf_inj :
     ∃ g : V' →ₗ[K] V, g.comp f = LinearMap.id := by
   let B := Basis.ofVectorSpaceIndex K V
   let hB := Basis.ofVectorSpace K V
-  have hB₀ : _ := hB.linearIndependent.to_subtype_range
-  have : LinearIndependent K (fun x => x : f '' B → V') := by
-    have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
-      LinearIndependent.image_subtype (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
+  have hB₀ : _ := hB.linearIndependent.linearIndepOn_id
+  have : LinearIndepOn K _root_.id (f '' B) := by
+    have h₁ : LinearIndepOn K _root_.id (f '' Set.range (Basis.ofVectorSpace K V)) :=
+      LinearIndepOn.image (f := f) hB₀ (show Disjoint _ _ by simp [hf_inj])
     rwa [Basis.range_ofVectorSpace K V] at h₁
   let C := this.extend (subset_univ _)
   have BC := this.subset_extend (subset_univ _)

Mathlib/LinearAlgebra/Dimension/Basic.lean

@@ -57,13 +57,13 @@ this is the same as the dimension of the space (i.e. the cardinality of any basi
 In particular this agrees with the usual notion of the dimension of a vector space. -/
 @[stacks 09G3 "first part"]
 protected irreducible_def Module.rank : Cardinal :=
-  ⨆ ι : { s : Set M // LinearIndependent R ((↑) : s → M) }, (#ι.1)
+  ⨆ ι : { s : Set M // LinearIndepOn R id s }, (#ι.1)
 
 theorem rank_le_card : Module.rank R M ≤ #M :=
   (Module.rank_def _ _).trans_le (ciSup_le' fun _ ↦ mk_set_le _)
 
-lemma nonempty_linearIndependent_set : Nonempty {s : Set M // LinearIndependent R ((↑) : s → M)} :=
-  ⟨⟨∅, linearIndependent_empty _ _⟩⟩
+lemma nonempty_linearIndependent_set : Nonempty {s : Set M // LinearIndepOn R id s } :=
+  ⟨⟨∅, linearIndepOn_empty _ _⟩⟩
 
 end
 
@@ -77,7 +77,7 @@ theorem cardinal_lift_le_rank {ι : Type w} {v : ι → M}
     (hv : LinearIndependent R v) :
     Cardinal.lift.{v} #ι ≤ Cardinal.lift.{w} (Module.rank R M) := by
   rw [Module.rank]
-  refine le_trans ?_ (lift_le.mpr <| le_ciSup (bddAbove_range _) ⟨_, hv.coe_range⟩)
+  refine le_trans ?_ (lift_le.mpr <| le_ciSup (bddAbove_range _) ⟨_, hv.linearIndepOn_id⟩)
   exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩
 
 lemma aleph0_le_rank {ι : Type w} [Infinite ι] {v : ι → M}
@@ -113,8 +113,8 @@ theorem lift_rank_le_of_injective_injectiveₛ (i : R' → R) (j : M →+ M')
     lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') := by
   simp_rw [Module.rank, lift_iSup (bddAbove_range _)]
   exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
-    (h.map_of_injective_injectiveₛ i j hi hj hc).image⟩,
-      lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩
+    LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
+    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩
 
 /-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map, and
 `j : M →+ M'` is an injective monoid homomorphism, such that the scalar multiplications on `M` and
@@ -180,9 +180,10 @@ theorem lift_rank_le_of_injective_injective [AddCommGroup M'] [Module R' M']
     (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
     lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') := by
   simp_rw [Module.rank, lift_iSup (bddAbove_range _)]
-  exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
-    (h.map_of_injective_injective i j hi (fun _ _ ↦ hj <| by rwa [j.map_zero]) hc).image⟩,
-      lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩
+  exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦
+    ⟨⟨j '' s, LinearIndepOn.id_image <| h.linearIndependent.map_of_injective_injective i j hi
+      (fun _ _ ↦ hj <| by rwa [j.map_zero]) hc⟩,
+    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩
 
 /-- The same-universe version of `lift_rank_le_of_injective_injective`. -/
 theorem rank_le_of_injective_injective [AddCommGroup M₁] [Module R' M₁]
@@ -367,17 +368,13 @@ theorem LinearMap.rank_le_of_surjective (f : M →ₗ[R] M₁) (h : Surjective f
 @[nontriviality, simp]
 theorem rank_subsingleton [Subsingleton R] : Module.rank R M = 1 := by
   haveI := Module.subsingleton R M
-  have : Nonempty { s : Set M // LinearIndependent R ((↑) : s → M) } :=
-    ⟨⟨∅, linearIndependent_empty _ _⟩⟩
+  have : Nonempty { s : Set M // LinearIndepOn R id s} := ⟨⟨∅, linearIndepOn_empty _ _⟩⟩
   rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
   · rintro ⟨s, hs⟩
     rw [Cardinal.mk_le_one_iff_set_subsingleton]
     apply subsingleton_of_subsingleton
   intro w hw
-  refine ⟨⟨{0}, ?_⟩, ?_⟩
-  · rw [linearIndependent_iff'ₛ]
-    subsingleton
-  · exact hw.trans_eq (Cardinal.mk_singleton _).symm
+  exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩
 
 lemma rank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M]
     [IsScalarTower S R M] (L L' : Submodule R M) {s : S} (hr : IsSMulRegular M s)