theorem Fin.size_pos {n : Nat} (i : Fin n) : 0 < n

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

theorem Fin.mod_def {n : Nat} (a : Fin n) (m : Fin n) : a % m = ⟨↑a % ↑m, ⋯⟩

theorem Fin.mul_def {n : Nat} (a : Fin n) (b : Fin n) : a * b = ⟨↑a * ↑b % n, ⋯⟩

theorem Fin.sub_def {n : Nat} (a : Fin n) (b : Fin n) : a - b = ⟨(n - ↑b + ↑a) % n, ⋯⟩

theorem Fin.size_pos' {n : Nat} [Nonempty (Fin n)] : 0 < n

@[simp]

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

theorem Fin.pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n)

coercions and constructions

@[simp]

theorem Fin.eta {n : Nat} (a : Fin n) (h : ↑a < n) : ⟨↑a, h⟩ = a

theorem Fin.ext_iff {n : Nat} {a : Fin n} {b : Fin n} : a = b ↔ ↑a = ↑b

theorem Fin.ext {n : Nat} {a : Fin n} {b : Fin n} (h : ↑a = ↑b) : a = b

theorem Fin.val_ne_iff {n : Nat} {a : Fin n} {b : Fin n} : ↑a ≠ ↑b ↔ a ≠ b

theorem Fin.forall_iff {n : Nat} {p : Fin n → Prop} : (∀ (i : Fin n), p i) ↔ ∀ (i : Nat) (h : i < n), p ⟨i, h⟩

theorem Fin.mk.inj_iff {n : Nat} {a : Nat} {b : Nat} {ha : a < n} {hb : b < n} : ⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b

theorem Fin.val_mk {m : Nat} {n : Nat} (h : m < n) : ↑⟨m, h⟩ = m

theorem Fin.eq_mk_iff_val_eq {n : Nat} {a : Fin n} {k : Nat} {hk : k < n} : a = ⟨k, hk⟩ ↔ ↑a = k

theorem Fin.mk_val {n : Nat} (i : Fin n) : ⟨↑i, ⋯⟩ = i

@[simp]

theorem Fin.val_ofNat' (n : Nat) [NeZero n] (a : Nat) : ↑(Fin.ofNat' n a) = a % n

@[simp]

theorem Fin.ofNat'_self {n : Nat} [NeZero n] : Fin.ofNat' n n = 0

@[simp]

theorem Fin.ofNat'_val_eq_self {n : Nat} [NeZero n] (x : Fin n) : Fin.ofNat' n ↑x = x

@[simp]

theorem Fin.mod_val {n : Nat} (a : Fin n) (b : Fin n) : ↑(a % b) = ↑a % ↑b

@[simp]

theorem Fin.div_val {n : Nat} (a : Fin n) (b : Fin n) : ↑(a / b) = ↑a / ↑b

@[simp]

theorem Fin.modn_val {n : Nat} (a : Fin n) (b : Nat) : ↑(a.modn b) = ↑a % b

@[simp]

theorem Fin.val_eq_zero (a : Fin 1) : ↑a = 0

theorem Fin.ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) : ↑(if h : c then x h else y h) = if h : c then ↑(x h) else ↑(y h)

theorem Fin.dite_val {n : Nat} {c : Prop} [Decidable c] {x : Fin n} {y : Fin n} : ↑(if c then x else y) = if c then ↑x else ↑y

order

theorem Fin.le_def {n : Nat} {a : Fin n} {b : Fin n} : a ≤ b ↔ ↑a ≤ ↑b

theorem Fin.lt_def {n : Nat} {a : Fin n} {b : Fin n} : a < b ↔ ↑a < ↑b

theorem Fin.lt_iff_val_lt_val {n : Nat} {a : Fin n} {b : Fin n} : a < b ↔ ↑a < ↑b

@[simp]

theorem Fin.not_le {n : Nat} {a : Fin n} {b : Fin n} : ¬a ≤ b ↔ b < a

@[simp]

theorem Fin.not_lt {n : Nat} {a : Fin n} {b : Fin n} : ¬a < b ↔ b ≤ a

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

theorem Fin.mk_le_mk {n : Nat} {x : Nat} {y : Nat} {hx : x < n} {hy : y < n} : ⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y

@[simp]

theorem Fin.mk_lt_mk {n : Nat} {x : Nat} {y : Nat} {hx : x < n} {hy : y < n} : ⟨x, hx⟩ < ⟨y, hy⟩ ↔ x < y

