Init.Data.Fin.Lemmas

This is not an instance because the binop% elaborator assumes that there are no non-trivial coercion loops, but this introduces a coercion from Nat to Fin n and back.

Non-trivial loops lead to undesirable and counterintuitive elaboration behavior. For example, for x : Fin k and n : Nat, it causes x < n to be elaborated as x < ↑n rather than ↑x < n, silently introducing wraparound arithmetic.

Note: as of 2025-06-03, Mathlib has such a coercion for Fin n anyway!

Equations

Instances For

source

def Fin.intCast {n : Nat} [NeZero n] (a : Int) :

Fin n

Equations

Instances For

source

def Fin.IntCast.instIntCast (n : Nat) [NeZero n] :

IntCast (Fin n)

This is not a global instance, but may be activated locally via open Fin.IntCast in ....

See the doc-string for Fin.NatCast.instNatCast for more details.

Equations

Instances For

source

theorem Fin.intCast_def {n : Nat} [NeZero n] (x : Int) :

↑x = if 0 ≤ x then Fin.ofNat n x.natAbs else -Fin.ofNat n x.natAbs

order #

source

theorem Fin.le_def {n : Nat} {a b : Fin n} :

a ≤ b ↔ ↑a ≤ ↑b

source

theorem Fin.lt_def {n : Nat} {a b : Fin n} :

a < b ↔ ↑a < ↑b

source

theorem Fin.lt_iff_val_lt_val {n : Nat} {a b : Fin n} :

a < b ↔ ↑a < ↑b

source

@[simp]

theorem Fin.not_le {n : Nat} {a b : Fin n} :

¬a ≤ b ↔ b < a

source

@[simp]

theorem Fin.not_lt {n : Nat} {a b : Fin n} :

¬a < b ↔ b ≤ a

source

@[simp]

theorem Fin.le_refl {n : Nat} (a : Fin n) :

a ≤ a

source

@[simp]

theorem Fin.lt_irrefl {n : Nat} (a : Fin n) :

¬a < a

source

theorem Fin.le_trans {n : Nat} {a b c : Fin n} :

a ≤ b → b ≤ c → a ≤ c

source

theorem Fin.lt_trans {n : Nat} {a b c : Fin n} :

a < b → b < c → a < c

source

theorem Fin.le_total {n : Nat} (a b : Fin n) :

a ≤ b ∨ b ≤ a

source

theorem Fin.lt_asymm {n : Nat} {a b : Fin n} (h : a < b) :

¬b < a

source

theorem Fin.ne_of_lt {n : Nat} {a b : Fin n} (h : a < b) :

a ≠ b

source

theorem Fin.ne_of_gt {n : Nat} {a b : Fin n} (h : a < b) :

b ≠ a

source

theorem Fin.le_of_lt {n : Nat} {a b : Fin n} (h : a < b) :

a ≤ b

source

theorem Fin.lt_of_le_of_lt {n : Nat} {a b c : Fin n} :

a ≤ b → b < c → a < c

source

theorem Fin.lt_of_lt_of_le {n : Nat} {a b c : Fin n} :

a < b → b ≤ c → a < c

source

theorem Fin.le_rfl {n : Nat} {a : Fin n} :

a ≤ a

source

theorem Fin.lt_iff_le_and_ne {n : Nat} {a b : Fin n} :

a < b ↔ a ≤ b ∧ a ≠ b

source

theorem Fin.lt_or_lt_of_ne {n : Nat} {a b : Fin n} (h : a ≠ b) :

a < b ∨ b < a

source

theorem Fin.lt_or_le {n : Nat} (a b : Fin n) :

a < b ∨ b ≤ a

source

theorem Fin.le_or_lt {n : Nat} (a b : Fin n) :

a ≤ b ∨ b < a

source

theorem Fin.le_of_eq {n : Nat} {a b : Fin n} (hab : a = b) :

a ≤ b

source

theorem Fin.ge_of_eq {n : Nat} {a b : Fin n} (hab : a = b) :

b ≤ a

source

theorem Fin.eq_or_lt_of_le {n : Nat} {a b : Fin n} :

a ≤ b → a = b ∨ a < b

source

theorem Fin.lt_or_eq_of_le {n : Nat} {a b : Fin n} :

a ≤ b → a < b ∨ a = b

source

theorem Fin.is_le {n : Nat} (i : Fin (n + 1)) :

↑i ≤ n

source

@[simp]

theorem Fin.is_le' {n : Nat} {a : Fin n} :

↑a ≤ n

source

theorem Fin.mk_lt_of_lt_val {n : Nat} {b : Fin n} {a : Nat} (h : a < ↑b) :

⟨a, ⋯⟩ < b

source

