Successors and predecessor operations of Fin n

This file contains a number of definitions and lemmas related to Fin.succ, Fin.pred, and related operations on Fin n.

Main definitions

• finCongr : Fin.cast as an Equiv, equivalence between Fin n and Fin m when n = m;
• Fin.succAbove : embeds Fin n into Fin (n + 1) skipping p.
• Fin.predAbove : the (partial) inverse of Fin.succAbove.

succ and casts into larger Fin types

theorem Fin.succ_injective (n : ℕ) : Function.Injective succ

@[simp]

theorem Fin.exists_succ_eq {n : ℕ} {x : Fin (n + 1)} : (∃ (y : Fin n), y.succ = x) ↔ x ≠ 0

theorem Fin.exists_succ_eq_of_ne_zero {n : ℕ} {x : Fin (n + 1)} (h : x ≠ 0) : ∃ (y : Fin n), y.succ = x

@[simp]

theorem Fin.succ_zero_eq_one' {n : ℕ} [NeZero n] : succ 0 = 1

theorem Fin.one_pos' {n : ℕ} [NeZero n] : 0 < 1

theorem Fin.zero_ne_one' {n : ℕ} [NeZero n] : 0 ≠ 1

@[simp]

theorem Fin.succ_one_eq_two' {n : ℕ} [NeZero n] : succ 1 = 2

The Fin.succ_one_eq_two in Lean only applies in Fin (n+2). This one instead uses a NeZero n typeclass hypothesis.

@[simp]

theorem Fin.le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} : k ≤ 0 ↔ k = 0

The Fin.le_zero_iff in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

@[simp]

theorem Fin.castLE_inj {n m : ℕ} {hmn : m ≤ n} {a b : Fin m} : castLE hmn a = castLE hmn b ↔ a = b

@[simp]

theorem Fin.castAdd_inj {n m : ℕ} {a b : Fin m} : castAdd n a = castAdd n b ↔ a = b

theorem Fin.castLE_injective {n m : ℕ} (hmn : m ≤ n) : Function.Injective (castLE hmn)

theorem Fin.castAdd_injective (m n : ℕ) : Function.Injective (castAdd n)

theorem Fin.castSucc_injective (n : ℕ) : Function.Injective castSucc

@[simp]

theorem Fin.castLE_castSucc {n m : ℕ} (i : Fin n) (h : n + 1 ≤ m) : castLE h i.castSucc = castLE ⋯ i

@[simp]

theorem Fin.castLE_comp_castSucc {n m : ℕ} (h : n + 1 ≤ m) : castLE h ∘ castSucc = castLE ⋯

@[simp]

theorem Fin.castLE_rfl (n : ℕ) : castLE ⋯ = id

@[simp]

theorem Fin.range_castLE {n k : ℕ} (h : n ≤ k) : Set.range (castLE h) = {i : Fin k | ↑i < n}

@[simp]

theorem Fin.coe_of_injective_castLE_symm {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi : i ∈ Set.range (castLE h)) : ↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

theorem Fin.leftInverse_cast {n m : ℕ} (eq : n = m) : Function.LeftInverse (Fin.cast ⋯) (Fin.cast eq)

theorem Fin.rightInverse_cast {n m : ℕ} (eq : n = m) : Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)

@[simp]

theorem Fin.cast_inj {n m : ℕ} (eq : n = m) {a b : Fin n} : Fin.cast eq a = Fin.cast eq b ↔ a = b

@[simp]

theorem Fin.cast_lt_cast {n m : ℕ} (eq : n = m) {a b : Fin n} : Fin.cast eq a < Fin.cast eq b ↔ a < b

@[simp]

theorem Fin.cast_le_cast {n m : ℕ} (eq : n = m) {a b : Fin n} : Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b

def finCongr {n m : ℕ} (eq : n = m) : Fin n ≃ Fin m

The 'identity' equivalence between Fin m and Fin n when m = n.

