chore(linear_algebra/affine_space/independent): allow dot notation on…

… affine_independent (#8974)

This renames a few lemmas to make dot notation on `affine_independent` possible.

src/analysis/convex/caratheodory.lean

@@ -59,14 +59,14 @@ begin
   obtain ⟨i₀, mem, w⟩ : ∃ i₀ ∈ s, ∀ i ∈ s, f i₀ / g i₀ ≤ f i / g i,
   { apply s.exists_min_image (λ z, f z / g z),
     obtain ⟨x, hx, hgx⟩ : ∃ x ∈ t, 0 < g x := gpos,
-    exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩, },
+    exact ⟨x, mem_filter.mpr ⟨hx, hgx⟩⟩ },
   have hg   : 0 < g i₀ := by { rw mem_filter at mem, exact mem.2 },
   have hi₀  : i₀ ∈ t   := filter_subset _ _ mem,
   let  k    : E → ℝ    := λ z, f z - (f i₀ / g i₀) * g z,
   have hk   : k i₀ = 0 := by field_simp [k, ne_of_gt hg],
   have ksum : ∑ e in t.erase i₀, k e = 1,
   { calc ∑ e in t.erase i₀, k e = ∑ e in t, k e :
-      by conv_rhs { rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add], }
+      by conv_rhs { rw [← insert_erase hi₀, sum_insert (not_mem_erase i₀ t), hk, zero_add] }
     ... = ∑ e in t, (f e - f i₀ / g i₀ * g e) : rfl
     ... = 1 : by rw [sum_sub_distrib, fsum, ← mul_sum, gsum, mul_zero, sub_zero] },
   refine ⟨⟨i₀, hi₀⟩, k, _, ksum, _⟩,
@@ -75,17 +75,17 @@ begin
     by_cases hes : e ∈ s,
     { have hge : 0 < g e := by { rw mem_filter at hes, exact hes.2 },
       rw ← le_div_iff hge,
-      exact w _ hes, },
+      exact w _ hes },
     { calc _ ≤ 0   : mul_nonpos_of_nonneg_of_nonpos _ _ -- prove two goals below
          ... ≤ f e : fpos e het,
       { apply div_nonneg (fpos i₀ (mem_of_subset (filter_subset _ t) mem)) (le_of_lt hg) },
-      { simpa only [mem_filter, het, true_and, not_lt] using hes }, } },
+      { simpa only [mem_filter, het, true_and, not_lt] using hes } } },
   { simp only [subtype.coe_mk, center_mass_eq_of_sum_1 _ id ksum, id],
     calc ∑ e in t.erase i₀, k e • e = ∑ e in t, k e • e : sum_erase _ (by rw [hk, zero_smul])
     ... = ∑ e in t, (f e - f i₀ / g i₀ * g e) • e : rfl
     ... = t.center_mass f id : _,
     simp only [sub_smul, mul_smul, sum_sub_distrib, ← smul_sum, gcombo, smul_zero,
-      sub_zero, center_mass, fsum, inv_one, one_smul, id.def], },
+      sub_zero, center_mass, fsum, inv_one, one_smul, id.def] }
 end
 
 variables {s : set E} {x : E} (hx : x ∈ convex_hull s)
@@ -122,7 +122,7 @@ begin
   let k := (min_card_finset_of_mem_convex_hull hx).card - 1,
   have hk : (min_card_finset_of_mem_convex_hull hx).card = k + 1,
   { exact (nat.succ_pred_eq_of_pos
-      (finset.card_pos.mpr (min_card_finset_of_mem_convex_hull_nonempty hx))).symm, },
+      (finset.card_pos.mpr (min_card_finset_of_mem_convex_hull_nonempty hx))).symm },
   classical,
   by_contra,
   obtain ⟨p, hp⟩ := mem_convex_hull_erase h (mem_min_card_finset_of_mem_convex_hull hx),