theorem Fin.mk_le_of_le_val {n : Nat} {b : Fin n} {a : Nat} (h : a ≤ ↑b) :

⟨a, ⋯⟩ ≤ b

source

@[simp]

theorem Fin.mk_le_mk {n x y : Nat} {hx : x < n} {hy : y < n} :

⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y

source

@[simp]

theorem Fin.mk_lt_mk {n x y : Nat} {hx : x < n} {hy : y < n} :

⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y

source

@[simp]

theorem Fin.val_zero (n : Nat) [NeZero n] :

↑0 = 0

source

@[simp]

theorem Fin.mk_zero {n : Nat} :

⟨0, ⋯⟩ = 0

source

@[simp]

theorem Fin.zero_le {n : Nat} [NeZero n] (a : Fin n) :

0 ≤ a

source

theorem Fin.zero_lt_one {n : Nat} :

0 < 1

source

@[simp]

theorem Fin.not_lt_zero {n : Nat} [NeZero n] (a : Fin n) :

¬a < 0

source

theorem Fin.pos_iff_ne_zero {n : Nat} [NeZero n] {a : Fin n} :

0 < a ↔ a ≠ 0

source

theorem Fin.eq_zero_or_eq_succ {n : Nat} (i : Fin (n + 1)) :

i = 0 ∨ ∃ (j : Fin n), i = j.succ

source

theorem Fin.eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) :

∃ (j : Fin n), i = j.succ

source

theorem Fin.le_antisymm_iff {n : Nat} {x y : Fin n} :

x = y ↔ x ≤ y ∧ y ≤ x

source

theorem Fin.le_antisymm {n : Nat} {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) :

x = y

source

@[simp]

theorem Fin.val_rev {n : Nat} (i : Fin n) :

↑i.rev = n - (↑i + 1)

source

@[simp]

theorem Fin.rev_rev {n : Nat} (i : Fin n) :

i.rev.rev = i

source

@[simp]

theorem Fin.rev_le_rev {n : Nat} {i j : Fin n} :

i.rev ≤ j.rev ↔ j ≤ i

source

@[simp]

theorem Fin.rev_inj {n : Nat} {i j : Fin n} :

i.rev = j.rev ↔ i = j

source

theorem Fin.rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + ↑i) :

i.rev = ⟨a, ⋯⟩

source

@[simp]

theorem Fin.rev_lt_rev {n : Nat} {i j : Fin n} :

i.rev < j.rev ↔ j < i

last #

source

@[simp]

theorem Fin.val_last (n : Nat) :

↑(last n) = n

source

@[simp]

theorem Fin.last_zero :

last 0 = 0

source

@[simp]

theorem Fin.zero_eq_last_iff {n : Nat} :

0 = last n ↔ n = 0

source

@[simp]

theorem Fin.last_eq_zero_iff {n : Nat} :

last n = 0 ↔ n = 0

source

theorem Fin.le_last {n : Nat} (i : Fin (n + 1)) :

i ≤ last n

source

theorem Fin.last_pos {n : Nat} :

0 < last (n + 1)

source

theorem Fin.eq_last_of_not_lt {n : Nat} {i : Fin (n + 1)} (h : ¬↑i < n) :

i = last n

source

theorem Fin.val_lt_last {n : Nat} {i : Fin (n + 1)} :

i ≠ last n → ↑i < n

source

@[simp]

theorem Fin.rev_last (n : Nat) :

(last n).rev = 0

source

@[simp]

theorem Fin.rev_zero (n : Nat) :

rev 0 = last n

addition, numerals, and coercion from Nat #

source

@[simp]

theorem Fin.val_one (n : Nat) :

↑1 = 1

source

@[simp]

theorem Fin.mk_one {n : Nat} :

⟨1, ⋯⟩ = 1

source

theorem Fin.subsingleton_iff_le_one {n : Nat} :

Subsingleton (Fin n) ↔ n ≤ 1

source

instance Fin.subsingleton_zero :

Subsingleton (Fin 0)

source

instance Fin.subsingleton_one :

Subsingleton (Fin 1)

source

theorem Fin.fin_one_eq_zero (a : Fin 1) :

a = 0

source

@[simp]

theorem Fin.zero_eq_one_iff {n : Nat} [NeZero n] :

0 = 1 ↔ n = 1

source

@[simp]

theorem Fin.one_eq_zero_iff {n : Nat} [NeZero n] :

1 = 0 ↔ n = 1

source

theorem Fin.add_def {n : Nat} (a b : Fin n) :

a + b = ⟨(↑a + ↑b) % n, ⋯⟩

source

theorem Fin.val_add {n : Nat} (a b : Fin n) :

↑(a + b) = (↑a + ↑b) % n

source

@[simp]

