feat(data/equiv/basic): Add fin_succ_above_equiv (#5145)

Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/data/equiv/fin.lean

@@ -37,24 +37,95 @@ def fin_two_equiv : fin 2 ≃ bool :=
   end,
   assume b, match b with tt := rfl | ff := rfl end⟩
 
-/-- Equivalence between `fin n.succ` and `option (fin n)` -/
-def fin_succ_equiv (n : ℕ) : fin n.succ ≃ option (fin n) :=
-⟨λ x, fin.cases none some x, λ x, option.rec_on x 0 fin.succ,
-  λ x, fin.cases rfl (λ i, show (option.rec_on (fin.cases none some (fin.succ i) : option (fin n))
-    0 fin.succ : fin n.succ) = _, by rw fin.cases_succ) x,
-  by rintro ⟨none | x⟩; [refl, exact fin.cases_succ _]⟩
+/-- 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) :
+  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] }}
+
+@[simp] lemma fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :
+  (fin_succ_equiv' i) i.cast_succ = none := by simp [fin_succ_equiv']
+
+lemma fin_succ_equiv'_below {n : ℕ} {i m : fin (n + 1)} (h : m < 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
+
+lemma fin_succ_equiv'_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :
+  (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
+
+@[simp] lemma fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :
+  (fin_succ_equiv' i).symm none = i.cast_succ := rfl
+
+lemma fin_succ_equiv_symm'_some_below {n : ℕ} {i m : fin (n + 1)} (h : m < 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) :
+  (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) :
+  (fin_succ_equiv' i).symm m = m.cast_succ :=
+by { convert fin_succ_equiv_symm'_some_below h; simp }
+
+lemma fin_succ_equiv_symm'_coe_above {n : ℕ} {i m : fin (n + 1)} (h : i ≤ m) :
+  (fin_succ_equiv' i).symm m = m.succ :=
+by { convert fin_succ_equiv_symm'_some_above h; simp }
+
+/-- 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)
 
 @[simp] lemma fin_succ_equiv_zero {n : ℕ} :
-  (fin_succ_equiv n) 0 = none := rfl
+  (fin_succ_equiv n) 0 = none :=
+by cases n; refl
 
 @[simp] lemma fin_succ_equiv_succ {n : ℕ} (m : fin n):
-  (fin_succ_equiv n) m.succ = some m := by simp [fin_succ_equiv]
+  (fin_succ_equiv n) m.succ = some m :=
+begin
+  cases n, { exact m.elim0 },
+  convert fin_succ_equiv'_above m.zero_le
+end
 
 @[simp] lemma fin_succ_equiv_symm_none {n : ℕ} :
-  (fin_succ_equiv n).symm none = 0 := rfl
+  (fin_succ_equiv n).symm none = 0 :=
+by cases n; refl
 
 @[simp] lemma fin_succ_equiv_symm_some {n : ℕ} (m : fin n) :
-  (fin_succ_equiv n).symm (some m) = m.succ := rfl
+  (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
+end
+
+@[simp] lemma fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :
+  (fin_succ_equiv n).symm m = m.succ :=
+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
 
 /-- Equivalence between `fin m ⊕ fin n` and `fin (m + n)` -/
 def sum_fin_sum_equiv : fin m ⊕ fin n ≃ fin (m + n) :=

src/data/fin.lean

@@ -566,12 +566,12 @@ lemma cast_succ_lt_last (a : fin n) : cast_succ a < last n := lt_iff_coe_lt_coe.
 @[simp] lemma cast_succ_zero : cast_succ (0 : fin (n + 1)) = 0 := rfl
 
 /-- `cast_succ i` is positive when `i` is positive -/
-lemma cast_succ_pos (i : fin (n + 1)) (h : 0 < i) : 0 < cast_succ i :=
+lemma cast_succ_pos {i : fin (n + 1)} (h : 0 < i) : 0 < cast_succ i :=
 by simpa [lt_iff_coe_lt_coe] using h
 
 lemma cast_succ_fin_succ (n : ℕ) (j : fin n) :
   cast_succ (fin.succ j) = fin.succ (cast_succ j) :=
-by { simp [fin.ext_iff], }
+by simp [fin.ext_iff]
 
 @[norm_cast, simp] lemma coe_eq_cast_succ : (a : fin (n + 1)) = a.cast_succ :=
 begin
@@ -762,6 +762,10 @@ def sub_nat (m) (i : fin (n + m)) (h : m ≤ (i : ℕ)) : fin n :=
 @[simp] lemma coe_sub_nat (i : fin (n + m)) (h : m ≤ i) : (i.sub_nat m h : ℕ) = i - m :=
 rfl
 
+@[simp] lemma pred_cast_succ_succ (i : fin n) :
+  pred (cast_succ i.succ) (ne_of_gt (cast_succ_pos i.succ_pos)) = i.cast_succ :=
+by simp [eq_iff_veq]
+
 end pred
 
 section succ_above
@@ -852,7 +856,7 @@ end
 lemma succ_above_pos (p : fin (n + 2)) (i : fin (n + 1)) (h : 0 < i) : 0 < p.succ_above i :=
 begin
   by_cases H : i.cast_succ < p,
-  { simpa [succ_above_below _ _ H] using cast_succ_pos _ h },
+  { simpa [succ_above_below _ _ H] using cast_succ_pos h },
   { simpa [succ_above_above _ _ (le_of_not_lt H)] using succ_pos _ },
 end
 
@@ -957,6 +961,22 @@ begin
   simp [cast_pred, pred_above, this]
 end
 
+lemma pred_above_below (p : fin (n + 1)) (i : fin (n + 2)) (h : i ≤ p.cast_succ) :
+  p.pred_above i = i.cast_pred :=
+begin
+  have : i ≤ (last n).cast_succ := h.trans p.le_last,
+  simp [pred_above, cast_pred, h.not_lt, this.not_lt]
+end
+
+@[simp] lemma pred_above_last : pred_above (fin.last n) = cast_pred := rfl
+
+lemma pred_above_last_apply (i : fin n) : pred_above (fin.last n) i = i.cast_pred :=
+by rw pred_above_last
+
+lemma pred_above_above (p : fin n) (i : fin (n + 1)) (h : p.cast_succ < i) :
+  p.pred_above i = i.pred (p.cast_succ.zero_le.trans_lt h).ne.symm :=
+by simp [pred_above, h]
+
 lemma cast_pred_monotone : monotone (@cast_pred n) :=
 pred_above_right_monotone (last _)
 

src/data/mv_polynomial/equiv.lean

@@ -302,14 +302,12 @@ begin
     dsimp [ring_equiv.coe_to_ring_hom, fin_succ_equiv, option_equiv_left, sum_ring_equiv],
     simp only [sum_to_iter_C, eval₂_C, rename_C, ring_hom.coe_comp] },
   { intro i,
-    dsimp [ring_equiv.coe_to_ring_hom, fin_succ_equiv, option_equiv_left, sum_ring_equiv,
-      _root_.fin_succ_equiv],
-    by_cases hi : i = 0,
-    { simp only [hi, fin.cases_zero, sum.swap, rename_X, equiv.option_equiv_sum_punit_none,
-        equiv.sum_comm_apply, comp_app, sum_to_iter_Xl, eval₂_X] },
-    { rw [← fin.succ_pred i hi],
-      simp only [rename_X, equiv.sum_comm_apply, comp_app, eval₂_X,
-        equiv.option_equiv_sum_punit_some, sum.swap, fin.cases_succ, sum_to_iter_Xr, eval₂_C] } }
+    dsimp [fin_succ_equiv, option_equiv_left, sum_ring_equiv],
+    refine fin.cases _ (λ _, _) i,
+    { simp only [fin.cases_zero, sum.swap, rename_X, equiv.option_equiv_sum_punit_none,
+                 equiv.sum_comm_apply, comp_app, sum_to_iter_Xl, eval₂_X, fin_succ_equiv_zero] },
+    { simp only [rename_X, equiv.sum_comm_apply, comp_app, eval₂_X,  eval₂_C, fin_succ_equiv_succ,
+                 equiv.option_equiv_sum_punit_some, sum.swap, fin.cases_succ, sum_to_iter_Xr] } }
 end
 
 @[simp] lemma fin_succ_equiv_apply (n : ℕ) (p : mv_polynomial (fin (n + 1)) R) :

src/linear_algebra/linear_independent.lean

@@ -842,7 +842,13 @@ lemma linear_independent_fin_cons {n} {v : fin n → V} :
     linear_independent K v ∧ x ∉ submodule.span K (range v) :=
 begin
   rw [← linear_independent_equiv (fin_succ_equiv n).symm, linear_independent_option],
-  simp [(∘), fin_succ_equiv, option.coe_def, fin.cons_succ, *]
+  convert iff.rfl,
+  { 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
 
 lemma linear_independent.fin_cons {n} {v : fin n → V} (hv : linear_independent K v)