Equations

• finCongr eq = { toFun := Fin.cast eq, invFun := Fin.cast ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem finCongr_symm_apply {n m : ℕ} (eq : n = m) (i : Fin m) : (finCongr eq).symm i = Fin.cast ⋯ i

@[simp]

theorem finCongr_apply {n m : ℕ} (eq : n = m) (i : Fin n) : (finCongr eq) i = Fin.cast eq i

@[simp]

theorem finCongr_apply_mk {n m : ℕ} (h : m = n) (k : ℕ) (hk : k < m) : (finCongr h) ⟨k, hk⟩ = ⟨k, ⋯⟩

@[simp]

theorem finCongr_refl {n : ℕ} (h : n = n := ⋯) : finCongr h = Equiv.refl (Fin n)

@[simp]

theorem finCongr_symm {n m : ℕ} (h : m = n) : (finCongr h).symm = finCongr ⋯

@[simp]

theorem finCongr_apply_coe {n m : ℕ} (h : m = n) (k : Fin m) : ↑((finCongr h) k) = ↑k

theorem finCongr_symm_apply_coe {n m : ℕ} (h : m = n) (k : Fin n) : ↑((finCongr h).symm k) = ↑k

theorem finCongr_eq_equivCast {n m : ℕ} (h : n = m) : finCongr h = Equiv.cast ⋯

While in many cases finCongr is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

theorem Fin.cast_eq_cast {n m : ℕ} (h : n = m) : Fin.cast h = cast ⋯

While in many cases Fin.cast is better than Equiv.cast/cast, sometimes we want to apply a generic theorem about cast.

theorem Fin.castSucc_le_succ {n : ℕ} (i : Fin n) : i.castSucc ≤ i.succ

@[simp]

theorem Fin.castSucc_le_castSucc_iff {n : ℕ} {a b : Fin n} : a.castSucc ≤ b.castSucc ↔ a ≤ b

@[simp]

theorem Fin.succ_le_castSucc_iff {n : ℕ} {a b : Fin n} : a.succ ≤ b.castSucc ↔ a < b

@[simp]

theorem Fin.castSucc_lt_succ_iff {n : ℕ} {a b : Fin n} : a.castSucc < b.succ ↔ a ≤ b

theorem Fin.le_of_castSucc_lt_of_succ_lt {n : ℕ} {a b : Fin (n + 1)} {i : Fin n} (hl : i.castSucc < a) (hu : b < i.succ) : b < a

theorem Fin.castSucc_lt_or_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.castSucc < p ∨ p < i.succ

theorem Fin.succ_le_or_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : i.succ ≤ p ∨ p ≤ i.castSucc

theorem Fin.eq_castSucc_of_ne_last {n : ℕ} {x : Fin (n + 1)} (h : x ≠ last n) : ∃ (y : Fin n), y.castSucc = x

theorem Fin.forall_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} : (∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P i.castSucc) ∧ P (last n)

theorem Fin.eq_castSucc_or_eq_last {n : ℕ} (i : Fin (n + 1)) : (∃ (j : Fin n), i = j.castSucc) ∨ i = last n

@[simp]

theorem Fin.castSucc_ne_last {n : ℕ} (i : Fin n) : i.castSucc ≠ last n

theorem Fin.exists_fin_succ' {n : ℕ} {P : Fin (n + 1) → Prop} : (∃ (i : Fin (n + 1)), P i) ↔ (∃ (i : Fin n), P i.castSucc) ∨ P (last n)

@[simp]

theorem Fin.castSucc_zero' {n : ℕ} [NeZero n] : castSucc 0 = 0

The Fin.castSucc_zero in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

@[simp]

theorem Fin.castSucc_pos_iff {n : ℕ} [NeZero n] {i : Fin n} : 0 < i.castSucc ↔ 0 < i

theorem Fin.castSucc_pos' {n : ℕ} [NeZero n] {i : Fin n} : 0 < i → 0 < i.castSucc