theorem Fin.zero_add {n : Nat} [NeZero n] (k : Fin n) :

0 + k = k

source

@[simp]

theorem Fin.add_zero {n : Nat} [NeZero n] (k : Fin n) :

k + 0 = k

source

theorem Fin.val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last n) :

↑(i + 1) = ↑i + 1

source

@[simp]

theorem Fin.last_add_one (n : Nat) :

last n + 1 = 0

source

theorem Fin.val_add_one {n : Nat} (i : Fin (n + 1)) :

↑(i + 1) = if i = last n then 0 else ↑i + 1

source

@[simp]

theorem Fin.val_two {n : Nat} :

↑2 = 2

source

theorem Fin.add_one_pos {n : Nat} (i : Fin (n + 1)) (h : i < last n) :

0 < i + 1

source

theorem Fin.one_pos {n : Nat} :

0 < 1

source

theorem Fin.zero_ne_one {n : Nat} :

0 ≠ 1

succ and casts into larger Fin types #

source

@[simp]

theorem Fin.val_succ {n : Nat} (j : Fin n) :

↑j.succ = ↑j + 1

source

@[simp]

theorem Fin.succ_pos {n : Nat} (a : Fin n) :

0 < a.succ

source

@[simp]

theorem Fin.succ_le_succ_iff {n : Nat} {a b : Fin n} :

a.succ ≤ b.succ ↔ a ≤ b

source

@[simp]

theorem Fin.succ_lt_succ_iff {n : Nat} {a b : Fin n} :

a.succ < b.succ ↔ a < b

source

@[simp]

theorem Fin.succ_inj {n : Nat} {a b : Fin n} :

a.succ = b.succ ↔ a = b

source

theorem Fin.succ_ne_zero {n : Nat} (k : Fin n) :

k.succ ≠ 0

source

@[simp]

theorem Fin.succ_zero_eq_one {n : Nat} :

succ 0 = 1

source

@[simp]

theorem Fin.succ_one_eq_two {n : Nat} :

succ 1 = 2

Version of succ_one_eq_two to be used by dsimp

source

@[simp]

theorem Fin.succ_mk (n i : Nat) (h : i < n) :

⟨i, h⟩.succ = ⟨i + 1, ⋯⟩

source

theorem Fin.mk_succ_pos {n : Nat} (i : Nat) (h : i < n) :

0 < ⟨i.succ, ⋯⟩

source

theorem Fin.one_lt_succ_succ {n : Nat} (a : Fin n) :

1 < a.succ.succ

source

@[simp]

theorem Fin.add_one_lt_iff {n : Nat} {k : Fin (n + 2)} :

k + 1 < k ↔ k = last (n + 1)

source

@[simp]

theorem Fin.add_one_le_iff {n : Nat} {k : Fin (n + 1)} :

k + 1 ≤ k ↔ k = last n

source

@[simp]

theorem Fin.last_le_iff {n : Nat} {k : Fin (n + 1)} :

last n ≤ k ↔ k = last n

source

@[simp]

theorem Fin.lt_add_one_iff {n : Nat} {k : Fin (n + 1)} :

k < k + 1 ↔ k < last n

source

@[simp]

theorem Fin.le_zero_iff {n : Nat} {k : Fin (n + 1)} :

k ≤ 0 ↔ k = 0

source

theorem Fin.succ_succ_ne_one {n : Nat} (a : Fin n) :

a.succ.succ ≠ 1

source

@[simp]

theorem Fin.coe_castLT {m n : Nat} (i : Fin m) (h : ↑i < n) :

↑(i.castLT h) = ↑i

source

@[simp]

theorem Fin.castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) :

⟨i, hn⟩.castLT hm = ⟨i, hm⟩

source

@[simp]

theorem Fin.coe_castLE {n m : Nat} (h : n ≤ m) (i : Fin n) :

↑(castLE h i) = ↑i

source

@[simp]

theorem Fin.castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :

castLE h ⟨i, hn⟩ = ⟨i, ⋯⟩

source

@[simp]

theorem Fin.castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) :

castLE h 0 = 0

source

@[simp]

theorem Fin.castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :

castLE h i.succ = (castLE ⋯ i).succ

source

@[simp]

theorem Fin.castLE_castLE {k m n : Nat} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :

castLE mn (castLE km i) = castLE ⋯ i

source

@[simp]

theorem Fin.castLE_comp_castLE {k m n : Nat} (km : k ≤ m) (mn : m ≤ n) :

castLE mn ∘ castLE km = castLE ⋯

source

@[simp]

theorem Fin.coe_cast {n m : Nat} (h : n = m) (i : Fin n) :

↑(Fin.cast h i) = ↑i

source

@[simp]

