feat(data/equiv/fin): fin_succ_equiv_last (#8805)

This commit changes the type of `fin_succ_equiv'`. `fin_succ_equiv' i` used to take an argument of type `fin n` which was 
strange and it now takes an argument of type `fin (n + 1)` meaning it is now possible to send `fin.last n` to `none` if desired. I also defined `fin.succ_equiv_last`, the canonical equiv `fin (n + 1)` to `option (fin n)` sending `fin.last` to `none`.

Author: ChrisHughes24

src/data/equiv/fin.lean

@@ -64,62 +64,80 @@ by { cases k, refl, }
 /-- An equivalence that removes `i` and maps it to `none`.
 This is a version of `fin.pred_above` that produces `option (fin n)` instead of
 mapping both `i.cast_succ` and `i.succ` to `i`. -/
-def fin_succ_equiv' {n : ℕ} (i : fin n) :
+def fin_succ_equiv' {n : ℕ} (i : fin (n + 1)) :
   fin (n + 1) ≃ option (fin n) :=
-{ to_fun := λ x, if x = i.cast_succ then none else some (i.pred_above x),
-  inv_fun := λ x, x.cases_on' i.cast_succ (fin.succ_above i.cast_succ),
-  left_inv := λ x, if h : x = i.cast_succ then by simp [h]
-                   else by simp [h, fin.succ_above_ne],
-  right_inv := λ x, by { cases x; simp [fin.succ_above_ne] }}
+have hx0 : ∀ {i x : fin (n + 1)}, i < x → x ≠ 0,
+  from λ i x hix, ne_of_gt (lt_of_le_of_lt i.zero_le hix),
+have hiltx : ∀ {i x : fin (n + 1)}, ¬ i < x → ¬ x = i → x < i,
+  from λ i x hix hxi, lt_of_le_of_ne (le_of_not_lt hix) hxi,
+have hxltn : ∀ {i x : fin (n + 1)}, ¬ i < x → ¬ x = i → (x : ℕ) < n,
+  from λ i x hix hxi, lt_of_lt_of_le (hiltx hix hxi) (nat.le_of_lt_succ i.2),
+{ to_fun := λ x,
+    if hix : i < x
+    then some (x.pred (hx0 hix))
+    else if hxi : x = i
+    then none
+    else some (x.cast_lt (hxltn hix hxi)),
+  inv_fun := λ x, x.cases_on' i (fin.succ_above i),
+  left_inv := λ x,
+    if hix : i < x
+    then
+      have hi : i ≤ fin.cast_succ (x.pred (hx0 hix)),
+        by { simp only [fin.le_iff_coe_le_coe, fin.coe_cast_succ, fin.coe_pred],
+          exact nat.le_pred_of_lt hix },
+      by simp [dif_pos hix, option.cases_on'_some, fin.succ_above_above _ _ hi, fin.succ_pred]
+    else if hxi : x = i
+    then by simp [hxi]
+    else have hi : fin.cast_succ (x.cast_lt (hxltn hix hxi)) < i,
+        from lt_of_le_of_ne (le_of_not_gt hix) (by simp [hxi]),
+      by simp only [dif_neg hix, dif_neg hxi, option.cases_on'_some, fin.succ_above_below _ _ hi,
+        fin.cast_succ_cast_lt],
+  right_inv := λ x, by {
+    cases x,
+    { simp },
+    { dsimp,
+      split_ifs,
+      { simp [fin.succ_above_above _ _ ((fin.lt_succ_above_iff _ _).1 h)] },
+      { simpa [fin.succ_above_ne] using h_1 },
+      { have : fin.cast_succ x < i,
+        { rwa [fin.lt_succ_above_iff, not_le] at h },
+        simp [fin.succ_above_below _ _ this] } } } }
 
 @[simp] lemma fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :
-  (fin_succ_equiv' i) i.cast_succ = none := by simp [fin_succ_equiv']
+  (fin_succ_equiv' i) i = none := by simp [fin_succ_equiv']
 
-lemma fin_succ_equiv'_below {n : ℕ} {i m : fin (n + 1)} (h : m < i) :
+lemma fin_succ_equiv'_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
   (fin_succ_equiv' i) m.cast_succ = some m :=
-begin
-  have : m.cast_succ ≤ i.cast_succ := h.le,
-  simp [fin_succ_equiv', h.ne, fin.pred_above_below, this]
-end
+by simp [fin_succ_equiv', dif_neg (not_lt_of_gt h), ne_of_lt h]
 
-lemma fin_succ_equiv'_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :
+lemma fin_succ_equiv'_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
   (fin_succ_equiv' i) m.succ = some m :=
-begin
-  have : i.cast_succ < m.succ,
-    { refine (lt_of_le_of_lt _ m.cast_succ_lt_succ), exact h },
-  simp [fin_succ_equiv', this, fin.pred_above_above, ne_of_gt]
-end
+by simp [fin_succ_equiv', fin.le_cast_succ_iff, *] at *
 
 @[simp] lemma fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :
-  (fin_succ_equiv' i).symm none = i.cast_succ := rfl
+  (fin_succ_equiv' i).symm none = i := rfl
 
-lemma fin_succ_equiv_symm'_some_below {n : ℕ} {i m : fin (n + 1)} (h : m < i) :
+lemma fin_succ_equiv'_symm_some_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
   (fin_succ_equiv' i).symm (some m) = m.cast_succ :=
 by simp [fin_succ_equiv', ne_of_gt h, fin.succ_above, not_le_of_gt h]
 
-lemma fin_succ_equiv_symm'_some_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :
+lemma fin_succ_equiv'_symm_some_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
   (fin_succ_equiv' i).symm (some m) = m.succ :=
 by simp [fin_succ_equiv', fin.succ_above, h.not_lt]
 
-lemma fin_succ_equiv_symm'_coe_below {n : ℕ} {i m : fin (n + 1)} (h : m < i) :
+lemma fin_succ_equiv'_symm_coe_below {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : m.cast_succ < i) :
   (fin_succ_equiv' i).symm m = m.cast_succ :=
-by { convert fin_succ_equiv_symm'_some_below h; simp }
+fin_succ_equiv'_symm_some_below h
 
-lemma fin_succ_equiv_symm'_coe_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :
+lemma fin_succ_equiv'_symm_coe_above {n : ℕ} {i : fin (n + 1)} {m : fin n} (h : i ≤ m.cast_succ) :
   (fin_succ_equiv' i).symm m = m.succ :=
-by { convert fin_succ_equiv_symm'_some_above h; simp }
+fin_succ_equiv'_symm_some_above h
 
 /-- Equivalence between `fin (n + 1)` and `option (fin n)`.
 This is a version of `fin.pred` that produces `option (fin n)` instead of
 requiring a proof that the input is not `0`. -/
--- TODO: make the `n = 0` case neater
 def fin_succ_equiv (n : ℕ) : fin (n + 1) ≃ option (fin n) :=
-nat.cases_on n
-{ to_fun := λ _, none,
-  inv_fun := λ _, 0,
-  left_inv := λ _, by simp,
-  right_inv := λ x, by { cases x, simp, exact x.elim0 } }
-(λ _, fin_succ_equiv' 0)
+fin_succ_equiv' 0
 
 @[simp] lemma fin_succ_equiv_zero {n : ℕ} :
   (fin_succ_equiv n) 0 = none :=
@@ -129,7 +147,7 @@ by cases n; refl
   (fin_succ_equiv n) m.succ = some m :=
 begin
   cases n, { exact m.elim0 },
-  convert fin_succ_equiv'_above m.zero_le
+  rw [fin_succ_equiv, fin_succ_equiv'_above (fin.zero_le _)],
 end
 
 @[simp] lemma fin_succ_equiv_symm_none {n : ℕ} :
@@ -140,7 +158,7 @@ by cases n; refl
   (fin_succ_equiv n).symm (some m) = m.succ :=
 begin
   cases n, { exact m.elim0 },
-  convert fin_succ_equiv_symm'_some_above m.zero_le
+  rw [fin_succ_equiv, fin_succ_equiv'_symm_some_above (fin.zero_le _)],
 end
 
 @[simp] lemma fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :
@@ -149,7 +167,31 @@ fin_succ_equiv_symm_some m
 
 /-- The equiv version of `fin.pred_above_zero`. -/
 lemma fin_succ_equiv'_zero {n : ℕ} :
-  fin_succ_equiv' (0 : fin (n + 1)) = fin_succ_equiv (n + 1) := rfl
+  fin_succ_equiv' (0 : fin (n + 1)) = fin_succ_equiv n := rfl
+
+/-- `equiv` between `fin (n + 1)` and `option (fin n)` sending `fin.last n` to `none` -/
+def fin_succ_equiv_last {n : ℕ} : fin (n + 1) ≃ option (fin n) :=
+fin_succ_equiv' (fin.last n)
+
+@[simp] lemma fin_succ_equiv_last_cast_succ {n : ℕ} (i : fin n) :
+  fin_succ_equiv_last i.cast_succ = some i :=
+fin_succ_equiv'_below i.2
+
+@[simp] lemma fin_succ_equiv_last_last {n : ℕ} :
+  fin_succ_equiv_last (fin.last n) = none :=
+by simp [fin_succ_equiv_last]
+
+@[simp] lemma fin_succ_equiv_last_symm_some {n : ℕ} (i : fin n) :
+  fin_succ_equiv_last.symm (some i) = i.cast_succ :=
+fin_succ_equiv'_symm_some_below i.2
+
+@[simp] lemma fin_succ_equiv_last_symm_coe {n : ℕ} (i : fin n) :
+  fin_succ_equiv_last.symm ↑i = i.cast_succ :=
+fin_succ_equiv'_symm_some_below i.2
+
+@[simp] lemma fin_succ_equiv_last_symm_none {n : ℕ}  :
+  fin_succ_equiv_last.symm none = fin.last n :=
+fin_succ_equiv'_symm_none _
 
 /-- Equivalence between `fin m ⊕ fin n` and `fin (m + n)` -/
 def fin_sum_fin_equiv : fin m ⊕ fin n ≃ fin (m + n) :=

src/linear_algebra/linear_independent.lean

@@ -23,7 +23,6 @@ one, including injectivity of `finsupp.total ι M R v` and some versions with ex
 linear combinations.
 
 ## Main definitions
-
 All definitions are given for families of vectors, i.e. `v : ι → M` where `M` is the module or
 vector space and `ι : Type*` is an arbitrary indexing type.
 
@@ -1133,7 +1132,6 @@ begin
   { ext,
     -- TODO: why doesn't simp use `fin_succ_equiv_symm_coe` here?
     rw [comp_app, comp_app, fin_succ_equiv_symm_coe, fin.cons_succ] },
-  { rw [comp_app, fin_succ_equiv_symm_none, fin.cons_zero] },
   { ext,
     rw [comp_app, comp_app, fin_succ_equiv_symm_coe, fin.cons_succ] }
 end