castSucc i is positive when i is positive.

The Fin.castSucc_pos in Lean only applies in Fin (n+1). This one instead uses a NeZero n typeclass hypothesis.

@[deprecated Fin.castSucc_eq_zero_iff (since := "2025-05-13")]

theorem Fin.castSucc_eq_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) : a.castSucc = 0 ↔ a = 0

@[deprecated Fin.castSucc_ne_zero_iff (since := "2025-05-13")]

theorem Fin.castSucc_ne_zero_iff' {n : ℕ} [NeZero n] (a : Fin n) : a.castSucc ≠ 0 ↔ a ≠ 0

theorem Fin.castSucc_ne_zero_of_lt {n : ℕ} {p i : Fin n} (h : p < i) : i.castSucc ≠ 0

theorem Fin.succ_ne_last_iff {n : ℕ} (a : Fin (n + 1)) : a.succ ≠ last (n + 1) ↔ a ≠ last n

theorem Fin.succ_ne_last_of_lt {n : ℕ} {p i : Fin n} (h : i < p) : i.succ ≠ last n

@[simp]

theorem Fin.coe_eq_castSucc {n : ℕ} {a : Fin n} : ↑↑a = a.castSucc

theorem Fin.coe_succ_lt_iff_lt {n : ℕ} {j k : Fin n} : ↑↑j < ↑↑k ↔ j < k

@[simp]

theorem Fin.range_castSucc {n : ℕ} : Set.range castSucc = {i : Fin n.succ | ↑i < n}

@[simp]

theorem Fin.coe_of_injective_castSucc_symm {n : ℕ} (i : Fin n.succ) (hi : i ∈ Set.range castSucc) : ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i

theorem Fin.castSucc_castAdd {n m : ℕ} (i : Fin n) : (castAdd m i).castSucc = castAdd (m + 1) i

theorem Fin.succ_castAdd {n m : ℕ} (i : Fin n) : (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨↑i + 1, ⋯⟩

theorem Fin.succ_natAdd {n m : ℕ} (i : Fin m) : (natAdd n i).succ = natAdd n i.succ

pred

theorem Fin.pred_one' {n : ℕ} [NeZero n] (h : 1 ≠ 0 := ⋯) : pred 1 h = 0

theorem Fin.pred_last {n : ℕ} (h : ¬last (n + 1) = 0 := ⋯) : (last (n + 1)).pred h = last n

theorem Fin.pred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : i.pred hi < j ↔ i < j.succ

theorem Fin.lt_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j < i.pred hi ↔ j.succ < i

theorem Fin.pred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : i.pred hi ≤ j ↔ i ≤ j.succ

theorem Fin.le_pred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j ≤ i.pred hi ↔ j.succ ≤ i

theorem Fin.castSucc_pred_eq_pred_castSucc {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc = a.castSucc.pred ⋯

theorem Fin.castSucc_pred_add_one_eq {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc + 1 = a

theorem Fin.le_pred_castSucc_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0) : b ≤ a.castSucc.pred ha ↔ b < a

theorem Fin.pred_castSucc_lt_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.castSucc ≠ 0) : a.castSucc.pred ha < b ↔ a ≤ b

theorem Fin.pred_castSucc_lt {n : ℕ} {a : Fin (n + 1)} (ha : a.castSucc ≠ 0) : a.castSucc.pred ha < a

theorem Fin.le_castSucc_pred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) : b ≤ (a.pred ha).castSucc ↔ b < a

theorem Fin.castSucc_pred_lt_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc < b ↔ a ≤ b

theorem Fin.castSucc_pred_lt {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) : (a.pred ha).castSucc < a

@[inline]

def Fin.castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ last n) : Fin n

castPred i sends i : Fin (n + 1) to Fin n as long as i ≠ last n.

Equations

• i.castPred h = i.castLT ⋯

@[simp]