theorem Fin.cast_castLE {k m n : Nat} (km : k ≤ m) (mn : m = n) (i : Fin k) :

Fin.cast mn (castLE km i) = castLE ⋯ i

source

@[simp]

theorem Fin.cast_castLT {k m n : Nat} (i : Fin k) (h : ↑i < m) (mn : m = n) :

Fin.cast mn (i.castLT h) = i.castLT ⋯

source

@[simp]

theorem Fin.cast_zero {n m : Nat} [NeZero n] [NeZero m] (h : n = m) :

Fin.cast h 0 = 0

source

@[simp]

theorem Fin.cast_last {n n' : Nat} {h : n + 1 = n' + 1} :

Fin.cast h (last n) = last n'

source

@[simp]

theorem Fin.cast_mk {n m : Nat} (h : n = m) (i : Nat) (hn : i < n) :

Fin.cast h ⟨i, hn⟩ = ⟨i, ⋯⟩

source

@[simp]

theorem Fin.cast_refl (n : Nat) (h : n = n) :

Fin.cast h = id

source

@[simp]

theorem Fin.cast_trans {n m k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :

Fin.cast h' (Fin.cast h i) = Fin.cast ⋯ i

source

theorem Fin.castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} :

castLE h' = Fin.cast h

source

@[simp]

theorem Fin.coe_castAdd {n : Nat} (m : Nat) (i : Fin n) :

↑(castAdd m i) = ↑i

source

@[simp]

theorem Fin.castAdd_zero {n : Nat} :

castAdd 0 = Fin.cast ⋯

source

theorem Fin.castAdd_lt {m : Nat} (n : Nat) (i : Fin m) :

↑(castAdd n i) < m

source

@[simp]

theorem Fin.castAdd_mk {n : Nat} (m i : Nat) (h : i < n) :

castAdd m ⟨i, h⟩ = ⟨i, ⋯⟩

source

@[simp]

theorem Fin.castAdd_castLT {n : Nat} (m : Nat) (i : Fin (n + m)) (hi : ↑i < n) :

castAdd m (i.castLT hi) = i

source

@[simp]

theorem Fin.castLT_castAdd {n : Nat} (m : Nat) (i : Fin n) :

(castAdd m i).castLT ⋯ = i

source

theorem Fin.castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :

castAdd m (Fin.cast h i) = Fin.cast ⋯ (castAdd m i)

For rewriting in the reverse direction, see Fin.cast_castAdd_left.

source

theorem Fin.cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :

Fin.cast h (castAdd m i) = castAdd m (Fin.cast ⋯ i)

source

@[simp]

theorem Fin.cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :

Fin.cast h (castAdd m' i) = castAdd m i

source

theorem Fin.castAdd_castAdd {m n p : Nat} (i : Fin m) :

castAdd p (castAdd n i) = Fin.cast ⋯ (castAdd (n + p) i)

source

@[simp]

theorem Fin.cast_succ_eq {n n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :

Fin.cast h i.succ = (Fin.cast ⋯ i).succ

The cast of the successor is the successor of the cast. See Fin.succ_cast_eq for rewriting in the reverse direction.

source

theorem Fin.succ_cast_eq {n n' : Nat} (i : Fin n) (h : n = n') :

(Fin.cast h i).succ = Fin.cast ⋯ i.succ

source

@[simp]

theorem Fin.coe_castSucc {n : Nat} (i : Fin n) :

↑i.castSucc = ↑i

source

@[simp]

theorem Fin.castSucc_mk (n i : Nat) (h : i < n) :

⟨i, h⟩.castSucc = ⟨i, ⋯⟩

source

@[simp]

theorem Fin.cast_castSucc {n n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :

Fin.cast h i.castSucc = (Fin.cast ⋯ i).castSucc

source

theorem Fin.castSucc_lt_succ {n : Nat} (i : Fin n) :

i.castSucc < i.succ

source

theorem Fin.le_castSucc_iff {n : Nat} {i : Fin (n + 1)} {j : Fin n} :

i ≤ j.castSucc ↔ i < j.succ

source

theorem Fin.castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :

i.castSucc < j ↔ i.succ ≤ j

source

@[simp]

theorem Fin.succ_last (n : Nat) :

(last n).succ = last n.succ

source

@[simp]

theorem Fin.succ_eq_last_succ {n : Nat} {i : Fin n.succ} :

i.succ = last (n + 1) ↔ i = last n

source

@[simp]

theorem Fin.castSucc_castLT {n : Nat} (i : Fin (n + 1)) (h : ↑i < n) :

(i.castLT h).castSucc = i

source

@[simp]

theorem Fin.castLT_castSucc {n : Nat} (a : Fin n) (h : ↑a < n) :

a.castSucc.castLT h = a

source

@[simp]

theorem Fin.castSucc_lt_castSucc_iff {n : Nat} {a b : Fin n} :

a.castSucc < b.castSucc ↔ a < b

source

theorem Fin.castSucc_inj {n : Nat} {a b : Fin n} :

a.castSucc = b.castSucc ↔ a = b

source

theorem Fin.castSucc_lt_last {n : Nat} (a : Fin n) :

a.castSucc < last n

source

@[simp]

theorem Fin.castSucc_zero {n : Nat} [NeZero n] :

castSucc 0 = 0

source

@[simp]

theorem Fin.castSucc_one {n : Nat} :

castSucc 1 = 1

source

theorem Fin.castSucc_pos {n : Nat} [NeZero n] {i : Fin n} (h : 0 < i) :

0 < i.castSucc

castSucc i is positive when i is positive

source

@[simp]

theorem Fin.castSucc_eq_zero_iff {n : Nat} [NeZero n] {a : Fin n} :

a.castSucc = 0 ↔ a = 0

source

theorem Fin.castSucc_ne_zero_iff {n : Nat} [NeZero n] {a : Fin n} :

a.castSucc ≠ 0 ↔ a ≠ 0

source

theorem Fin.castSucc_fin_succ (n : Nat) (j : Fin n) :

j.succ.castSucc = j.castSucc.succ

source

@[simp]

theorem Fin.coeSucc_eq_succ {n : Nat} {a : Fin n} :

a.castSucc + 1 = a.succ

source

theorem Fin.lt_succ {n : Nat} {a : Fin n} :

a.castSucc < a.succ

source

theorem Fin.exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} :

(∃ (j : Fin n), j.castSucc = i) ↔ i ≠ last n

source

theorem Fin.succ_castSucc {n : Nat} (i : Fin n) :

i.castSucc.succ = i.succ.castSucc

source

@[simp]

theorem Fin.coe_addNat {n : Nat} (m : Nat) (i : Fin n) :

↑(i.addNat m) = ↑i + m

source

@[simp]

theorem Fin.addNat_zero (n : Nat) (i : Fin n) :

i.addNat 0 = i

source

@[simp]

theorem Fin.addNat_one {n : Nat} {i : Fin n} :

i.addNat 1 = i.succ

source

theorem Fin.le_coe_addNat {n : Nat} (m : Nat) (i : Fin n) :

m ≤ ↑(i.addNat m)

source

@[simp]

theorem Fin.addNat_mk {m : Nat} (n i : Nat) (hi : i < m) :

⟨i, hi⟩.addNat n = ⟨i + n, ⋯⟩

source

@[simp]

theorem Fin.cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :

Fin.cast h (i.addNat 0) = Fin.cast ⋯ i

source

theorem Fin.addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :

(Fin.cast h i).addNat m = Fin.cast ⋯ (i.addNat m)

For rewriting in the reverse direction, see Fin.cast_addNat_left.

source

theorem Fin.cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :

Fin.cast h (i.addNat m) = (Fin.cast ⋯ i).addNat m

source

@[simp]

theorem Fin.cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :

Fin.cast h (i.addNat m') = i.addNat m

source

@[simp]

theorem Fin.coe_natAdd (n : Nat) {m : Nat} (i : Fin m) :

↑(natAdd n i) = n + ↑i

source

@[simp]

theorem Fin.natAdd_mk {m : Nat} (n i : Nat) (hi : i < m) :

natAdd n ⟨i, hi⟩ = ⟨n + i, ⋯⟩

source

theorem Fin.le_coe_natAdd {n : Nat} (m : Nat) (i : Fin n) :

m ≤ ↑(natAdd m i)

source

@[simp]

theorem Fin.natAdd_zero {n : Nat} :

natAdd 0 = Fin.cast ⋯

source

theorem Fin.natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :

natAdd m (Fin.cast h i) = Fin.cast ⋯ (natAdd m i)

For rewriting in the reverse direction, see Fin.cast_natAdd_right.

source

theorem Fin.cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :

Fin.cast h (natAdd m i) = natAdd m (Fin.cast ⋯ i)

source

@[simp]

theorem Fin.cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :

Fin.cast h (natAdd m' i) = natAdd m i

source

theorem Fin.castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :

castAdd p (natAdd m i) = Fin.cast ⋯ (natAdd m (castAdd p i))

source

theorem Fin.natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :

natAdd m (castAdd p i) = Fin.cast ⋯ (castAdd p (natAdd m i))

source

theorem Fin.natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :

natAdd m (natAdd n i) = Fin.cast ⋯ (natAdd (m + n) i)

source

theorem Fin.cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :

Fin.cast h (natAdd 0 i) = Fin.cast ⋯ i

source

@[simp]

theorem Fin.cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :

Fin.cast ⋯ (natAdd n i) = i.addNat n

source

@[simp]

theorem Fin.cast_addNat {n : Nat} (m : Nat) (i : Fin n) :

Fin.cast ⋯ (i.addNat m) = natAdd m i

source

@[simp]

theorem Fin.natAdd_last {m n : Nat} :

natAdd n (last m) = last (n + m)

source

@[simp]

theorem Fin.addNat_last {m : Nat} (n : Nat) :

(last n).addNat m = Fin.cast ⋯ (last (n + m))

source

theorem Fin.natAdd_castSucc {m n : Nat} {i : Fin m} :

natAdd n i.castSucc = (natAdd n i).castSucc

source

@[simp]

theorem Fin.natAdd_eq_addNat (n : Nat) (i : Fin n) :

natAdd n i = i.addNat n

source

theorem Fin.rev_castAdd {n : Nat} (k : Fin n) (m : Nat) :

(castAdd m k).rev = k.rev.addNat m

source

theorem Fin.rev_addNat {n : Nat} (k : Fin n) (m : Nat) :

(k.addNat m).rev = castAdd m k.rev

source

theorem Fin.rev_castSucc {n : Nat} (k : Fin n) :

k.castSucc.rev = k.rev.succ

source

theorem Fin.rev_succ {n : Nat} (k : Fin n) :

k.succ.rev = k.rev.castSucc

source

@[simp]

theorem Fin.castSucc_succ {n : Nat} (i : Fin n) :

i.succ.castSucc = i.castSucc.succ

source

@[simp]

theorem Fin.castLE_refl {n : Nat} (h : n ≤ n) (i : Fin n) :

castLE h i = i

source

@[simp]

theorem Fin.castSucc_castLE {n m : Nat} (h : n ≤ m) (i : Fin n) :

(castLE h i).castSucc = castLE ⋯ i

source

@[simp]

theorem Fin.castSucc_natAdd {k : Nat} (n : Nat) (i : Fin k) :

(natAdd n i).castSucc = natAdd n i.castSucc

pred #

source

@[simp]

theorem Fin.coe_pred {n : Nat} (j : Fin (n + 1)) (h : j ≠ 0) :

↑(j.pred h) = ↑j - 1

source

@[simp]

theorem Fin.succ_pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) :

(i.pred h).succ = i

source

@[simp]

theorem Fin.pred_succ {n : Nat} (i : Fin n) {h : i.succ ≠ 0} :

i.succ.pred h = i

source

theorem Fin.pred_eq_iff_eq_succ {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n} :

i.pred hi = j ↔ i = j.succ

source

theorem Fin.pred_mk_succ {n : Nat} (i : Nat) (h : i < n + 1) :

⟨i + 1, ⋯⟩.pred ⋯ = ⟨i, h⟩

source

@[simp]

theorem Fin.pred_mk_succ' {n : Nat} (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂ : ⟨i + 1, h₁⟩ ≠ 0) :

⟨i + 1, h₁⟩.pred h₂ = ⟨i, ⋯⟩

source

theorem Fin.pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w : ⟨i, h⟩ ≠ 0) :

⟨i, h⟩.pred w = ⟨i - 1, ⋯⟩

source

@[simp]

theorem Fin.pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :

a.pred ha ≤ b.pred hb ↔ a ≤ b

source

@[simp]

theorem Fin.pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :

a.pred ha < b.pred hb ↔ a < b

source

@[simp]

theorem Fin.pred_inj {n : Nat} {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0} :

a.pred ha = b.pred hb ↔ a = b

source

@[simp]

theorem Fin.pred_one {n : Nat} :

pred 1 ⋯ = 0

source

theorem Fin.pred_add_one {n : Nat} (i : Fin (n + 2)) (h : ↑i < n + 1) :

(i + 1).pred ⋯ = i.castLT h

source

@[simp]

theorem Fin.coe_subNat {n m : Nat} (i : Fin (n + m)) (h : m ≤ ↑i) :

↑(subNat m i h) = ↑i - m

source

@[simp]

theorem Fin.subNat_mk {n m i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :

subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, ⋯⟩

source

@[simp]

theorem Fin.subNat_zero {n : Nat} (i : Fin n) (h : 0 ≤ ↑i) :

subNat 0 i h = i

source

@[simp]

theorem Fin.subNat_one_succ {n : Nat} (i : Fin (n + 1)) (h : 1 ≤ ↑i) :

(subNat 1 i h).succ = i

source

@[simp]

theorem Fin.pred_castSucc_succ {n : Nat} (i : Fin n) :

i.succ.castSucc.pred ⋯ = i.castSucc

source

@[simp]

theorem Fin.addNat_subNat {n m : Nat} {i : Fin (n + m)} (h : m ≤ ↑i) :

(subNat m i h).addNat m = i

source

@[simp]

theorem Fin.subNat_addNat {n : Nat} (i : Fin n) (m : Nat) (h : m ≤ ↑(i.addNat m) := ⋯) :

subNat m (i.addNat m) h = i

source

@[simp]

theorem Fin.natAdd_subNat_cast {n m : Nat} {i : Fin (n + m)} (h : n ≤ ↑i) :

natAdd n (subNat n (Fin.cast ⋯ i) h) = i

Recursion and induction principles #

source

def Fin.succRec {motive : (n : Nat) → Fin n → Sort u_1} (zero : (n : Nat) → motive n.succ 0) (succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ) {n : Nat} (i : Fin n) :

motive n i

An induction principle for Fin that considers a given i : Fin n as given by a sequence of i applications of Fin.succ.

The cases in the induction are:

zero demonstrates the motive for (0 : Fin (n + 1)) for all bounds n
succ demonstrates the motive for Fin.succ applied to an arbitrary Fin for an arbitrary bound n

Unlike Fin.induction, the motive quantifies over the bound, and the bound varies at each inductive step. Fin.succRecOn is a version of this induction principle that takes the Fin argument first.

Equations

Instances For

source

def Fin.succRecOn {n : Nat} (i : Fin n) {motive : (n : Nat) → Fin n → Sort u_1} (zero : (n : Nat) → motive (n + 1) 0) (succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ) :

motive n i

An induction principle for Fin that considers a given i : Fin n as given by a sequence of i applications of Fin.succ.

The cases in the induction are:

zero demonstrates the motive for (0 : Fin (n + 1)) for all bounds n
succ demonstrates the motive for Fin.succ applied to an arbitrary Fin for an arbitrary bound n

Unlike Fin.induction, the motive quantifies over the bound, and the bound varies at each inductive step. Fin.succRec is a version of this induction principle that takes the Fin argument last.

Equations

Instances For

source

@[simp]

theorem Fin.succRecOn_zero {motive : (n : Nat) → Fin n → Sort u_1} {zero : (n : Nat) → motive (n + 1) 0} {succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ} (n : Nat) :

succRecOn 0 zero succ = zero n

source

@[simp]

theorem Fin.succRecOn_succ {motive : (n : Nat) → Fin n → Sort u_1} {zero : (n : Nat) → motive (n + 1) 0} {succ : (n : Nat) → (i : Fin n) → motive n i → motive n.succ i.succ} {n : Nat} (i : Fin n) :

i.succ.succRecOn zero succ = succ n i (i.succRecOn zero succ)

source

def Fin.induction {n : Nat} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSucc → motive i.succ) (i : Fin (n + 1)) :

motive i

Proves a statement by induction on the underlying Nat value in a Fin (n + 1).

For the induction:

zero is the base case, demonstrating motive 0.
succ is the inductive step, assuming the motive for i : Fin n (lifted to Fin (n + 1) with Fin.castSucc) and demonstrating it for i.succ.

Fin.inductionOn is a version of this induction principle that takes the Fin as its first parameter, Fin.cases is the corresponding case analysis operator, and Fin.reverseInduction is a version that starts at the greatest value instead of 0.

Equations

Instances For

source

def Fin.induction.go {n : Nat} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSucc → motive i.succ) (i : Nat) (hi : i < n + 1) :

motive ⟨i, hi⟩

Equations

Instances For

source

@[simp]

theorem Fin.induction_zero {n : Nat} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (hs : (i : Fin n) → motive i.castSucc → motive i.succ) :

(fun (i : Fin (n + 1)) => induction zero hs i) 0 = zero

source

@[simp]

theorem Fin.induction_succ {n : Nat} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSucc → motive i.succ) (i : Fin n) :

