feat(data/fin): fin.succ_cast_succ (#8828)

leanprover-community · Aug 26, 2021 · bafeccf · bafeccf
1 parent cb1932d
commit bafeccf
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/fin.lean b/src/data/fin.lean
@@ -695,6 +695,10 @@ begin
   exact congr_arg coe (equiv.apply_of_injective_symm _ _ _)
 end
 
+lemma succ_cast_succ {n : ℕ} (i : fin n) :
+  i.cast_succ.succ = i.succ.cast_succ :=
+fin.ext (by simp)
+
 /-- `add_nat m i` adds `m` to `i`, generalizes `fin.succ`. -/
 def add_nat (m) : fin n ↪o fin (n + m) :=
 order_embedding.of_strict_mono (λ i, ⟨(i : ℕ) + m, add_lt_add_right i.2 _⟩) $