theorem Fin.castLT_eq_castPred {n : ℕ} (i : Fin (n + 1)) (h : i < last n) (h' : ¬i = last n := ⋯) : i.castLT h = i.castPred h'

@[simp]

theorem Fin.coe_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ last n) : ↑(i.castPred h) = ↑i

@[simp]

theorem Fin.castPred_castSucc {n : ℕ} {i : Fin n} (h' : ¬i.castSucc = last n := ⋯) : i.castSucc.castPred h' = i

@[simp]

theorem Fin.castSucc_castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ last n) : (i.castPred h).castSucc = i

theorem Fin.castPred_eq_iff_eq_castSucc {n : ℕ} (i : Fin (n + 1)) (hi : i ≠ last n) (j : Fin n) : i.castPred hi = j ↔ i = j.castSucc

@[simp]

theorem Fin.castPred_mk {n : ℕ} (i : ℕ) (h₁ : i < n) (h₂ : i < n.succ := ⋯) (h₃ : ⟨i, h₂⟩ ≠ last n := ⋯) : ⟨i, h₂⟩.castPred h₃ = ⟨i, h₁⟩

@[simp]

theorem Fin.castPred_le_castPred_iff {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} : i.castPred hi ≤ j.castPred hj ↔ i ≤ j

theorem Fin.castPred_le_castPred {n : ℕ} {i j : Fin (n + 1)} (h : i ≤ j) (hj : j ≠ last n) : i.castPred ⋯ ≤ j.castPred hj

A version of the right-to-left implication of castPred_le_castPred_iff that deduces i ≠ last n from i ≤ j and j ≠ last n.

@[simp]

theorem Fin.castPred_lt_castPred_iff {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} : i.castPred hi < j.castPred hj ↔ i < j

theorem Fin.castPred_lt_castPred {n : ℕ} {i j : Fin (n + 1)} (h : i < j) (hj : j ≠ last n) : i.castPred ⋯ < j.castPred hj

A version of the right-to-left implication of castPred_lt_castPred_iff that deduces i ≠ last n from i < j.

theorem Fin.castPred_lt_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) : i.castPred hi < j ↔ i < j.castSucc

theorem Fin.lt_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) : j < i.castPred hi ↔ j.castSucc < i

theorem Fin.castPred_le_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) : i.castPred hi ≤ j ↔ i ≤ j.castSucc

theorem Fin.le_castPred_iff {n : ℕ} {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ last n) : j ≤ i.castPred hi ↔ j.castSucc ≤ i

@[simp]

theorem Fin.castPred_inj {n : ℕ} {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} : i.castPred hi = j.castPred hj ↔ i = j

@[simp]

theorem Fin.castPred_zero {n : ℕ} [NeZero n] : castPred 0 ⋯ = 0

@[deprecated Fin.castPred_zero (since := "2025-05-11")]

theorem Fin.castPred_zero' {n : ℕ} [NeZero n] : castPred 0 ⋯ = 0

Alias of Fin.castPred_zero.

@[simp]

theorem Fin.castPred_eq_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (h : i ≠ last n) : i.castPred h = 0 ↔ i = 0

theorem Fin.castPred_ne_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (h₁ : i ≠ last n) (h₂ : i ≠ 0) : i.castPred h₁ ≠ 0

@[simp]

theorem Fin.castPred_one {n : ℕ} [NeZero n] : castPred 1 ⋯ = 1

theorem Fin.succ_castPred_eq_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ last n) (ha' : a.succ ≠ last (n + 1) := ⋯) : (a.castPred ha).succ = a.succ.castPred ha'

theorem Fin.succ_castPred_eq_add_one {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ last n) : (a.castPred ha).succ = a + 1

theorem Fin.castpred_succ_le_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ last (n + 1)) : a.succ.castPred ha ≤ b ↔ a < b

theorem Fin.lt_castPred_succ_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ last (n + 1)) : b < a.succ.castPred ha ↔ b ≤ a

