The finite type with n elements

Fin n is the type whose elements are natural numbers smaller than n. This file expands on the development in the core library.

Main definitions

Induction principles

• finZeroElim : Elimination principle for the empty set Fin 0, generalizes Fin.elim0. Further definitions and eliminators can be found in Init.Data.Fin.Lemmas

Embeddings and isomorphisms

• Fin.valEmbedding : coercion to natural numbers as an Embedding;
• Fin.succEmb : Fin.succ as an Embedding;
• Fin.castLEEmb h : Fin.castLE as an Embedding, embed Fin n into Fin m, h : n ≤ m;
• finCongr : Fin.cast as an Equiv, equivalence between Fin n and Fin m when n = m;
• Fin.castAddEmb m : Fin.castAdd as an Embedding, embed Fin n into Fin (n+m);
• Fin.castSuccEmb : Fin.castSucc as an Embedding, embed Fin n into Fin (n+1);
• Fin.addNatEmb m i : Fin.addNat as an Embedding, add m on i on the right, generalizes Fin.succ;
• Fin.natAddEmb n i : Fin.natAdd as an Embedding, adds n on i on the left;

Other casts

• Fin.divNat i : divides i : Fin (m * n) by n;
• Fin.modNat i : takes the mod of i : Fin (m * n) by n;

def finZeroElim {α : Fin 0 → Sort u_1} (x : Fin 0) : α x

Elimination principle for the empty set Fin 0, dependent version.

Equations

• finZeroElim x = x.elim0

@[simp]

theorem Fin.mk_eq_one {n a : ℕ} {ha : a < n + 2} : ⟨a, ha⟩ = 1 ↔ a = 1

@[simp]

theorem Fin.one_eq_mk {n a : ℕ} {ha : a < n + 2} : 1 = ⟨a, ha⟩ ↔ a = 1

instance Fin.instCanLiftNatValLt {n : ℕ} : CanLift ℕ (Fin n) val fun (x : ℕ) => x < n

def Fin.rec0 {α : Fin 0 → Sort u_1} (i : Fin 0) : α i

A dependent variant of Fin.elim0.

Equations

• i.rec0 = absurd ⋯ ⋯

theorem Fin.val_injective {n : ℕ} : Function.Injective val

theorem Fin.size_positive {n : ℕ} : ∀ (a : Fin n), 0 < n

If you actually have an element of Fin n, then the n is always positive

theorem Fin.size_positive' {n : ℕ} [Nonempty (Fin n)] : 0 < n

theorem Fin.prop {n : ℕ} (a : Fin n) : ↑a < n

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

theorem Fin.ne_zero_of_lt {n : ℕ} {a b : Fin (n + 1)} (hab : a < b) : b ≠ 0

theorem Fin.ne_last_of_lt {n : ℕ} {a b : Fin (n + 1)} (hab : a < b) : a ≠ last n

