refactor(data/fin): drop fin.cast_add_right (#9371)

This was a duplicate of `fin.nat_add`. Also simplify some definitions of equivalences.

Author: urkud

src/data/equiv/fin.lean

@@ -44,7 +44,7 @@ def fin_two_equiv : fin 2 ≃ bool :=
 
 /-- The 'identity' equivalence between `fin n` and `fin m` when `n = m`. -/
 def fin_congr {n m : ℕ} (h : n = m) : fin n ≃ fin m :=
-equiv.subtype_equiv_right (λ x, by subst h)
+(fin.cast h).to_equiv
 
 @[simp] lemma fin_congr_apply_mk {n m : ℕ} (h : n = m) (k : ℕ) (w : k < n) :
   fin_congr h ⟨k, w⟩ = ⟨k, by { subst h, exact w }⟩ :=
@@ -66,64 +66,40 @@ 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 + 1)) :
   fin (n + 1) ≃ option (fin n) :=
-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)),
+{ to_fun := i.insert_nth none some,
   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] } } } }
+  left_inv := λ x, fin.succ_above_cases i (by simp) (λ j, by simp) x,
+  right_inv := λ x, by cases x; dsimp; simp }
 
 @[simp] lemma fin_succ_equiv'_at {n : ℕ} (i : fin (n + 1)) :
   (fin_succ_equiv' i) i = none := by simp [fin_succ_equiv']
 