induction zero succ i.succ = succ i (induction zero succ i.castSucc)

source

def Fin.inductionOn {n : Nat} (i : Fin (n + 1)) {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSucc → motive i.succ) :

motive i

Proves a statement by induction on the underlying Nat value in a Fin (n + 1).

For the induction:

zero is the base case, demonstrating motive 0.
succ is the inductive step, assuming the motive for i : Fin n (lifted to Fin (n + 1) with Fin.castSucc) and demonstrating it for i.succ.

Fin.induction is a version of this induction principle that takes the Fin as its last parameter.

Equations

Instances For

source

def Fin.cases {n : Nat} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) :

motive i

Proves a statement by cases on the underlying Nat value in a Fin (n + 1).

The two cases are:

zero, used when the value is of the form (0 : Fin (n + 1))
succ, used when the value is of the form (j : Fin n).succ

The corresponding induction principle is Fin.induction.

Equations

Instances For

source

@[simp]

theorem Fin.cases_zero {n : Nat} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} :

cases zero succ 0 = zero

source

@[simp]

theorem Fin.cases_succ {n : Nat} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} (i : Fin n) :

cases zero succ i.succ = succ i

source

@[simp]

theorem Fin.cases_succ' {n : Nat} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} {i : Nat} (h : i + 1 < n + 1) :

