Documentation

Init.Data.Fin.Lemmas

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

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 nProp} :
(∀ (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} (a : Nat) (is_pos : n > 0) :
(Fin.ofNat' a is_pos) = a % n
@[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
theorem Fin.ite_val {n : Nat} {c : Prop} [Decidable c] {x : cFin n} (y : ¬cFin 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 bb ca c
theorem Fin.lt_trans {n : Nat} {a : Fin n} {b : Fin n} {c : Fin n} :
a < bb < ca < 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) :
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
@[simp]
theorem Fin.val_last (n : Nat) :
(Fin.last n) = n
theorem Fin.le_last {n : Nat} (i : Fin (n + 1)) :
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) :
theorem Fin.val_lt_last {n : Nat} {i : Fin (n + 1)} :
i Fin.last ni < n
@[simp]
theorem Fin.rev_last (n : Nat) :
(Fin.last n).rev = 0
@[simp]
theorem Fin.rev_zero (n : Nat) :

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.fin_one_eq_zero (a : Fin 1) :
a = 0
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
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} :
@[simp]
theorem Fin.succ_one_eq_two {n : Nat} :

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)} :
@[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) :
@[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) :
@[simp]
theorem Fin.castLE_comp_castLE {k : Nat} {m : Nat} {n : Nat} (km : k m) (mn : m n) :
@[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} :
@[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_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} :
@[simp]
theorem Fin.coe_castAdd {n : Nat} (m : Nat) (i : Fin n) :
(Fin.castAdd m i) = i
@[simp]
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) :

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) :
@[simp]
theorem Fin.cast_castAdd_right {n : Nat} {m : Nat} {m' : Nat} (i : Fin n) (h : n + m' = n + m) :
theorem Fin.castAdd_castAdd {m : Nat} {n : Nat} {p : Nat} (i : Fin m) :
@[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} :
@[simp]
theorem Fin.castSucc_one {n : Nat} :
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_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)
theorem Fin.natAdd_cast {n : Nat} {n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :

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) :
@[simp]
theorem Fin.cast_natAdd_left {n : Nat} {m : Nat} {m' : Nat} (i : Fin n) (h : m' + n = m + n) :
theorem Fin.castAdd_natAdd (p : Nat) (m : Nat) {n : Nat} (i : Fin n) :
theorem Fin.natAdd_castAdd (p : Nat) (m : Nat) {n : Nat} (i : Fin n) :
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') :
@[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} :
theorem Fin.natAdd_castSucc {m : Nat} {n : Nat} {i : Fin m} :
Fin.natAdd n i.castSucc = (Fin.natAdd n i).castSucc
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.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 nSort u_1} (zero : (n : Nat) → motive n.succ 0) (succ : (n : Nat) → (i : Fin n) → motive n imotive 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
Instances For
    def Fin.succRecOn {n : Nat} (i : Fin n) {motive : (n : Nat) → Fin nSort u_1} (zero : (n : Nat) → motive (n + 1) 0) (succ : (n : Nat) → (i : Fin n) → motive n imotive 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
    Instances For
      @[simp]
      theorem Fin.succRecOn_zero {motive : (n : Nat) → Fin nSort u_1} {zero : (n : Nat) → motive (n + 1) 0} {succ : (n : Nat) → (i : Fin n) → motive n imotive n.succ i.succ} (n : Nat) :
      Fin.succRecOn 0 zero succ = zero n
      @[simp]
      theorem Fin.succRecOn_succ {motive : (n : Nat) → Fin nSort u_1} {zero : (n : Nat) → motive (n + 1) 0} {succ : (n : Nat) → (i : Fin n) → motive n imotive 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.castSuccmotive 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
      Instances For
        def Fin.induction.go {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSuccmotive i.succ) (i : Nat) (hi : i < n + 1) :
        motive i, hi
        Equations
        Instances For
          @[simp]
          theorem Fin.induction_zero {n : Nat} {motive : Fin (n + 1)Sort u_1} (zero : motive 0) (hs : (i : Fin n) → motive i.castSuccmotive 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.castSuccmotive 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.castSuccmotive 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
          Instances For
            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
            Instances For
              @[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 1Prop} :
              (∀ (i : Fin 1), p i) p 0
              theorem Fin.exists_fin_one {p : Fin 1Prop} :
              (∃ (i : Fin 1), p i) p 0
              theorem Fin.forall_fin_two {p : Fin 2Prop} :
              (∀ (i : Fin 2), p i) p 0 p 1
              theorem Fin.exists_fin_two {p : Fin 2Prop} :
              (∃ (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.succmotive 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
              Instances For
                @[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.succmotive 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.succmotive 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
                Instances For
                  @[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
                  Instances For
                    @[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 #

                    @[simp]
                    theorem Fin.ofNat'_add {n : Nat} (x : Nat) (lt : 0 < n) (y : Fin n) :
                    Fin.ofNat' x lt + y = Fin.ofNat' (x + y) lt
                    @[simp]
                    theorem Fin.add_ofNat' {n : Nat} (x : Fin n) (y : Nat) (lt : 0 < n) :
                    x + Fin.ofNat' y lt = Fin.ofNat' (x + y) lt

                    sub #

                    theorem Fin.coe_sub {n : Nat} (a : Fin n) (b : Fin n) :
                    (a - b) = (n - b + a) % n
                    @[simp]
                    theorem Fin.ofNat'_sub {n : Nat} (x : Nat) (lt : 0 < n) (y : Fin n) :
                    Fin.ofNat' x lt - y = Fin.ofNat' (n - y + x) lt
                    @[simp]
                    theorem Fin.sub_ofNat' {n : Nat} (x : Fin n) (y : Nat) (lt : 0 < n) :
                    x - Fin.ofNat' y lt = Fin.ofNat' (n - y % n + x) lt
                    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