+@[simp] lemma fin_succ_equiv'_succ_above {n : ℕ} (i : fin (n + 1)) (j : fin n) :
+  fin_succ_equiv' i (i.succ_above j) = some j :=
+@fin.insert_nth_apply_succ_above n (λ _, option (fin n)) 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 :=
-by simp [fin_succ_equiv', dif_neg (not_lt_of_gt h), ne_of_lt h]
+by rw [← fin.succ_above_below _ _ h, fin_succ_equiv'_succ_above]
 
 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 :=
-by simp [fin_succ_equiv', fin.le_cast_succ_iff, *] at *
+by rw [← fin.succ_above_above _ _ h, fin_succ_equiv'_succ_above]
 
 @[simp] lemma fin_succ_equiv'_symm_none {n : ℕ} (i : fin (n + 1)) :
   (fin_succ_equiv' i).symm none = i := rfl
 
+@[simp] lemma fin_succ_equiv'_symm_some {n : ℕ} (i : fin (n + 1)) (j : fin n) :
+  (fin_succ_equiv' i).symm (some j) = i.succ_above j :=
+rfl
+
 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]
+fin.succ_above_below i m h
 
 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]
+fin.succ_above_above i m h
 
 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 :=
@@ -145,21 +121,15 @@ by cases n; refl
 
 @[simp] lemma fin_succ_equiv_succ {n : ℕ} (m : fin n):
   (fin_succ_equiv n) m.succ = some m :=
-begin
-  cases n, { exact m.elim0 },
-  rw [fin_succ_equiv, fin_succ_equiv'_above (fin.zero_le _)],
-end
+fin_succ_equiv'_above (fin.zero_le _)
 
 @[simp] lemma fin_succ_equiv_symm_none {n : ℕ} :
   (fin_succ_equiv n).symm none = 0 :=
-by cases n; refl
+fin_succ_equiv'_symm_none _
 
 @[simp] lemma fin_succ_equiv_symm_some {n : ℕ} (m : fin n) :
   (fin_succ_equiv n).symm (some m) = m.succ :=
-begin
-  cases n, { exact m.elim0 },
-  rw [fin_succ_equiv, fin_succ_equiv'_symm_some_above (fin.zero_le _)],
-end
+congr_fun fin.succ_above_zero m
 
 @[simp] lemma fin_succ_equiv_symm_coe {n : ℕ} (m : fin n) :
   (fin_succ_equiv n).symm m = m.succ :=
@@ -195,76 +165,49 @@ 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) :=
-{ to_fun := λ x, sum.rec_on x
-    (λ y, ⟨y.1, nat.lt_of_lt_of_le y.2 $ nat.le_add_right m n⟩)
-    (λ y, ⟨m + y.1, nat.add_lt_add_left y.2 m⟩),
-  inv_fun := λ x, if H : x.1 < m
-    then sum.inl ⟨x.1, H⟩
-    else sum.inr ⟨x.1 - m, nat.lt_of_add_lt_add_left $
-      show m + (x.1 - m) < m + n,
-      from (nat.add_sub_of_le $ le_of_not_gt H).symm ▸ x.2⟩,
-  left_inv := λ x, begin
-    cases x with y y,
-    { simp [fin.ext_iff, y.is_lt], },
-    { have H : ¬m + y.val < m := not_lt_of_ge (nat.le_add_right _ _),
-      simp [H, nat.add_sub_cancel_left, fin.ext_iff] }
-  end,
-  right_inv := λ x, begin
-    by_cases H : (x:ℕ) < m,
-    { dsimp, rw [dif_pos H], simp },
-    { dsimp, rw [dif_neg H], simp [fin.ext_iff, nat.add_sub_of_le (le_of_not_gt H)] }
-  end }
+{ to_fun := sum.elim (fin.cast_add n) (fin.nat_add m),
+  inv_fun := λ i, @fin.add_cases m n (λ _, fin m ⊕ fin n) sum.inl sum.inr i,
+  left_inv := λ x, by { cases x with y y; dsimp; simp },
+  right_inv := λ x, by refine fin.add_cases (λ i, _) (λ i, _) x; simp }
 
 @[simp] lemma fin_sum_fin_equiv_apply_left (i : fin m) :
   (fin_sum_fin_equiv (sum.inl i) : fin (m + n)) = fin.cast_add n i := rfl
 
 @[simp] lemma fin_sum_fin_equiv_apply_right (i : fin n) :
-  (fin_sum_fin_equiv (sum.inr i) : fin (m + n)) = fin.cast_add_right m i := rfl
+  (fin_sum_fin_equiv (sum.inr i) : fin (m + n)) = fin.nat_add m i := rfl
 
-@[simp] lemma fin_sum_fin_equiv_symm_apply_left (x : fin (m + n)) (h : ↑x < m) :
-  fin_sum_fin_equiv.symm x = sum.inl ⟨x.1, h⟩ :=
-by simp [fin_sum_fin_equiv, dif_pos h]
+@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add (x : fin m) :
+  fin_sum_fin_equiv.symm (fin.cast_add n x) = sum.inl x :=
+fin_sum_fin_equiv.symm_apply_apply (sum.inl x)
 
-@[simp] lemma fin_sum_fin_equiv_symm_apply_right (x : fin (m + n)) (h : m ≤ ↑x) :
-  fin_sum_fin_equiv.symm x = sum.inr ⟨x.1 - m, nat.lt_of_add_lt_add_left $
-      show m + (x.1 - m) < m + n, from (nat.add_sub_of_le $ h).symm ▸ x.2⟩ :=
-by simp [fin_sum_fin_equiv, dif_neg (not_lt.mpr h)]
-
-@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add {m n : ℕ} (i : fin m) :
-  fin_sum_fin_equiv.symm (fin.cast_add n i) = sum.inl i :=
-begin
-  rw [fin_sum_fin_equiv_symm_apply_left _ (fin.cast_add_lt _ _)],
-  simp
-end
-
-@[simp] lemma fin_sum_fin_equiv_symm_apply_cast_add_right {m n : ℕ} (i : fin m) :
-  fin_sum_fin_equiv.symm (fin.cast_add_right n i) = sum.inr i :=
-begin
-  rw [fin_sum_fin_equiv_symm_apply_right _ (fin.le_cast_add_right _ _)],
-  simp
-end
+@[simp] lemma fin_sum_fin_equiv_symm_apply_nat_add (x : fin n) :
+  fin_sum_fin_equiv.symm (fin.nat_add m x) = sum.inr x :=
+fin_sum_fin_equiv.symm_apply_apply (sum.inr x)
 
 /-- The equivalence between `fin (m + n)` and `fin (n + m)` which rotates by `n`. -/
 def fin_add_flip : fin (m + n) ≃ fin (n + m) :=
 (fin_sum_fin_equiv.symm.trans (equiv.sum_comm _ _)).trans fin_sum_fin_equiv
 
-@[simp] lemma fin_add_flip_apply_left {k : ℕ} (h : k < m)
+@[simp] lemma fin_add_flip_apply_cast_add (k : fin m) (n : ℕ) :
+  fin_add_flip (fin.cast_add n k) = fin.nat_add n k :=
+by simp [fin_add_flip]
+
+@[simp] lemma fin_add_flip_apply_nat_add (k : fin n) (m : ℕ) :
+  fin_add_flip (fin.nat_add m k) = fin.cast_add m k :=
+by simp [fin_add_flip]
+
+@[simp] lemma fin_add_flip_apply_mk_left {k : ℕ} (h : k < m)
   (hk : k < m + n := nat.lt_add_right k m n h)
   (hnk : n + k < n + m := add_lt_add_left h n) :
   fin_add_flip (⟨k, hk⟩ : fin (m + n)) = ⟨n + k, hnk⟩ :=
-begin
-  dsimp [fin_add_flip, fin_sum_fin_equiv],
-  rw [dif_pos h],
-  refl,
-end
+by convert fin_add_flip_apply_cast_add ⟨k, h⟩ n
 
-@[simp] lemma fin_add_flip_apply_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
-  fin_add_flip (⟨k, h₂⟩ : fin (m + n)) =
-    ⟨k - m, lt_of_le_of_lt (nat.sub_le _ _) (by { convert h₂ using 1, simp [add_comm] })⟩ :=
+@[simp] lemma fin_add_flip_apply_mk_right {k : ℕ} (h₁ : m ≤ k) (h₂ : k < m + n) :
+  fin_add_flip (⟨k, h₂⟩ : fin (m + n)) = ⟨k - m, sub_le_self'.trans_lt $ add_comm m n ▸ h₂⟩ :=
 begin
-  dsimp [fin_add_flip, fin_sum_fin_equiv],
-  rw [dif_neg (not_lt.mpr h₁)],
-  refl,
+  convert fin_add_flip_apply_nat_add ⟨k - m, (sub_lt_iff_right h₁).2 _⟩ m,
+  { simp [nat.add_sub_cancel' h₁] },
+  { rwa add_comm }
 end
 
 /-- Rotate `fin n` one step to the right. -/
@@ -282,7 +225,7 @@ end
 lemma fin_rotate_last' : fin_rotate (n+1) ⟨n, lt_add_one _⟩ = ⟨0, nat.zero_lt_succ _⟩ :=
 begin
   dsimp [fin_rotate],
-  rw fin_add_flip_apply_right,
+  rw fin_add_flip_apply_mk_right,
   simp,
 end