theorem Fin.lt_castPred_succ {n : ℕ} {a : Fin (n + 1)} (ha : a.succ ≠ last (n + 1)) : a < a.succ.castPred ha

theorem Fin.succ_castPred_le_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ last n) : (a.castPred ha).succ ≤ b ↔ a < b

theorem Fin.lt_succ_castPred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ last n) : b < (a.castPred ha).succ ↔ b ≤ a

theorem Fin.lt_succ_castPred {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ last n) : a < (a.castPred ha).succ

theorem Fin.castPred_le_pred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ last n) (hb : b ≠ 0) : a.castPred ha ≤ b.pred hb ↔ a < b

theorem Fin.pred_lt_castPred_iff {n : ℕ} {a b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ last n) : a.pred ha < b.castPred hb ↔ a ≤ b

theorem Fin.pred_lt_castPred {n : ℕ} {a : Fin (n + 1)} (h₁ : a ≠ 0) (h₂ : a ≠ last n) : a.pred h₁ < a.castPred h₂

def Fin.succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1)

succAbove p i embeds Fin n into Fin (n + 1) with a hole around p.

Equations

• p.succAbove i = if i.castSucc < p then i.castSucc else i.succ

theorem Fin.succAbove_of_castSucc_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.castSucc < p) : p.succAbove i = i.castSucc

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) embeds i by castSucc when the resulting i.castSucc < p.

theorem Fin.succAbove_of_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : i.succ ≤ p) : p.succAbove i = i.castSucc

theorem Fin.succAbove_of_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p ≤ i.castSucc) : p.succAbove i = i.succ

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 Fin.succAbove_of_lt_succ {n : ℕ} (p : Fin (n + 1)) (i : Fin n) (h : p < i.succ) : p.succAbove i = i.succ

theorem Fin.succAbove_succ_of_lt {n : ℕ} (p i : Fin n) (h : p < i) : p.succ.succAbove i = i.succ

theorem Fin.succAbove_succ_of_le {n : ℕ} (p i : Fin n) (h : i ≤ p) : p.succ.succAbove i = i.castSucc

@[simp]

theorem Fin.succAbove_succ_self {n : ℕ} (j : Fin n) : j.succ.succAbove j = j.castSucc

theorem Fin.succAbove_castSucc_of_lt {n : ℕ} (p i : Fin n) (h : i < p) : p.castSucc.succAbove i = i.castSucc

theorem Fin.succAbove_castSucc_of_le {n : ℕ} (p i : Fin n) (h : p ≤ i) : p.castSucc.succAbove i = i.succ

@[simp]

theorem Fin.succAbove_castSucc_self {n : ℕ} (j : Fin n) : j.castSucc.succAbove j = j.succ

theorem Fin.succAbove_pred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : p < i) : p.succAbove (i.pred ⋯) = i

theorem Fin.succAbove_pred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hi : i ≠ 0) : p.succAbove (i.pred hi) = (i.pred hi).castSucc

@[simp]

theorem Fin.succAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ 0) : p.succAbove (p.pred h) = (p.pred h).castSucc

theorem Fin.succAbove_castPred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : i < p) : p.succAbove (i.castPred ⋯) = i

theorem Fin.succAbove_castPred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hi : i ≠ last n) : p.succAbove (i.castPred hi) = (i.castPred hi).succ

theorem Fin.succAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (h : p ≠ last n) : p.succAbove (p.castPred h) = (p.castPred h).succ

@[simp]

theorem Fin.succAbove_ne {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i ≠ p

Embedding i : Fin n into Fin (n + 1) with a hole around p : Fin (n + 1) never results in p itself

@[simp]

theorem Fin.ne_succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p ≠ p.succAbove i

theorem Fin.succAbove_right_injective {n : ℕ} {p : Fin (n + 1)} : Function.Injective p.succAbove

Given a fixed pivot p : Fin (n + 1), p.succAbove is injective.

theorem Fin.succAbove_right_inj {n : ℕ} {p : Fin (n + 1)} {i j : Fin n} : p.succAbove i = p.succAbove j ↔ i = j

Given a fixed pivot p : Fin (n + 1), p.succAbove is injective.

@[simp]

theorem Fin.succAbove_ne_zero_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} (ha : a ≠ 0) : a.succAbove 0 = 0

