chore(Logic/Equiv/Fin/Rotate): generalize from Fin (n + 1) to Fin n (#37338)

vihdzp · vihdzp · commit 4ec5d95aa624 · 2026-03-31T03:17:44.000Z
We can infer `NeZero n` if we already have `i : Fin n`.
diff --git a/Mathlib/Geometry/Polygon/Basic.lean b/Mathlib/Geometry/Polygon/Basic.lean
@@ -84,7 +84,6 @@ theorem HasNondegenerateVertices.hasNondegenerateEdges [NeZero n] [Nontrivial R]
     (h : poly.HasNondegenerateVertices R) : poly.HasNondegenerateEdges := by
   obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
   intro i
-  simp only [finRotate_succ_apply]
   simpa using (h i).injective.ne (by decide : (0 : Fin 3) ≠ 1)
 
 theorem HasNondegenerateVertices.three_le [NeZero n] [Nontrivial R] {poly : Polygon P n}
diff --git a/Mathlib/Logic/Equiv/Fin/Rotate.lean b/Mathlib/Logic/Equiv/Fin/Rotate.lean
@@ -64,27 +64,34 @@ theorem Fin.snoc_eq_cons_rotate {α : Type*} (v : Fin n → α) (a : α) :
 theorem finRotate_one : finRotate 1 = Equiv.refl _ :=
   Subsingleton.elim _ _
 
-@[simp] theorem finRotate_succ_apply (i : Fin (n + 1)) : finRotate (n + 1) i = i + 1 := by
-  cases n
-  · exact @Subsingleton.elim (Fin 1) _ _ _
-  obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
-  · simp [finRotate_last]
-  · cases i
-    simp only [Fin.lt_def, Fin.val_last] at h
-    simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]
+@[simp]
+theorem finRotate_apply (i : Fin n) : haveI := i.neZero; finRotate n i = i + 1 := by
+  match n with
+  | 0 => exact i.elim0
+  | 1 => exact @Subsingleton.elim (Fin 1) _ _ _
+  | n + 2 =>
+    obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
+    · simp [finRotate_last]
+    · cases i
+      simp only [Fin.lt_def, Fin.val_last] at h
+      simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]
+
+@[deprecated finRotate_apply (since := "2026-03-29")]
+theorem finRotate_succ_apply (i : Fin (n + 1)) : finRotate (n + 1) i = i + 1 := by
+  simp
 
 theorem finRotate_apply_zero : finRotate n.succ 0 = 1 := by
   simp
 
 theorem coe_finRotate_of_ne_last {i : Fin n.succ} (h : i ≠ Fin.last n) :
     (finRotate (n + 1) i : ℕ) = i + 1 := by
-  rw [finRotate_succ_apply]
+  rw [finRotate_apply]
   have : (i : ℕ) < n := Fin.val_lt_last h
   exact Fin.val_add_one_of_lt this
 
 theorem coe_finRotate (i : Fin n.succ) :
     (finRotate n.succ i : ℕ) = if i = Fin.last n then (0 : ℕ) else i + 1 := by
-  rw [finRotate_succ_apply, Fin.val_add_one i]
+  rw [finRotate_apply, Fin.val_add_one i]
 
 theorem lt_finRotate_iff_ne_last (i : Fin (n + 1)) :
     i < finRotate _ i ↔ i ≠ Fin.last n := by
@@ -95,14 +102,19 @@ theorem lt_finRotate_iff_ne_neg_one [NeZero n] (i : Fin n) :
   obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
   rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]
 
-@[simp] lemma finRotate_succ_symm_apply [NeZero n] (i : Fin n) : (finRotate _).symm i = i - 1 := by
-  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
+@[simp]
+lemma finRotate_symm_apply (i : Fin n) : haveI := i.neZero; (finRotate _).symm i = i - 1 := by
+  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero i.pos.ne'
   apply (finRotate n.succ).symm_apply_eq.mpr
-  rw [finRotate_succ_apply, sub_add_cancel]
+  rw [finRotate_apply, sub_add_cancel]
+
+@[deprecated finRotate_symm_apply (since := "2026-03-29")]
+lemma finRotate_succ_symm_apply [NeZero n] (i : Fin n) : (finRotate _).symm i = i - 1 := by
+  simp
 
 lemma coe_finRotate_symm_of_ne_zero [NeZero n] {i : Fin n} (hi : i ≠ 0) :
     ((finRotate _).symm i : ℕ) = i - 1 := by
-  rwa [finRotate_succ_symm_apply, Fin.val_sub_one_of_ne_zero]
+  rwa [finRotate_symm_apply, Fin.val_sub_one_of_ne_zero]
 
 theorem finRotate_symm_lt_iff_ne_zero [NeZero n] (i : Fin n) :
     (finRotate _).symm i < i ↔ i ≠ 0 := by
@@ -128,5 +140,5 @@ lemma finCycle_eq_finRotate_iterate {k : Fin n} : finCycle k = (finRotate n)^[k.
     | zero => simp
     | succ k ih =>
       rw [Fin.val_eq_val, Fin.val_castSucc] at ih
-      rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_succ_apply,
+      rw [Fin.val_succ, Function.iterate_succ', Function.comp_apply, ← ih, finRotate_apply,
         finCycle_apply, finCycle_apply, add_assoc, Fin.coeSucc_eq_succ]