cases zero succ ⟨i.succ, h⟩ = succ ⟨i, ⋯⟩

source

theorem Fin.forall_fin_succ {n : Nat} {P : Fin (n + 1) → Prop} :

(∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ

source

theorem Fin.exists_fin_succ {n : Nat} {P : Fin (n + 1) → Prop} :

(∃ (i : Fin (n + 1)), P i) ↔ P 0 ∨ ∃ (i : Fin n), P i.succ

source

theorem Fin.forall_fin_one {p : Fin 1 → Prop} :

(∀ (i : Fin 1), p i) ↔ p 0

source

theorem Fin.exists_fin_one {p : Fin 1 → Prop} :

(∃ (i : Fin 1), p i) ↔ p 0

source

theorem Fin.forall_fin_two {p : Fin 2 → Prop} :

(∀ (i : Fin 2), p i) ↔ p 0 ∧ p 1

source

theorem Fin.exists_fin_two {p : Fin 2 → Prop} :

(∃ (i : Fin 2), p i) ↔ p 0 ∨ p 1

source

theorem Fin.fin_two_eq_of_eq_zero_iff {a b : Fin 2} :

(a = 0 ↔ b = 0) → a = b

source

@[irreducible]

def Fin.reverseInduction {n : Nat} {motive : Fin (n + 1) → Sort u_1} (last : motive (last n)) (cast : (i : Fin n) → motive i.succ → motive i.castSucc) (i : Fin (n + 1)) :

motive i

Proves a statement by reverse induction on the underlying Nat value in a Fin (n + 1).

For the induction:

last is the base case, demonstrating motive (Fin.last n).
cast is the inductive step, assuming the motive for (j : Fin n).succ and demonstrating it for the predecessor j.castSucc.

Fin.induction is the non-reverse induction principle.

Equations

Instances For

source

@[simp]

theorem Fin.reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort u_1} {zero : motive (last n)} {succ : (i : Fin n) → motive i.succ → motive i.castSucc} :