@[simp]

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

@[simp]

theorem Fin.mk_zero {n : Nat} : ⟨0, ⋯⟩ = 0

@[simp]

theorem Fin.zero_le {n : Nat} (a : Fin (n + 1)) : 0 ≤ a

theorem Fin.zero_lt_one {n : Nat} : 0 < 1

@[simp]

theorem Fin.not_lt_zero {n : Nat} (a : Fin (n + 1)) : ¬a < 0

theorem Fin.pos_iff_ne_zero {n : Nat} {a : Fin (n + 1)} : 0 < a ↔ a ≠ 0

theorem Fin.eq_zero_or_eq_succ {n : Nat} (i : Fin (n + 1)) : i = 0 ∨ ∃ (j : Fin n), i = j.succ

theorem Fin.eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ (j : Fin n), i = j.succ

theorem Fin.le_antisymm_iff {n : Nat} {x : Fin n} {y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x

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

@[simp]

theorem Fin.val_rev {n : Nat} (i : Fin n) : ↑i.rev = n - (↑i + 1)

@[simp]

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

@[simp]

theorem Fin.rev_le_rev {n : Nat} {i : Fin n} {j : Fin n} : i.rev ≤ j.rev ↔ j ≤ i

@[simp]

theorem Fin.rev_inj {n : Nat} {i : Fin n} {j : Fin n} : i.rev = j.rev ↔ i = j

theorem Fin.rev_eq {n : Nat} {a : Nat} (i : Fin (n + 1)) (h : n = a + ↑i) : i.rev = ⟨a, ⋯⟩

@[simp]

theorem Fin.rev_lt_rev {n : Nat} {i : Fin n} {j : Fin n} : i.rev < j.rev ↔ j < i

last

@[simp]

theorem Fin.val_last (n : Nat) : ↑(Fin.last n) = n

@[simp]

theorem Fin.last_zero : Fin.last 0 = 0

@[simp]

theorem Fin.zero_eq_last_iff {n : Nat} : 0 = Fin.last n ↔ n = 0

@[simp]

theorem Fin.last_eq_zero_iff {n : Nat} : Fin.last n = 0 ↔ n = 0

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

theorem Fin.last_pos {n : Nat} : 0 < Fin.last (n + 1)

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

theorem Fin.val_lt_last {n : Nat} {i : Fin (n + 1)} : i ≠ Fin.last n → ↑i < n

@[simp]

theorem Fin.rev_last (n : Nat) : (Fin.last n).rev = 0

@[simp]

theorem Fin.rev_zero (n : Nat) : Fin.rev 0 = Fin.last n

addition, numerals, and coercion from Nat

@[simp]

theorem Fin.val_one (n : Nat) : ↑1 = 1

@[simp]

theorem Fin.mk_one {n : Nat} : ⟨1, ⋯⟩ = 1

theorem Fin.subsingleton_iff_le_one {n : Nat} : Subsingleton (Fin n) ↔ n ≤ 1

instance Fin.subsingleton_zero : Subsingleton (Fin 0)

Equations

• Fin.subsingleton_zero = ⋯

instance Fin.subsingleton_one : Subsingleton (Fin 1)

Equations

• Fin.subsingleton_one = ⋯

theorem Fin.fin_one_eq_zero (a : Fin 1) : a = 0

@[simp]

theorem Fin.zero_eq_one_iff {n : Nat} [NeZero n] : 0 = 1 ↔ n = 1

@[simp]

theorem Fin.one_eq_zero_iff {n : Nat} [NeZero n] : 1 = 0 ↔ n = 1

theorem Fin.add_def {n : Nat} (a : Fin n) (b : Fin n) : a + b = ⟨(↑a + ↑b) % n, ⋯⟩

theorem Fin.val_add {n : Nat} (a : Fin n) (b : Fin n) : ↑(a + b) = (↑a + ↑b) % n

@[simp]

theorem Fin.zero_add {n : Nat} [NeZero n] (i : Fin n) : 0 + i = i

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

@[simp]

theorem Fin.last_add_one (n : Nat) : Fin.last n + 1 = 0

theorem Fin.val_add_one {n : Nat} (i : Fin (n + 1)) : ↑(i + 1) = if i = Fin.last n then 0 else ↑i + 1

@[simp]

theorem Fin.val_two {n : Nat} : ↑2 = 2

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

theorem Fin.one_pos {n : Nat} : 0 < 1

theorem Fin.zero_ne_one {n : Nat} : 0 ≠ 1

succ and casts into larger Fin types

@[simp]

theorem Fin.val_succ {n : Nat} (j : Fin n) : ↑j.succ = ↑j + 1

@[simp]

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

@[simp]

theorem Fin.succ_le_succ_iff {n : Nat} {a : Fin n} {b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b

@[simp]

theorem Fin.succ_lt_succ_iff {n : Nat} {a : Fin n} {b : Fin n} : a.succ < b.succ ↔ a < b

@[simp]

theorem Fin.succ_inj {n : Nat} {a : Fin n} {b : Fin n} : a.succ = b.succ ↔ a = b

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

@[simp]

theorem Fin.succ_zero_eq_one {n : Nat} : Fin.succ 0 = 1

@[simp]

theorem Fin.succ_one_eq_two {n : Nat} : Fin.succ 1 = 2

Version of succ_one_eq_two to be used by dsimp

@[simp]

theorem Fin.succ_mk (n : Nat) (i : Nat) (h : i < n) : ⟨i, h⟩.succ = ⟨i + 1, ⋯⟩

theorem Fin.mk_succ_pos {n : Nat} (i : Nat) (h : i < n) : 0 < ⟨i.succ, ⋯⟩

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

@[simp]

theorem Fin.add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = Fin.last (n + 1)

@[simp]

theorem Fin.add_one_le_iff {n : Nat} {k : Fin (n + 1)} : k + 1 ≤ k ↔ k = Fin.last n

@[simp]

theorem Fin.last_le_iff {n : Nat} {k : Fin (n + 1)} : Fin.last n ≤ k ↔ k = Fin.last n

@[simp]

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

@[simp]

theorem Fin.le_zero_iff {n : Nat} {k : Fin (n + 1)} : k ≤ 0 ↔ k = 0

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

@[simp]

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

@[simp]

theorem Fin.castLT_mk (i : Nat) (n : Nat) (m : Nat) (hn : i < n) (hm : i < m) : ⟨i, hn⟩.castLT hm = ⟨i, hm⟩

@[simp]

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

@[simp]

theorem Fin.castLE_mk (i : Nat) (n : Nat) (m : Nat) (hn : i < n) (h : n ≤ m) : Fin.castLE h ⟨i, hn⟩ = ⟨i, ⋯⟩

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Fin.cast_last {n : Nat} {n' : Nat} {h : n + 1 = n' + 1} : Fin.cast h (Fin.last n) = Fin.last n'

@[simp]

theorem Fin.cast_mk {n : Nat} {m : Nat} (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, ⋯⟩

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Fin.castAdd_zero {n : Nat} : Fin.castAdd 0 = Fin.cast ⋯

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

@[simp]

theorem Fin.castAdd_mk {n : Nat} (m : Nat) (i : Nat) (h : i < n) : Fin.castAdd m ⟨i, h⟩ = ⟨i, ⋯⟩

@[simp]

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

@[simp]

theorem Fin.castLT_castAdd {n : Nat} (m : Nat) (i : Fin n) : (Fin.castAdd m i).castLT ⋯ = i

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

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

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

@[simp]

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

theorem Fin.castAdd_castAdd {m : Nat} {n : Nat} {p : Nat} (i : Fin m) : Fin.castAdd p (Fin.castAdd n i) = Fin.cast ⋯ (Fin.castAdd (n + p) i)

@[simp]

theorem Fin.cast_succ_eq {n : Nat} {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.

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

@[simp]

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

@[simp]

theorem Fin.castSucc_mk (n : Nat) (i : Nat) (h : i < n) : ⟨i, h⟩.castSucc = ⟨i, ⋯⟩

@[simp]

theorem Fin.cast_castSucc {n : Nat} {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} : Fin.cast h i.castSucc = (Fin.cast ⋯ i).castSucc

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

theorem Fin.le_castSucc_iff {n : Nat} {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ

theorem Fin.castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} : i.castSucc < j ↔ i.succ ≤ j

@[simp]

theorem Fin.succ_last (n : Nat) : (Fin.last n).succ = Fin.last n.succ

@[simp]

theorem Fin.succ_eq_last_succ {n : Nat} {i : Fin n.succ} : i.succ = Fin.last (n + 1) ↔ i = Fin.last n

@[simp]

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

@[simp]

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

@[simp]

theorem Fin.castSucc_lt_castSucc_iff {n : Nat} {a : Fin n} {b : Fin n} : a.castSucc < b.castSucc ↔ a < b

theorem Fin.castSucc_inj {n : Nat} {a : Fin n} {b : Fin n} : a.castSucc = b.castSucc ↔ a = b

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

@[simp]

theorem Fin.castSucc_zero {n : Nat} : Fin.castSucc 0 = 0

@[simp]

theorem Fin.castSucc_one {n : Nat} : Fin.castSucc 1 = 1

theorem Fin.castSucc_pos {n : Nat} {i : Fin (n + 1)} (h : 0 < i) : 0 < i.castSucc

castSucc i is positive when i is positive

@[simp]

theorem Fin.castSucc_eq_zero_iff {n : Nat} {a : Fin (n + 1)} : a.castSucc = 0 ↔ a = 0

theorem Fin.castSucc_ne_zero_iff {n : Nat} {a : Fin (n + 1)} : a.castSucc ≠ 0 ↔ a ≠ 0

theorem Fin.castSucc_fin_succ (n : Nat) (j : Fin n) : j.succ.castSucc = j.castSucc.succ

@[simp]

theorem Fin.coeSucc_eq_succ {n : Nat} {a : Fin n} : a.castSucc + 1 = a.succ

theorem Fin.lt_succ {n : Nat} {a : Fin n} : a.castSucc < a.succ

theorem Fin.exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ (j : Fin n), j.castSucc = i) ↔ i ≠ Fin.last n

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

@[simp]

theorem Fin.coe_addNat {n : Nat} (m : Nat) (i : Fin n) : ↑(i.addNat m) = ↑i + m

@[simp]

theorem Fin.addNat_zero (n : Nat) (i : Fin n) : i.addNat 0 = i

@[simp]

theorem Fin.addNat_one {n : Nat} {i : Fin n} : i.addNat 1 = i.succ

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

@[simp]

theorem Fin.addNat_mk {m : Nat} (n : Nat) (i : Nat) (hi : i < m) : ⟨i, hi⟩.addNat n = ⟨i + n, ⋯⟩

@[simp]

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

theorem Fin.addNat_cast {n : Nat} {n' : Nat} {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.

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

@[simp]

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

@[simp]

theorem Fin.coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : ↑(Fin.natAdd n i) = n + ↑i

@[simp]

theorem Fin.natAdd_mk {m : Nat} (n : Nat) (i : Nat) (hi : i < m) : Fin.natAdd n ⟨i, hi⟩ = ⟨n + i, ⋯⟩

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

@[simp]

theorem Fin.natAdd_zero {n : Nat} : Fin.natAdd 0 = Fin.cast ⋯

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

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

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

@[simp]

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

theorem Fin.castAdd_natAdd (p : Nat) (m : Nat) {n : Nat} (i : Fin n) : Fin.castAdd p (Fin.natAdd m i) = Fin.cast ⋯ (Fin.natAdd m (Fin.castAdd p i))

theorem Fin.natAdd_castAdd (p : Nat) (m : Nat) {n : Nat} (i : Fin n) : Fin.natAdd m (Fin.castAdd p i) = Fin.cast ⋯ (Fin.castAdd p (Fin.natAdd m i))

theorem Fin.natAdd_natAdd (m : Nat) (n : Nat) {p : Nat} (i : Fin p) : Fin.natAdd m (Fin.natAdd n i) = Fin.cast ⋯ (Fin.natAdd (m + n) i)

@[simp]

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

@[simp]

theorem Fin.cast_natAdd (n : Nat) {m : Nat} (i : Fin m) : Fin.cast ⋯ (Fin.natAdd n i) = i.addNat n

@[simp]

theorem Fin.cast_addNat {n : Nat} (m : Nat) (i : Fin n) : Fin.cast ⋯ (i.addNat m) = Fin.natAdd m i

@[simp]

theorem Fin.natAdd_last {m : Nat} {n : Nat} : Fin.natAdd n (Fin.last m) = Fin.last (n + m)

@[simp]

theorem Fin.addNat_last {m : Nat} (n : Nat) : (Fin.last n).addNat m = Fin.cast ⋯ (Fin.last (n + m))

theorem Fin.natAdd_castSucc {m : Nat} {n : Nat} {i : Fin m} : Fin.natAdd n i.castSucc = (Fin.natAdd n i).castSucc

@[simp]

theorem Fin.natAdd_eq_addNat (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n

theorem Fin.rev_castAdd {n : Nat} (k : Fin n) (m : Nat) : (Fin.castAdd m k).rev = k.rev.addNat m

theorem Fin.rev_addNat {n : Nat} (k : Fin n) (m : Nat) : (k.addNat m).rev = Fin.castAdd m k.rev

theorem Fin.rev_castSucc {n : Nat} (k : Fin n) : k.castSucc.rev = k.rev.succ

theorem Fin.rev_succ {n : Nat} (k : Fin n) : k.succ.rev = k.rev.castSucc

pred

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Fin.pred_mk_succ {n : Nat} (i : Nat) (h : i < n + 1) : ⟨i + 1, ⋯⟩.pred ⋯ = ⟨i, h⟩

@[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, ⋯⟩

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Fin.pred_one {n : Nat} : Fin.pred 1 ⋯ = 0

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

@[simp]

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

@[simp]

theorem Fin.subNat_mk {n : Nat} {m : Nat} {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) : Fin.subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, ⋯⟩

@[simp]

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

@[simp]

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

@[simp]

theorem Fin.pred_castSucc_succ {n : Nat} (i : Fin n) : i.succ.castSucc.pred ⋯ = i.castSucc

@[simp]

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

@[simp]

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

@[simp]

theorem Fin.natAdd_subNat_cast {n : Nat} {m : Nat} {i : Fin (n + m)} (h : n ≤ ↑i) : Fin.natAdd n (Fin.subNat n (Fin.cast ⋯ i) h) = i

recursion and induction principles

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

Define motive n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: zero n defines 0-th element motive (n+1) 0 of an (n+1)-tuple, and succ n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

Equations

• Fin.succRec zero succ i = i.elim0
• Fin.succRec zero succ ⟨0, isLt⟩ = ⋯.mpr (zero n)
• Fin.succRec zero succ ⟨i.succ, h⟩ = succ n ⟨i, ⋯⟩ (Fin.succRec zero succ ⟨i, ⋯⟩)

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

Define motive n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: zero n defines the 0-th element motive (n+1) 0 of an (n+1)-tuple, and succ n i defines the (i+1)-st element of an (n+1)-tuple based on n, i, and the i-th element of an n-tuple.

A version of Fin.succRec taking i : Fin n as the first argument.

Equations

• i.succRecOn zero succ = Fin.succRec zero succ i

@[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) : Fin.succRecOn 0 zero succ = zero n

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

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

Define motive i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: zero handles the base case on motive 0, and succ defines the inductive step using motive i.castSucc.

Equations

• Fin.induction zero succ ⟨i, hi⟩ = Fin.induction.go zero succ i hi

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

• Fin.induction.go zero succ 0 hi = ⋯.mpr zero
• Fin.induction.go zero succ i.succ hi = succ ⟨i, ⋯⟩ (Fin.induction.go zero succ i ⋯)

@[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)) => Fin.induction zero hs i) 0 = zero

@[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) : Fin.induction zero succ i.succ = succ i (Fin.induction zero succ i.castSucc)

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

Define motive i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: zero handles the base case on motive 0, and succ defines the inductive step using motive i.castSucc.

A version of Fin.induction taking i : Fin (n + 1) as the first argument.

Equations

• i.inductionOn zero succ = Fin.induction zero succ i

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

Define f : Π i : Fin n.succ, motive i by separately handling the cases i = 0 and i = j.succ, j : Fin n.

Equations

• Fin.cases zero succ i = Fin.induction zero (fun (i : Fin n) (x : motive i.castSucc) => succ i) i

@[simp]

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

@[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) : Fin.cases zero succ i.succ = succ i

@[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) : Fin.cases zero succ ⟨i.succ, h⟩ = succ ⟨i, ⋯⟩

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

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

theorem Fin.forall_fin_one {p : Fin 1 → Prop} : (∀ (i : Fin 1), p i) ↔ p 0

theorem Fin.exists_fin_one {p : Fin 1 → Prop} : (∃ (i : Fin 1), p i) ↔ p 0

theorem Fin.forall_fin_two {p : Fin 2 → Prop} : (∀ (i : Fin 2), p i) ↔ p 0 ∧ p 1

theorem Fin.exists_fin_two {p : Fin 2 → Prop} : (∃ (i : Fin 2), p i) ↔ p 0 ∨ p 1

theorem Fin.fin_two_eq_of_eq_zero_iff {a : Fin 2} {b : Fin 2} : (a = 0 ↔ b = 0) → a = b

@[irreducible]

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

Define motive i by reverse induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: last handles the base case on motive (Fin.last n), and cast defines the inductive step using motive i.succ, inducting downwards.

Equations

• Fin.reverseInduction last cast i = if hi : i = Fin.last n then _root_.cast ⋯ last else let j := ⟨↑i, ⋯⟩; cast j (Fin.reverseInduction last cast j.succ)

@[simp]

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

@[simp]

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

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

Define f : Π i : Fin n.succ, motive i by separately handling the cases i = Fin.last n and i = j.castSucc, j : Fin n.

Equations

• Fin.lastCases last cast i = Fin.reverseInduction last (fun (i : Fin n) (x : motive i.succ) => cast i) i

@[simp]

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

@[simp]

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

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

Define f : Π i : Fin (m + n), motive i by separately handling the cases i = castAdd n i, j : Fin m and i = natAdd m j, j : Fin n.

Equations

• Fin.addCases left right i = if hi : ↑i < m then ⋯ ▸ left (i.castLT hi) else ⋯ ▸ right (Fin.subNat m (Fin.cast ⋯ i) ⋯)

@[simp]

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

@[simp]

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

add

theorem Fin.ofNat'_add {n : Nat} [NeZero n] (x : Nat) (y : Fin n) : Fin.ofNat' n x + y = Fin.ofNat' n (x + ↑y)

theorem Fin.add_ofNat' {n : Nat} [NeZero n] (x : Fin n) (y : Nat) : x + Fin.ofNat' n y = Fin.ofNat' n (↑x + y)

sub

theorem Fin.coe_sub {n : Nat} (a : Fin n) (b : Fin n) : ↑(a - b) = (n - ↑b + ↑a) % n

theorem Fin.ofNat'_sub {n : Nat} [NeZero n] (x : Nat) (y : Fin n) : Fin.ofNat' n x - y = Fin.ofNat' n (n - ↑y + x)

theorem Fin.sub_ofNat' {n : Nat} [NeZero n] (x : Fin n) (y : Nat) : x - Fin.ofNat' n y = Fin.ofNat' n (n - y % n + ↑x)

@[simp]

theorem Fin.sub_self {n : Nat} [NeZero n] {x : Fin n} : x - x = 0

theorem Fin.coe_sub_iff_le {n : Nat} {a : Fin n} {b : Fin n} : ↑(a - b) = ↑a - ↑b ↔ b ≤ a

theorem Fin.sub_val_of_le {n : Nat} {a : Fin n} {b : Fin n} : b ≤ a → ↑(a - b) = ↑a - ↑b

theorem Fin.coe_sub_iff_lt {n : Nat} {a : Fin n} {b : Fin n} : ↑(a - b) = n + ↑a - ↑b ↔ a < b

mul

theorem Fin.val_mul {n : Nat} (a : Fin n) (b : Fin n) : ↑(a * b) = ↑a * ↑b % n

theorem Fin.coe_mul {n : Nat} (a : Fin n) (b : Fin n) : ↑(a * b) = ↑a * ↑b % n

theorem Fin.mul_one {n : Nat} (k : Fin (n + 1)) : k * 1 = k

theorem Fin.mul_comm {n : Nat} (a : Fin n) (b : Fin n) : a * b = b * a

instance Fin.instCommutativeHMul {n : Nat} : Std.Commutative fun (x1 x2 : Fin n) => x1 * x2

Equations

• ⋯ = ⋯

theorem Fin.mul_assoc {n : Nat} (a : Fin n) (b : Fin n) (c : Fin n) : a * b * c = a * (b * c)

instance Fin.instAssociativeHMul {n : Nat} : Std.Associative fun (x1 x2 : Fin n) => x1 * x2

Equations

• ⋯ = ⋯

theorem Fin.one_mul {n : Nat} (k : Fin (n + 1)) : 1 * k = k

instance Fin.instLawfulIdentityHAddNatOfNatHMul {n : Nat} : Std.LawfulIdentity (fun (x1 x2 : Fin (n + 1)) => x1 * x2) 1

Equations

• ⋯ = ⋯

theorem Fin.mul_zero {n : Nat} (k : Fin (n + 1)) : k * 0 = 0

theorem Fin.zero_mul {n : Nat} (k : Fin (n + 1)) : 0 * k = 0