def Fin.equivSubtype {n : ℕ} : Fin n ≃ { i : ℕ // i < n }

Equivalence between Fin n and { i // i < n }.

Equations

• Fin.equivSubtype = { toFun := fun (a : Fin n) => ⟨↑a, ⋯⟩, invFun := fun (a : { i : ℕ // i < n }) => ⟨↑a, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Fin.equivSubtype_apply {n : ℕ} (a : Fin n) : equivSubtype a = ⟨↑a, ⋯⟩

@[simp]

theorem Fin.equivSubtype_symm_apply {n : ℕ} (a : { i : ℕ // i < n }) : equivSubtype.symm a = ⟨↑a, ⋯⟩

coercions and constructions

theorem Fin.val_eq_val {n : ℕ} (a b : Fin n) : ↑a = ↑b ↔ a = b

theorem Fin.ne_iff_vne {n : ℕ} (a b : Fin n) : a ≠ b ↔ ↑a ≠ ↑b

theorem Fin.mk_eq_mk {n a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} : ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'

theorem Fin.heq_fun_iff {α : Sort u_1} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} : f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Assume k = l. If two functions defined on Fin k and Fin l are equal on each element, then they coincide (in the heq sense).

theorem Fin.heq_fun₂_iff {α : Sort u_1} {k l k' l' : ℕ} (h : k = l) (h' : k' = l') {f : Fin k → Fin k' → α} {g : Fin l → Fin l' → α} : f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Assume k = l and k' = l'. If two functions Fin k → Fin k' → α and Fin l → Fin l' → α are equal on each pair, then they coincide (in the heq sense).

theorem Fin.heq_ext_iff {k l : ℕ} (h : k = l) {i : Fin k} {j : Fin l} : i ≍ j ↔ ↑i = ↑j

Two elements of Fin k and Fin l are heq iff their values in ℕ coincide. This requires k = l. For the left implication without this assumption, see val_eq_val_of_heq.

order

theorem Fin.lt_or_ge {n : ℕ} (a b : Fin n) : a < b ∨ b ≤ a

Fin.lt_or_ge is an alias of Fin.lt_or_le. It is preferred since it follows the mathlib naming convention.

theorem Fin.le_or_gt {n : ℕ} (a b : Fin n) : a ≤ b ∨ b < a

Fin.le_or_gt is an alias of Fin.le_or_lt. It is preferred since it follows the mathlib naming convention.

theorem Fin.le_iff_val_le_val {n : ℕ} {a b : Fin n} : a ≤ b ↔ ↑a ≤ ↑b

@[simp]

theorem Fin.val_fin_lt {n : ℕ} {a b : Fin n} : ↑a < ↑b ↔ a < b

a < b as natural numbers if and only if a < b in Fin n.

@[simp]

theorem Fin.val_fin_le {n : ℕ} {a b : Fin n} : ↑a ≤ ↑b ↔ a ≤ b

a ≤ b as natural numbers if and only if a ≤ b in Fin n.

theorem Fin.min_val {n : ℕ} {a : Fin n} : min (↑a) n = ↑a

theorem Fin.max_val {n : ℕ} {a : Fin n} : max (↑a) n = n

def Fin.valEmbedding {n : ℕ} : Fin n ↪ ℕ

The inclusion map Fin n → ℕ is an embedding.

Equations

• Fin.valEmbedding = { toFun := Fin.val, inj' := ⋯ }

@[simp]

theorem Fin.valEmbedding_apply {n : ℕ} : ⇑valEmbedding = val

@[simp]

theorem Fin.equivSubtype_symm_trans_valEmbedding {n : ℕ} : equivSubtype.symm.toEmbedding.trans valEmbedding = Function.Embedding.subtype fun (x : ℕ) => x < n

instance Fin.instWellFoundedRelation_mathlib {n : ℕ} : WellFoundedRelation (Fin n)

Use the ordering on Fin n for checking recursive definitions.

For example, the following definition is not accepted by the termination checker, unless we declare the WellFoundedRelation instance:

def factorial {n : ℕ} : Fin n → ℕ
  | ⟨0, _⟩ := 1
  | ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩

Equations

• Fin.instWellFoundedRelation_mathlib = measure Fin.val

@[deprecated Fin.val_zero (since := "2025-02-24")]

theorem Fin.val_zero' (n : ℕ) [NeZero n] : ↑0 = 0

Alias of Fin.val_zero.

@[simp]

theorem Fin.mk_zero' (n : ℕ) [NeZero n] : ⟨0, ⋯⟩ = 0

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

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

theorem Fin.zero_le' {n : ℕ} [NeZero n] (a : Fin n) : 0 ≤ a

@[simp]

theorem Fin.val_pos_iff {n : ℕ} [NeZero n] {a : Fin n} : 0 < ↑a ↔ 0 < a

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

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

@[simp]

theorem Fin.cast_eq_self {n : ℕ} (a : Fin n) : Fin.cast ⋯ a = a

@[simp]

theorem Fin.cast_eq_zero {k l : ℕ} [NeZero k] [NeZero l] (h : k = l) (x : Fin k) : Fin.cast h x = 0 ↔ x = 0

theorem Fin.cast_injective {k l : ℕ} (h : k = l) : Function.Injective (Fin.cast h)

theorem Fin.last_pos' {n : ℕ} [NeZero n] : 0 < last n

theorem Fin.one_lt_last {n : ℕ} [NeZero n] : 1 < last (n + 1)

Coercions to ℤ and the fin_omega tactic.

theorem Fin.coe_int_sub_eq_ite {n : ℕ} (u v : Fin n) : ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

theorem Fin.coe_int_sub_eq_mod {n : ℕ} (u v : Fin n) : ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

theorem Fin.coe_int_add_eq_ite {n : ℕ} (u v : Fin n) : ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

theorem Fin.coe_int_add_eq_mod {n : ℕ} (u v : Fin n) : ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

def Fin.tacticFin_omega : Lean.ParserDescr

Preprocessor for omega to handle inequalities in Fin. Note that this involves a lot of case splitting, so may be slow.

Equations

• Fin.tacticFin_omega = Lean.ParserDescr.node `Fin.tacticFin_omega 1024 (Lean.ParserDescr.nonReservedSymbol "fin_omega" false)

addition, numerals, and coercion from Nat

@[simp]

theorem Fin.val_one' (n : ℕ) [NeZero n] : ↑1 = 1 % n

@[deprecated Fin.val_one' (since := "2025-03-10")]

theorem Fin.val_one'' {n : ℕ} : ↑1 = 1 % (n + 1)

instance Fin.nontrivial {n : ℕ} [NeZero n] : Nontrivial (Fin (n + 1))

theorem Fin.nontrivial_iff_two_le {n : ℕ} : Nontrivial (Fin n) ↔ 2 ≤ n

theorem Fin.exists_ne_and_ne_of_two_lt {n : ℕ} (i j : Fin n) (h : 2 < n) : ∃ (k : Fin n), k ≠ i ∧ k ≠ j

If working with more than two elements, we can always pick a third distinct from two existing elements.

instance Fin.inhabitedFinOneAdd (n : ℕ) : Inhabited (Fin (1 + n))

Equations

• Fin.inhabitedFinOneAdd n = inferInstance

@[simp]

theorem Fin.default_eq_zero (n : ℕ) [NeZero n] : default = 0

theorem Fin.val_add_eq_ite {n : ℕ} (a b : Fin n) : ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

theorem Fin.val_add_eq_of_add_lt {n : ℕ} {a b : Fin n} (huv : ↑a + ↑b < n) : ↑(a + b) = ↑a + ↑b

theorem Fin.intCast_val_sub_eq_sub_add_ite {n : ℕ} (a b : Fin n) : ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

theorem Fin.one_le_of_ne_zero {n : ℕ} [NeZero n] {k : Fin n} (hk : k ≠ 0) : 1 ≤ k

theorem Fin.val_sub_one_of_ne_zero {n : ℕ} [NeZero n] {i : Fin n} (hi : i ≠ 0) : ↑(i - 1) = ↑i - 1

@[simp]

theorem Fin.ofNat_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat n a = ↑a

@[deprecated Fin.ofNat_eq_cast (since := "2025-05-30")]

theorem Fin.ofNat'_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : Fin.ofNat n a = ↑a

Alias of Fin.ofNat_eq_cast.

@[simp]

theorem Fin.val_natCast (a n : ℕ) [NeZero n] : ↑↑a = a % n

theorem Fin.val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : ↑↑a = a

Converting an in-range number to Fin (n + 1) produces a result whose value is the original number.

@[simp]

theorem Fin.cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : ↑↑a = a

If n is non-zero, converting the value of a Fin n to Fin n results in the same value.

@[simp]

theorem Fin.natCast_self (n : ℕ) [NeZero n] : ↑n = 0

@[simp]

theorem Fin.natCast_eq_zero {a n : ℕ} [NeZero n] : ↑a = 0 ↔ n ∣ a

@[simp]

theorem Fin.natCast_eq_last (n : ℕ) : ↑n = last n

theorem Fin.natCast_eq_mk {m n : ℕ} (h : m < n) : have this := ⋯; ↑m = ⟨m, h⟩

theorem Fin.one_eq_mk_of_lt {n : ℕ} (h : 1 < n) : have this := ⋯; 1 = ⟨1, h⟩

theorem Fin.le_val_last {n : ℕ} (i : Fin (n + 1)) : i ≤ ↑n

theorem Fin.natCast_le_natCast {n a b : ℕ} (han : a ≤ n) (hbn : b ≤ n) : ↑a ≤ ↑b ↔ a ≤ b

theorem Fin.natCast_lt_natCast {n a b : ℕ} (han : a ≤ n) (hbn : b ≤ n) : ↑a < ↑b ↔ a < b

theorem Fin.natCast_mono {n a b : ℕ} (hbn : b ≤ n) (hab : a ≤ b) : ↑a ≤ ↑b

theorem Fin.natCast_strictMono {n a b : ℕ} (hbn : b ≤ n) (hab : a < b) : ↑a < ↑b

@[simp]

theorem Fin.castLE_natCast {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ℕ) : castLE h ↑a = ↑(a % m)

succ and casts into larger Fin types

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

def Fin.succEmb (n : ℕ) : Fin n ↪ Fin (n + 1)

Fin.succ as an Embedding

Equations

• Fin.succEmb n = { toFun := Fin.succ, inj' := ⋯ }

@[simp]

theorem Fin.coe_succEmb {n : ℕ} : ⇑(succEmb n) = succ

@[deprecated Fin.coe_succEmb (since := "2025-04-12")]

theorem Fin.val_succEmb {n : ℕ} : ⇑(succEmb n) = succ

Alias of Fin.coe_succEmb.

@[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

def Fin.castLEEmb {n m : ℕ} (h : n ≤ m) : Fin n ↪ Fin m

Fin.castLE as an Embedding, castLEEmb h i embeds i into a larger Fin type.

Equations

• Fin.castLEEmb h = { toFun := Fin.castLE h, inj' := ⋯ }

@[simp]

theorem Fin.castLEEmb_apply {n m : ℕ} (h : n ≤ m) (i : Fin n) : (castLEEmb h) i = castLE h i

@[simp]

theorem Fin.coe_castLEEmb {m n : ℕ} (hmn : m ≤ n) : ⇑(castLEEmb hmn) = castLE hmn

theorem Fin.nonempty_embedding_iff {n m : ℕ} : Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

theorem Fin.equiv_iff_eq {n m : ℕ} : Nonempty (Fin m ≃ Fin n) ↔ m = n

@[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.

def Fin.castAddEmb {n : ℕ} (m : ℕ) : Fin n ↪ Fin (n + m)

Fin.castAdd as an Embedding, castAddEmb m i embeds i : Fin n in Fin (n+m). See also Fin.natAddEmb and Fin.addNatEmb.

Equations

• Fin.castAddEmb m = Fin.castLEEmb ⋯

@[simp]

theorem Fin.coe_castAddEmb {n : ℕ} (m : ℕ) : ⇑(castAddEmb m) = castAdd m

theorem Fin.castAddEmb_apply {n : ℕ} (m : ℕ) (i : Fin n) : (castAddEmb m) i = castAdd m i

def Fin.castSuccEmb {n : ℕ} : Fin n ↪ Fin (n + 1)

Fin.castSucc as an Embedding, castSuccEmb i embeds i : Fin n in Fin (n+1).

Equations

• Fin.castSuccEmb = Fin.castAddEmb 1

@[simp]

theorem Fin.coe_castSuccEmb {n : ℕ} : ⇑castSuccEmb = castSucc

theorem Fin.castSuccEmb_apply {n : ℕ} (i : Fin n) : castSuccEmb i = i.castSucc

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

@[deprecated Fin.eq_castSucc_of_ne_last (since := "2025-02-06")]

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

Alias of Fin.eq_castSucc_of_ne_last.

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

def Fin.addNatEmb {n : ℕ} (m : ℕ) : Fin n ↪ Fin (n + m)

Fin.addNat as an Embedding, addNatEmb m i adds m to i, generalizes Fin.succ.

Equations

• Fin.addNatEmb m = { toFun := fun (x : Fin n) => x.addNat m, inj' := ⋯ }

@[simp]

theorem Fin.addNatEmb_apply {n : ℕ} (m : ℕ) (x✝ : Fin n) : (addNatEmb m) x✝ = x✝.addNat m

def Fin.natAddEmb (n : ℕ) {m : ℕ} : Fin m ↪ Fin (n + m)

Fin.natAdd as an Embedding, natAddEmb n i adds n to i "on the left".

Equations

• Fin.natAddEmb n = { toFun := Fin.natAdd n, inj' := ⋯ }

@[simp]

theorem Fin.natAddEmb_apply (n : ℕ) {m : ℕ} (i : Fin m) : (natAddEmb n) i = natAdd n 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

@[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.

def Fin.succAboveEmb {n : ℕ} (p : Fin (n + 1)) : Fin n ↪ Fin (n + 1)

Fin.succAbove p as an Embedding.

Equations

• p.succAboveEmb = { toFun := p.succAbove, inj' := ⋯ }

@[simp]

theorem Fin.succAboveEmb_apply {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : p.succAboveEmb i = p.succAbove i

@[simp]

theorem Fin.coe_succAboveEmb {n : ℕ} (p : Fin (n + 1)) : ⇑p.succAboveEmb = p.succAbove

@[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

@[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.

def Fin.divNat {n m : ℕ} (i : Fin (m * n)) : Fin m

Compute i / n, where n is a Nat and inferred the type of i.

Equations

• i.divNat = ⟨↑i / n, ⋯⟩

@[simp]

theorem Fin.coe_divNat {n m : ℕ} (i : Fin (m * n)) : ↑i.divNat = ↑i / n

def Fin.modNat {n m : ℕ} (i : Fin (m * n)) : Fin n

Compute i % n, where n is a Nat and inferred the type of i.

Equations

• i.modNat = ⟨↑i % n, ⋯⟩

@[simp]

theorem Fin.coe_modNat {n m : ℕ} (i : Fin (m * n)) : ↑i.modNat = ↑i % n

theorem Fin.modNat_rev {n m : ℕ} (i : Fin (m * n)) : i.rev.modNat = i.modNat.rev

recursion and induction principles

theorem Fin.liftFun_iff_succ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} : Relator.LiftFun (fun (x1 x2 : Fin (n + 1)) => x1 < x2) r f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

theorem Fin.eq_zero (n : Fin 1) : n = 0

theorem Fin.eq_one_of_ne_zero (i : Fin 2) (hi : i ≠ 0) : i = 1

@[deprecated Fin.eq_one_of_ne_zero (since := "2025-04-27")]

theorem Fin.eq_one_of_neq_zero (i : Fin 2) (hi : i ≠ 0) : i = 1

Alias of Fin.eq_one_of_ne_zero.

@[simp]

theorem Fin.coe_neg_one {n : ℕ} : ↑(-1) = n

theorem Fin.last_sub {n : ℕ} (i : Fin (n + 1)) : last n - i = i.rev

theorem Fin.add_one_le_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : a + 1 ≤ b

theorem Fin.exists_eq_add_of_le {n : ℕ} {a b : Fin n} (h : a ≤ b) : ∃ k ≤ b, b = a + k

theorem Fin.exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1

theorem Fin.pos_of_ne_zero {n : ℕ} {a : Fin (n + 1)} (h : a ≠ 0) : 0 < a

theorem Fin.sub_succ_le_sub_of_le {n : ℕ} {u v : Fin (n + 2)} (h : u < v) : v - (u + 1) < v - u

@[simp]

theorem Fin.coe_natCast_eq_mod (m n : ℕ) [NeZero m] : ↑↑n = n % m

theorem Fin.coe_ofNat_eq_mod (m n : ℕ) [NeZero m] : ↑(OfNat.ofNat n) = OfNat.ofNat n % m

mul

theorem Fin.mul_one' {n : ℕ} [NeZero n] (k : Fin n) : k * 1 = k

theorem Fin.one_mul' {n : ℕ} [NeZero n] (k : Fin n) : 1 * k = k

theorem Fin.mul_zero' {n : ℕ} [NeZero n] (k : Fin n) : k * 0 = 0

theorem Fin.zero_mul' {n : ℕ} [NeZero n] (k : Fin n) : 0 * k = 0