@@ -150,9 +150,9 @@ begin
     exact ⟨caratheodory.min_card_finset_of_mem_convex_hull hx,
            caratheodory.min_card_finset_of_mem_convex_hull_subseteq hx,
            caratheodory.affine_independent_min_card_finset_of_mem_convex_hull hx,
-           caratheodory.mem_min_card_finset_of_mem_convex_hull hx⟩, },
-  { iterate 3 { convert set.Union_subset _, intro, },
-    exact convex_hull_mono ‹_›, },
+           caratheodory.mem_min_card_finset_of_mem_convex_hull hx⟩ },
+  { iterate 3 { convert set.Union_subset _, intro },
+    exact convex_hull_mono ‹_› }
 end
 
 /-- A more explicit version of `convex_hull_eq_union`. -/
@@ -168,17 +168,14 @@ begin
   obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃,
   let t' := t.filter (λ i, w i ≠ 0),
   refine ⟨t', t'.fintype_coe_sort, (coe : t' → E), w ∘ (coe : t' → E), _, _, _, _, _⟩,
-  { rw subtype.range_coe_subtype, exact set.subset.trans (finset.filter_subset _ t) ht₁, },
-  { exact affine_independent_embedding_of_affine_independent
-      ⟨_, inclusion_injective (finset.filter_subset (λ i, w i ≠ 0) t)⟩ ht₂, },
-  { intros i, suffices : w i ≠ 0,
-    { cases this.lt_or_lt with hneg hpos,
-      { exfalso, rw ← not_le at hneg, apply hneg, exact hw₁ _ (finset.mem_filter.mp i.2).1, },
-      { exact hpos, }, },
-    exact (finset.mem_filter.mp i.property).2, },
-  { erw [finset.sum_attach, finset.sum_filter_ne_zero, hw₂], },
+  { rw subtype.range_coe_subtype, exact subset.trans (finset.filter_subset _ t) ht₁ },
+  { exact ht₂.comp_embedding
+      ⟨_, inclusion_injective (finset.filter_subset (λ i, w i ≠ 0) t)⟩ },
+  { exact λ i, (hw₁ _ (finset.mem_filter.mp i.2).1).lt_of_ne
+      (finset.mem_filter.mp i.property).2.symm },
+  { erw [finset.sum_attach, finset.sum_filter_ne_zero, hw₂] },
   { change ∑ (i : t') in t'.attach, (λ e, w e • e) ↑i = x,
     erw [finset.sum_attach, finset.sum_filter_of_ne],
-    { rw t.center_mass_eq_of_sum_1 id hw₂ at hw₃, exact hw₃, },
-    { intros e he hwe contra, apply hwe, rw [contra, zero_smul], }, },
+    { rw t.center_mass_eq_of_sum_1 id hw₂ at hw₃, exact hw₃ },
+    { intros e he hwe contra, apply hwe, rw [contra, zero_smul] } }
 end

src/geometry/euclidean/circumcenter.lean

@@ -191,7 +191,7 @@ end
 /-- Given a finite nonempty affinely independent family of points,
 there is a unique (circumcenter, circumradius) pair for those points
 in the affine subspace they span. -/
-lemma exists_unique_dist_eq_of_affine_independent {ι : Type*} [hne : nonempty ι] [fintype ι]
+lemma _root_.affine_independent.exists_unique_dist_eq {ι : Type*} [hne : nonempty ι] [fintype ι]
     {p : ι → P} (ha : affine_independent ℝ p) :
   ∃! cccr : (P × ℝ), cccr.fst ∈ affine_span ℝ (set.range p) ∧
     ∀ i, dist (p i) cccr.fst = cccr.snd :=
@@ -233,8 +233,7 @@ begin
           simp },
         { simp } },
       haveI : nonempty ι2 := fintype.card_pos_iff.1 (hc.symm ▸ nat.zero_lt_succ _),