theorem Fin.succAbove_eq_zero_iff {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) : a.succAbove b = 0 ↔ b = 0

theorem Fin.succAbove_ne_zero {n : ℕ} [NeZero n] {a : Fin (n + 1)} {b : Fin n} (ha : a ≠ 0) (hb : b ≠ 0) : a.succAbove b ≠ 0

@[simp]

theorem Fin.succAbove_zero {n : ℕ} : succAbove 0 = succ

Embedding Fin n into Fin (n + 1) with a hole around zero embeds by succ.

theorem Fin.succAbove_zero_apply {n : ℕ} (i : Fin n) : succAbove 0 i = i.succ

@[simp]

theorem Fin.succAbove_ne_last_last {n : ℕ} {a : Fin (n + 2)} (h : a ≠ last (n + 1)) : a.succAbove (last n) = last (n + 1)

theorem Fin.succAbove_eq_last_iff {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last (n + 1)) : a.succAbove b = last (n + 1) ↔ b = last n

theorem Fin.succAbove_ne_last {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last (n + 1)) (hb : b ≠ last n) : a.succAbove b ≠ last (n + 1)

@[simp]

theorem Fin.succAbove_last {n : ℕ} : (last n).succAbove = castSucc

Embedding Fin n into Fin (n + 1) with a hole around last n embeds by castSucc.

theorem Fin.succAbove_last_apply {n : ℕ} (i : Fin n) : (last n).succAbove i = i.castSucc

