From b075cdd0e6ad8b5a3295e7484b2ae59e9b2ec2a7 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Wed, 17 Jan 2024 06:36:36 +0000 Subject: [PATCH] fix(Data/Fin/Basic): Redefine `succAbove` (#9793) Tweak to `succAbove` to make its definition consistent with that of `predAbove` --- Mathlib/Data/Fin/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 79c9c2ce16b92..504aba3c8b032 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -1555,7 +1555,7 @@ section SuccAbove /-- `succAbove p i` embeds `Fin n` into `Fin (n + 1)` with a hole around `p`. -/ def succAbove (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1) := - if i.1 < p.1 then castSucc i else succ i + if castSucc i < p then i.castSucc else i.succ theorem strictMono_succAbove (p : Fin (n + 1)) : StrictMono (succAbove p) := (castSuccEmb : Fin n ↪o _).strictMono.ite (succEmbedding n).strictMono @@ -1613,7 +1613,7 @@ theorem succAbove_last_apply (i : Fin n) : succAbove (Fin.last n) i = castSucc i /-- Embedding `i : Fin n` into `Fin (n + 1)` with a hole around `p : Fin (n + 1)` embeds `i` by `succ` when the resulting `p < i.succ`. -/ theorem succAbove_above (p : Fin (n + 1)) (i : Fin n) (h : p ≤ castSucc i) : - p.succAbove i = i.succ := by simp [le_iff_val_le_val] at h; simp [succAbove, h.not_lt] + p.succAbove i = i.succ := if_neg h.not_lt #align fin.succ_above_above Fin.succAbove_above /-- Embedding `i : Fin n` into `Fin (n + 1)` is always about some hole `p`. -/