-      have ha2 : affine_independent ℝ (λ i2 : ι2, p i2) :=
-        affine_independent_subtype_of_affine_independent ha _,
+      have ha2 : affine_independent ℝ (λ i2 : ι2, p i2) := ha.subtype _,
       replace hm := hm ha2 hc,
       have hr : set.range p = insert (p i) (set.range (λ i2 : ι2, p i2)),
       { change _ = insert _ (set.range (λ i2 : {x | x ≠ i}, p i2)),
@@ -253,7 +252,7 @@ begin
         (subset_span_points ℝ _)
         _
         hm,
-      convert not_mem_affine_span_diff_of_affine_independent ha i set.univ,
+      convert ha.not_mem_affine_span_diff i set.univ,
       change set.range (λ i2 : {x | x ≠ i}, p i2) = _,
       rw ←set.image_eq_range,
       congr' with j, simp, refl } }
@@ -273,15 +272,15 @@ include V
 
 /-- The pair (circumcenter, circumradius) of a simplex. -/
 def circumcenter_circumradius {n : ℕ} (s : simplex ℝ P n) : (P × ℝ) :=
-(exists_unique_dist_eq_of_affine_independent s.independent).some
+s.independent.exists_unique_dist_eq.some
 
 /-- The property satisfied by the (circumcenter, circumradius) pair. -/
 lemma circumcenter_circumradius_unique_dist_eq {n : ℕ} (s : simplex ℝ P n) :
   (s.circumcenter_circumradius.fst ∈ affine_span ℝ (set.range s.points) ∧
     ∀ i, dist (s.points i) s.circumcenter_circumradius.fst = s.circumcenter_circumradius.snd) ∧
   (∀ cccr : (P × ℝ), (cccr.fst ∈ affine_span ℝ (set.range s.points) ∧
     ∀ i, dist (s.points i) cccr.fst = cccr.snd) → cccr = s.circumcenter_circumradius) :=
-(exists_unique_dist_eq_of_affine_independent s.independent).some_spec
+s.independent.exists_unique_dist_eq.some_spec
 
 /-- The circumcenter of a simplex. -/
 def circumcenter {n : ℕ} (s : simplex ℝ P n) : P :=
@@ -346,8 +345,7 @@ begin
   intro h,
   have hr := s.dist_circumcenter_eq_circumradius,
   simp_rw [←h, dist_eq_zero] at hr,
-  have h01 := (injective_of_affine_independent s.independent).ne
-    (dec_trivial : (0 : fin (n + 2)) ≠ 1),
+  have h01 := s.independent.injective.ne (dec_trivial : (0 : fin (n + 2)) ≠ 1),
   simpa [hr] using h01
 end
 
@@ -703,8 +701,8 @@ begin
   use r,
   intros sx hsxps,
   have hsx : affine_span ℝ (set.range sx.points) = s,
-  { refine affine_span_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one sx.independent
-      (span_points_subset_coe_of_subset_coe (set.subset.trans hsxps h)) _,
+  { refine sx.independent.affine_span_eq_of_le_of_card_eq_finrank_add_one
+      (span_points_subset_coe_of_subset_coe (hsxps.trans h)) _,
     simp [hd] },
   have hc : c ∈ affine_span ℝ (set.range sx.points) := hsx.symm ▸ hc,
   exact (sx.eq_circumradius_of_dist_eq
@@ -759,8 +757,8 @@ begin
   use c,
   intros sx hsxps,
   have hsx : affine_span ℝ (set.range sx.points) = s,
-  { refine affine_span_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one sx.independent
-      (span_points_subset_coe_of_subset_coe (set.subset.trans hsxps h)) _,
+  { refine sx.independent.affine_span_eq_of_le_of_card_eq_finrank_add_one
+      (span_points_subset_coe_of_subset_coe (hsxps.trans h)) _,
     simp [hd] },
   have hc : c ∈ affine_span ℝ (set.range sx.points) := hsx.symm ▸ hc,
   exact (sx.eq_circumcenter_of_dist_eq

src/geometry/euclidean/monge_point.lean

@@ -398,8 +398,8 @@ begin
     (vector_span_mono ℝ (set.image_subset_range s.points ↑(univ.erase i))),
   have hc : card (univ.erase i) = n + 1, { rw card_erase_of_mem (mem_univ _), simp },
   refine add_left_cancel (trans h _),
-  rw [finrank_vector_span_of_affine_independent s.independent (fintype.card_fin _),
-      ← finset.coe_image, finrank_vector_span_image_finset_of_affine_independent s.independent hc]
+  rw [s.independent.finrank_vector_span (fintype.card_fin _),
+      ← finset.coe_image, s.independent.finrank_vector_span_image_finset hc]
 end
 
 /-- A line through a vertex is the altitude through that vertex if and
@@ -573,7 +573,7 @@ begin
   symmetry,
   rw [←h₂, t₂.affine_span_insert_singleton_eq_altitude_iff],
   rw [h₂],
-  use (injective_of_affine_independent t₁.independent).ne hi₁₂,
+  use t₁.independent.injective.ne hi₁₂,
   have he : affine_span ℝ (set.range t₂.points) = affine_span ℝ (set.range t₁.points),
   { refine ext_of_direction_eq _
       ⟨t₁.points i₃, mem_affine_span ℝ ⟨j₃, h₃⟩, mem_affine_span ℝ (set.mem_range_self _)⟩,
@@ -586,8 +586,8 @@ begin
              mem_affine_span ℝ (set.mem_range_self _),
              mem_affine_span ℝ (set.mem_range_self _)⟩ },
     { rw [direction_affine_span, direction_affine_span,
-          finrank_vector_span_of_affine_independent t₁.independent (fintype.card_fin _),
-          finrank_vector_span_of_affine_independent t₂.independent (fintype.card_fin _)] } },
+          t₁.independent.finrank_vector_span (fintype.card_fin _),
+          t₂.independent.finrank_vector_span (fintype.card_fin _)] } },
   rw he,
   use mem_affine_span ℝ (set.mem_range_self _),
   have hu : finset.univ.erase j₂ = {j₁, j₃}, { clear h₁ h₂ h₃, dec_trivial! },
@@ -677,7 +677,7 @@ begin
     rw set.insert_diff_self_of_not_mem ho at hs,
     refine set.eq_of_subset_of_card_le hs _,
     rw [set.card_range_of_injective hpi,
-        set.card_range_of_injective (injective_of_affine_independent t.independent)] }
+        set.card_range_of_injective t.independent.injective] }
 end
 
 /-- For any three points in an orthocentric system generated by