reverseInduction zero succ (last n) = zero

source

@[simp]

theorem Fin.reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort u_1} {zero : motive (last n)} {succ : (i : Fin n) → motive i.succ → motive i.castSucc} (i : Fin n) :

reverseInduction zero succ i.castSucc = succ i (reverseInduction zero succ i.succ)

source

def Fin.lastCases {n : Nat} {motive : Fin (n + 1) → Sort u_1} (last : motive (last n)) (cast : (i : Fin n) → motive i.castSucc) (i : Fin (n + 1)) :

motive i

Proves a statement by cases on the underlying Nat value in a Fin (n + 1), checking whether the value is the greatest representable or a predecessor of some other.

The two cases are:

last, used when the value is Fin.last n
cast, used when the value is of the form (j : Fin n).succ

The corresponding induction principle is Fin.reverseInduction.

Equations

Instances For

source

@[simp]

theorem Fin.lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort u_1} {last : motive (last n)} {cast : (i : Fin n) → motive i.castSucc} :

lastCases last cast (Fin.last n) = last

source

@[simp]

theorem Fin.lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort u_1} {last : motive (last n)} {cast : (i : Fin n) → motive i.castSucc} (i : Fin n) :

lastCases last cast i.castSucc = cast i

source

def Fin.addCases {m n : Nat} {motive : Fin (m + n) → Sort u} (left : (i : Fin m) → motive (castAdd n i)) (right : (i : Fin n) → motive (natAdd m i)) (i : Fin (m + n)) :

motive i

A case analysis operator for i : Fin (m + n) that separately handles the cases where i < m and where m ≤ i < m + n.

The first case, where i < m, is handled by left. In this case, i can be represented as Fin.castAdd n (j : Fin m).

The second case, where m ≤ i < m + n, is handled by right. In this case, i can be represented as Fin.natAdd m (j : Fin n).

Equations

Instances For

source

@[simp]

theorem Fin.addCases_left {m n : Nat} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (castAdd n i)} {right : (i : Fin n) → motive (natAdd m i)} (i : Fin m) :

addCases left right (castAdd n i) = left i

source

@[simp]

theorem Fin.addCases_right {m n : Nat} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (castAdd n i)} {right : (i : Fin n) → motive (natAdd m i)} (i : Fin n) :

addCases left right (natAdd m i) = right i