theorem Fin.succAbove_lt_iff_castSucc_lt {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.castSucc < p

Embedding i : Fin n into Fin (n + 1) using a pivot p that is greater results in a value that is less than p.

theorem Fin.succAbove_lt_iff_succ_le {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAbove i < p ↔ i.succ ≤ p

theorem Fin.lt_succAbove_iff_le_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p ≤ i.castSucc

Embedding i : Fin n into Fin (n + 1) using a pivot p that is lesser results in a value that is greater than p.

theorem Fin.lt_succAbove_iff_lt_castSucc {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p < p.succAbove i ↔ p < i.succ

theorem Fin.succAbove_pos {n : ℕ} [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) : 0 < p.succAbove i

Embedding a positive Fin n results in a positive Fin (n + 1)

theorem Fin.castPred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : x.castSucc < y) (h' : y.succAbove x ≠ last n := ⋯) : (y.succAbove x).castPred h' = x

theorem Fin.pred_succAbove {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : y ≤ x.castSucc) (h' : y.succAbove x ≠ 0 := ⋯) : (y.succAbove x).pred h' = x

theorem Fin.exists_succAbove_eq {n : ℕ} {x y : Fin (n + 1)} (h : x ≠ y) : ∃ (z : Fin n), y.succAbove z = x

@[simp]

theorem Fin.exists_succAbove_eq_iff {n : ℕ} {x y : Fin (n + 1)} : (∃ (z : Fin n), x.succAbove z = y) ↔ y ≠ x

@[simp]

theorem Fin.range_succAbove {n : ℕ} (p : Fin (n + 1)) : Set.range p.succAbove = {p}ᶜ

The range of p.succAbove is everything except p.

@[simp]

theorem Fin.range_succ (n : ℕ) : Set.range succ = {0}ᶜ

theorem Fin.succAbove_left_injective {n : ℕ} : Function.Injective succAbove

succAbove is injective at the pivot

@[simp]

theorem Fin.succAbove_left_inj {n : ℕ} {x y : Fin (n + 1)} : x.succAbove = y.succAbove ↔ x = y

succAbove is injective at the pivot

@[simp]

theorem Fin.zero_succAbove {n : ℕ} (i : Fin n) : succAbove 0 i = i.succ

theorem Fin.succ_succAbove_zero {n : ℕ} [NeZero n] (i : Fin n) : i.succ.succAbove 0 = 0

@[simp]

theorem Fin.succ_succAbove_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.succ.succAbove j.succ = (i.succAbove j).succ

succ commutes with succAbove.

@[simp]

theorem Fin.castSucc_succAbove_castSucc {n : ℕ} {i : Fin (n + 1)} {j : Fin n} : i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

castSucc commutes with succAbove.

theorem Fin.pred_succAbove_pred {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0) (hk : a.succAbove b ≠ 0 := ⋯) : (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

pred commutes with succAbove.

theorem Fin.castPred_succAbove_castPred {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last (n + 1)) (hb : b ≠ last n) (hk : a.succAbove b ≠ last (n + 1) := ⋯) : (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

castPred commutes with succAbove.

theorem Fin.one_succAbove_zero {n : ℕ} : succAbove 1 0 = 0

@[simp]

theorem Fin.succ_succAbove_one {n : ℕ} [NeZero n] (i : Fin (n + 1)) : i.succ.succAbove 1 = (i.succAbove 0).succ

By moving succ to the outside of this expression, we create opportunities for further simplification using succAbove_zero or succ_succAbove_zero.

@[simp]

theorem Fin.one_succAbove_succ {n : ℕ} (j : Fin n) : succAbove 1 j.succ = j.succ.succ

@[simp]

theorem Fin.one_succAbove_one {n : ℕ} : succAbove 1 1 = 2

def Fin.predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : Fin n

predAbove p i surjects i : Fin (n+1) into Fin n by subtracting one if p < i.

Equations

• p.predAbove i = if h : p.castSucc < i then i.pred ⋯ else i.castPred ⋯

theorem Fin.predAbove_of_le_castSucc {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i ≤ p.castSucc) : p.predAbove i = i.castPred ⋯

theorem Fin.predAbove_of_lt_succ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) : p.predAbove i = i.castPred ⋯

theorem Fin.predAbove_of_castSucc_lt {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) : p.predAbove i = i.pred ⋯

theorem Fin.predAbove_of_succ_le {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.succ ≤ i) : p.predAbove i = i.pred ⋯

theorem Fin.predAbove_succ_of_lt {n : ℕ} (p i : Fin n) (h : i < p) : p.predAbove i.succ = i.succ.castPred ⋯

theorem Fin.predAbove_succ_of_le {n : ℕ} (p i : Fin n) (h : p ≤ i) : p.predAbove i.succ = i

@[simp]

theorem Fin.predAbove_succ_self {n : ℕ} (p : Fin n) : p.predAbove p.succ = p

theorem Fin.predAbove_castSucc_of_lt {n : ℕ} (p i : Fin n) (h : p < i) : p.predAbove i.castSucc = i.castSucc.pred ⋯

theorem Fin.predAbove_castSucc_of_le {n : ℕ} (p i : Fin n) (h : i ≤ p) : p.predAbove i.castSucc = i

@[simp]

theorem Fin.predAbove_castSucc_self {n : ℕ} (p : Fin n) : p.predAbove p.castSucc = p

theorem Fin.predAbove_pred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : i < p) : (p.pred ⋯).predAbove i = i.castPred ⋯

theorem Fin.predAbove_pred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : p ≤ i) (hp : p ≠ 0) : (p.pred hp).predAbove i = i.pred ⋯

theorem Fin.predAbove_pred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ 0) : (p.pred hp).predAbove p = p.pred hp

theorem Fin.predAbove_castPred_of_lt {n : ℕ} (p i : Fin (n + 1)) (h : p < i) : (p.castPred ⋯).predAbove i = i.pred ⋯

theorem Fin.predAbove_castPred_of_le {n : ℕ} (p i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ last n) : (p.castPred hp).predAbove i = i.castPred ⋯

theorem Fin.predAbove_castPred_self {n : ℕ} (p : Fin (n + 1)) (hp : p ≠ last n) : (p.castPred hp).predAbove p = p.castPred hp

@[simp]

theorem Fin.predAbove_right_zero {n : ℕ} [NeZero n] {i : Fin n} : i.predAbove 0 = 0

theorem Fin.predAbove_zero_succ {n : ℕ} [NeZero n] {i : Fin n} : predAbove 0 i.succ = i

@[simp]

theorem Fin.predAbove_zero_of_ne_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0) : predAbove 0 i = i.pred hi

theorem Fin.succ_predAbove_zero {n : ℕ} [NeZero n] {j : Fin (n + 1)} (h : j ≠ 0) : (predAbove 0 j).succ = j

theorem Fin.predAbove_zero {n : ℕ} [NeZero n] {i : Fin (n + 1)} : predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

@[simp]

theorem Fin.predAbove_right_last {n : ℕ} {i : Fin (n + 1)} : i.predAbove (last (n + 1)) = last n

theorem Fin.predAbove_last_castSucc {n : ℕ} {i : Fin (n + 1)} : (last n).predAbove i.castSucc = i

@[simp]

theorem Fin.predAbove_last_of_ne_last {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ last (n + 1)) : (last n).predAbove i = i.castPred hi

theorem Fin.predAbove_last_apply {n : ℕ} {i : Fin (n + 2)} : (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi

theorem Fin.predAbove_surjective {n : ℕ} (p : Fin n) : Function.Surjective p.predAbove

@[simp]

theorem Fin.succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.castSucc) : p.castSucc.succAbove (p.predAbove i) = i

Sending Fin (n+1) to Fin n by subtracting one from anything above p then back to Fin (n+1) with a gap around p is the identity away from p.

@[simp]

theorem Fin.succ_succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.succ) : p.succ.succAbove (p.predAbove i) = i