@@ -742,8 +742,8 @@ begin
   haveI := hfd,
   refine eq_of_le_of_finrank_eq (direction_le (affine_span_mono ℝ hps)) _,
   rw [hs, direction_affine_span, direction_affine_span,
-      finrank_vector_span_of_affine_independent ha (fintype.card_fin _),
-      finrank_vector_span_of_affine_independent t.independent (fintype.card_fin _)]
+      ha.finrank_vector_span (fintype.card_fin _),
+      t.independent.finrank_vector_span (fintype.card_fin _)]
 end
 
 /-- All triangles in an orthocentric system have the same circumradius. -/
@@ -756,15 +756,15 @@ begin
   have ht₂s := ht₂,
   rw hts at ht₂,
   rcases exists_dist_eq_circumradius_of_subset_insert_orthocenter hto ht₂
-    (injective_of_affine_independent t₂.independent) with ⟨c, hc, h⟩,
+    t₂.independent.injective with ⟨c, hc, h⟩,
   rw set.forall_range_iff at h,
   have hs : set.range t.points ⊆ s,
   { rw hts,
     exact set.subset_insert _ _ },
   rw [affine_span_of_orthocentric_system ⟨t, hto, hts⟩ hs
-        (injective_of_affine_independent t.independent),
+        t.independent.injective,
       ←affine_span_of_orthocentric_system ⟨t, hto, hts⟩ ht₂s
-        (injective_of_affine_independent t₂.independent)] at hc,
+        t₂.independent.injective] at hc,
   exact (t₂.eq_circumradius_of_dist_eq hc h).symm
 end
 
