fix(Data/Fin/Basic): castPred consistency redefinition. (#9780)

This PR redefines castPred to be more consistent with the definition of both `pred` and `castSucc`, so that the relationship between `castSucc` and `castPred` and `succ` and `pred` becomes exactly analogous.

It also adds some supplementary and analogous lemmas designed to facilitate this.

As `castPred` is no longer dependent on `predAbove`, its definition is moved to a more appropriate place.

Author: linesthatinterlace

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -543,7 +543,8 @@ instance {n : ℕ} {i : Fin (n + 1)} : Epi (σ i) := by
     -- This was not needed before leanprover/lean4#2644
     dsimp
     rw [Fin.predAbove_below i b (by simpa only [Fin.coe_eq_castSucc] using h)]
-    simp only [len_mk, Fin.coe_eq_castSucc, Fin.castPred_castSucc]
+    simp only [len_mk, Fin.coe_eq_castSucc]
+    rfl
   · use b.succ
     -- This was not needed before leanprover/lean4#2644
     dsimp
@@ -623,12 +624,11 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
   · -- This was not needed before leanprover/lean4#2644
     dsimp
     rw [Fin.predAbove_below i x h']
-    have eq := Fin.castSucc_castPred (gt_of_gt_of_ge (Fin.castSucc_lt_last i) h')
     dsimp [δ]
-    erw [Fin.succAbove_below i.succ x.castPred _]
+    erw [Fin.succAbove_below _ _ _]
     swap
-    · rwa [eq, ← Fin.le_castSucc_iff]
-    rw [eq]
+    · exact (Fin.castSucc_lt_succ_iff.mpr h')
+    rfl
   · simp only [not_le] at h'
     let y := x.pred <| by rintro (rfl : x = 0); simp at h'
     have hy : x = y.succ := (Fin.succ_pred x _).symm
@@ -673,22 +673,18 @@ theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (
       · exfalso
         exact h₂ h'.symm
   rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
-  let z := x.castPred
-  use z
-  rw [← show Fin.castSucc z = x from
-    Fin.castSucc_castPred (lt_of_lt_of_le h₂ (Fin.le_last y))] at h₁ h₂
+  use x.castPred ((Fin.le_last _).trans_lt' h₂).ne
   apply eq_σ_comp_of_not_injective'
-  rw [Fin.castSucc_lt_iff_succ_le] at h₂
   apply le_antisymm
-  · exact θ.toOrderHom.monotone (le_of_lt (Fin.castSucc_lt_succ z))
-  · rw [h₁]
-    exact θ.toOrderHom.monotone h₂
+  · exact θ.toOrderHom.monotone (le_of_lt (Fin.castSucc_lt_succ _))
+  · rw [Fin.castSucc_castPred, h₁]
+    exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)
 #align simplex_category.eq_σ_comp_of_not_injective SimplexCategory.eq_σ_comp_of_not_injective
 
 theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))
     (i : Fin (n + 2)) (hi : ∀ x, θ.toOrderHom x ≠ i) : ∃ θ' : Δ ⟶ mk n, θ = θ' ≫ δ i := by
   by_cases h : i < Fin.last (n + 1)
-  · use θ ≫ σ (Fin.castPred i)
+  · use θ ≫ σ (Fin.castPred i h.ne)
     ext1
     ext1
     ext1 x
@@ -699,23 +695,18 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
       -- This was not needed before leanprover/lean4#2644
       dsimp
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [Fin.predAbove_below (Fin.castPred i) (θ.toOrderHom x)
-          (by simpa [Fin.castSucc_castPred h] using h')]
+      erw [Fin.predAbove_below _ _ (by exact h')]
       dsimp [δ]
       erw [Fin.succAbove_below i]
       swap
-      · simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc]
-        exact
-          lt_of_le_of_lt (Fin.coe_castPred_le_self _)
-            (Fin.lt_iff_val_lt_val.mp ((Ne.le_iff_lt (hi x)).mp h'))
-      rw [Fin.castSucc_castPred]
-      apply lt_of_le_of_lt h' h
+      · rw [(hi x).le_iff_lt] at h'
+        exact h'
+      rfl
     · simp only [not_le] at h'
       -- The next three tactics used to be a simp only call before leanprover/lean4#2644
       rw [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk, OrderHom.coe_mk]
       erw [OrderHom.coe_mk]
-      erw [Fin.predAbove_above (Fin.castPred i) (θ.toOrderHom x)
-          (by simpa only [Fin.castSucc_castPred h] using h')]
+      erw [Fin.predAbove_above _ _ (by exact h')]
       dsimp [δ]
       rw [Fin.succAbove_above i _]
       -- This was not needed before leanprover/lean4#2644
@@ -725,11 +716,12 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
         Nat.le_sub_one_of_lt (Fin.lt_iff_val_lt_val.mp h')
   · obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)
     use θ ≫ σ (Fin.last _)
-    ext x : 4
+    ext x : 3
     dsimp [δ, σ]
-    dsimp only [Fin.castPred]
-    rw [Fin.predAbove_last, Fin.succAbove_last, Fin.castSucc_castPred]
-    exact (Ne.le_iff_lt (hi x)).mp (Fin.le_last _)
+    simp_rw [Fin.succAbove_last, Fin.predAbove_last_apply]
+    split_ifs with h
+    · exact ((hi x) h).elim
+    · rfl
 #align simplex_category.eq_comp_δ_of_not_surjective' SimplexCategory.eq_comp_δ_of_not_surjective'
 
 theorem eq_comp_δ_of_not_surjective {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))