Sending Fin (n+1) to Fin n by subtracting one from anything above p then back to Fin (n+1) with a gap around p.succ is the identity away from p.succ.

@[simp]

theorem Fin.predAbove_succAbove {n : ℕ} (p i : Fin n) : p.predAbove (p.castSucc.succAbove i) = i

Sending Fin n into Fin (n + 1) with a gap at p then back to Fin n by subtracting one from anything above p is the identity.

@[simp]

theorem Fin.succ_predAbove_succ {n : ℕ} (a : Fin n) (b : Fin (n + 1)) : a.succ.predAbove b.succ = (a.predAbove b).succ

succ commutes with predAbove.

@[simp]

theorem Fin.castSucc_predAbove_castSucc {n : ℕ} (a : Fin n) (b : Fin (n + 1)) : a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

castSucc commutes with predAbove.

theorem Fin.predAbove_predAbove_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : (j.predAbove i).predAbove (i.succAbove j) = j

theorem Fin.succAbove_succAbove_predAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : (i.succAbove j).succAbove (j.predAbove i) = i

theorem Fin.succAbove_succAbove_succAbove_predAbove {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (k : Fin n) : (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)

Given i : Fin (n + 2) and j : Fin (n + 1), there are two ways to represent the order embedding Fin n → Fin (n + 2) leaving holes at i and i.succAbove j.

One is i.succAbove ∘ j.succAbove. It corresponds to embedding Fin n to Fin (n + 1) leaving a hole at j, then embedding the result to Fin (n + 2) leaving a hole at i. The other one is (i.succAbove j).succAbove ∘ (j.predAbove i).succAbove. It corresponds to swapping the roles of i and j.

This lemma says that these two ways are equal. It is used in Fin.removeNth_removeNth_eq_swap to show that two ways of removing 2 elements from a sequence give the same answer.