@@ -777,7 +777,7 @@ begin
   rcases ho with ⟨t₀, ht₀o, ht₀s⟩,
   rw ht₀s at ht,
   rcases exists_of_range_subset_orthocentric_system ht₀o ht
-    (injective_of_affine_independent t.independent) with
+    t.independent.injective with
     ⟨i₁, i₂, i₃, j₂, j₃, h₁₂, h₁₃, h₂₃, h₁₂₃, h₁, hj₂₃, h₂, h₃⟩ | hs,
   { obtain ⟨j₁, hj₁₂, hj₁₃, hj₁₂₃⟩ :
       ∃ j₁ : fin 3, j₁ ≠ j₂ ∧ j₁ ≠ j₃ ∧ ∀ j : fin 3, j = j₁ ∨ j = j₂ ∨ j = j₃,

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -70,14 +70,13 @@ variables {k}
 
 /-- The `vector_span` of a finite subset of an affinely independent
 family has dimension one less than its cardinality. -/
-lemma finrank_vector_span_image_finset_of_affine_independent {p : ι → P}
+lemma affine_independent.finrank_vector_span_image_finset {p : ι → P}
   (hi : affine_independent k p) {s : finset ι} {n : ℕ} (hc : finset.card s = n + 1) :
   finrank k (vector_span k (s.image p : set P)) = n :=
 begin
-  have hi' := affine_independent_of_subset_affine_independent
-    (affine_independent_set_of_affine_independent hi) (set.image_subset_range p ↑s),
+  have hi' := hi.range.mono (set.image_subset_range p ↑s),
   have hc' : (s.image p).card = n + 1,
-  { rwa [s.card_image_of_injective (injective_of_affine_independent hi)] },
+  { rwa s.card_image_of_injective hi.injective },
   have hn : (s.image p).nonempty,
   { simp [hc', ←finset.card_pos] },
   rcases hn with ⟨p₁, hp₁⟩,
@@ -94,37 +93,37 @@ end
 
 /-- The `vector_span` of a finite affinely independent family has
 dimension one less than its cardinality. -/
-lemma finrank_vector_span_of_affine_independent [fintype ι] {p : ι → P}
+lemma affine_independent.finrank_vector_span [fintype ι] {p : ι → P}
   (hi : affine_independent k p) {n : ℕ} (hc : fintype.card ι = n + 1) :
   finrank k (vector_span k (set.range p)) = n :=
 begin
   rw ← finset.card_univ at hc,
   rw [← set.image_univ, ← finset.coe_univ, ← finset.coe_image],
-  exact finrank_vector_span_image_finset_of_affine_independent hi hc
+  exact hi.finrank_vector_span_image_finset hc
 end
 
 /-- If the `vector_span` of a finite subset of an affinely independent
 family lies in a submodule with dimension one less than its
 cardinality, it equals that submodule. -/
-lemma vector_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one
+lemma affine_independent.vector_span_image_finset_eq_of_le_of_card_eq_finrank_add_one
   {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sm : submodule k V}
   [finite_dimensional k sm] (hle : vector_span k (s.image p : set P) ≤ sm)
   (hc : finset.card s = finrank k sm + 1) : vector_span k (s.image p : set P) = sm :=
-eq_of_le_of_finrank_eq hle $ finrank_vector_span_image_finset_of_affine_independent hi hc
+eq_of_le_of_finrank_eq hle $ hi.finrank_vector_span_image_finset hc
 
 /-- If the `vector_span` of a finite affinely independent
 family lies in a submodule with dimension one less than its
 cardinality, it equals that submodule. -/
-lemma vector_span_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one [fintype ι]
+lemma affine_independent.vector_span_eq_of_le_of_card_eq_finrank_add_one [fintype ι]
   {p : ι → P} (hi : affine_independent k p) {sm : submodule k V} [finite_dimensional k sm]
   (hle : vector_span k (set.range p) ≤ sm) (hc : fintype.card ι = finrank k sm + 1) :
   vector_span k (set.range p) = sm :=
-eq_of_le_of_finrank_eq hle $ finrank_vector_span_of_affine_independent hi hc
+eq_of_le_of_finrank_eq hle $ hi.finrank_vector_span hc
 
 /-- If the `affine_span` of a finite subset of an affinely independent
 family lies in an affine subspace whose direction has dimension one
 less than its cardinality, it equals that subspace. -/
-lemma affine_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one
+lemma affine_independent.affine_span_image_finset_eq_of_le_of_card_eq_finrank_add_one
   {p : ι → P} (hi : affine_independent k p) {s : finset ι} {sp : affine_subspace k P}
   [finite_dimensional k sp.direction] (hle : affine_span k (s.image p : set P) ≤ sp)
   (hc : finset.card s = finrank k sp.direction + 1) : affine_span k (s.image p : set P) = sp :=
@@ -134,39 +133,39 @@ begin
   refine eq_of_direction_eq_of_nonempty_of_le _ ((affine_span_nonempty k _).2 hn) hle,
   have hd := direction_le hle,
   rw direction_affine_span at ⊢ hd,
-  exact vector_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one hi hd hc
+  exact hi.vector_span_image_finset_eq_of_le_of_card_eq_finrank_add_one hd hc
 end
 
 /-- If the `affine_span` of a finite affinely independent family lies
 in an affine subspace whose direction has dimension one less than its
 cardinality, it equals that subspace. -/
-lemma affine_span_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one [fintype ι]
+lemma affine_independent.affine_span_eq_of_le_of_card_eq_finrank_add_one [fintype ι]
   {p : ι → P} (hi : affine_independent k p) {sp : affine_subspace k P}
   [finite_dimensional k sp.direction] (hle : affine_span k (set.range p) ≤ sp)
   (hc : fintype.card ι = finrank k sp.direction + 1) : affine_span k (set.range p) = sp :=
 begin
   rw ←finset.card_univ at hc,
   rw [←set.image_univ, ←finset.coe_univ, ← finset.coe_image] at ⊢ hle,
-  exact affine_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one hi hle hc
+  exact hi.affine_span_image_finset_eq_of_le_of_card_eq_finrank_add_one hle hc
 end
 
 /-- The `vector_span` of a finite affinely independent family whose
 cardinality is one more than that of the finite-dimensional space is
 `⊤`. -/
-lemma vector_span_eq_top_of_affine_independent_of_card_eq_finrank_add_one [finite_dimensional k V]
+lemma affine_independent.vector_span_eq_top_of_card_eq_finrank_add_one [finite_dimensional k V]
   [fintype ι] {p : ι → P} (hi : affine_independent k p) (hc : fintype.card ι = finrank k V + 1) :
   vector_span k (set.range p) = ⊤ :=
-eq_top_of_finrank_eq $ finrank_vector_span_of_affine_independent hi hc
+eq_top_of_finrank_eq $ hi.finrank_vector_span hc
 
 /-- The `affine_span` of a finite affinely independent family whose
 cardinality is one more than that of the finite-dimensional space is
 `⊤`. -/
-lemma affine_span_eq_top_of_affine_independent_of_card_eq_finrank_add_one [finite_dimensional k V]
+lemma affine_independent.affine_span_eq_top_of_card_eq_finrank_add_one [finite_dimensional k V]
   [fintype ι] {p : ι → P} (hi : affine_independent k p) (hc : fintype.card ι = finrank k V + 1) :
   affine_span k (set.range p) = ⊤ :=
 begin
   rw [←finrank_top, ←direction_top k V P] at hc,
-  exact affine_span_eq_of_le_of_affine_independent_of_card_eq_finrank_add_one hi le_top hc
+  exact hi.affine_span_eq_of_le_of_card_eq_finrank_add_one le_top hc
 end
 
 variables (k)