import algebra.ne_zero

import algebra.order.with_zero

import order.rel_iso.basic

import data.nat.order.basic

import order.hom.set

universes u v

open fin nat function

def fin_zero_elim {α : fin 0 → Sort u} (x : fin 0) : α x := x.elim0

namespace fin

def elim0' {α : Sort*} (x : fin 0) : α := x.elim0

variables {n m : ℕ} {a b : fin n}

instance fin_to_nat (n : ℕ) : has_coe (fin n) nat := ⟨fin.val⟩

lemma val_injective : function.injective (@fin.val n) := @fin.eq_of_veq n

protected lemma prop (a : fin n) : a.val < n := a.2

@[simp] lemma is_lt (a : fin n) : (a : ℕ) < n := a.2

protected lemma pos (i : fin n) : 0 < n := lt_of_le_of_lt (nat.zero_le _) i.is_lt

lemma pos_iff_nonempty {n : ℕ} : 0 < n ↔ nonempty (fin n) := ⟨λ h, ⟨⟨0, h⟩⟩, λ ⟨i⟩, i.pos⟩

def equiv_subtype : fin n ≃ { i // i < n } :=

{ to_fun := λ a, ⟨a.1, a.2⟩, inv_fun := λ a, ⟨a.1, a.2⟩,

left_inv := λ ⟨_, _⟩, rfl, right_inv := λ ⟨_, _⟩, rfl }

section coe

@[simp] protected lemma eta (a : fin n) (h : (a : ℕ) < n) : (⟨(a : ℕ), h⟩ : fin n) = a :=

by cases a; refl

lemma ext {a b : fin n} (h : (a : ℕ) = b) : a = b := eq_of_veq h

lemma ext_iff {a b : fin n} : a = b ↔ (a : ℕ) = b :=

iff.intro (congr_arg _) fin.eq_of_veq

lemma coe_injective {n : ℕ} : injective (coe : fin n → ℕ) := fin.val_injective

lemma coe_eq_coe (a b : fin n) : (a : ℕ) = b ↔ a = b :=

ext_iff.symm

lemma eq_iff_veq (a b : fin n) : a = b ↔ a.1 = b.1 :=

⟨veq_of_eq, eq_of_veq⟩

lemma ne_iff_vne (a b : fin n) : a ≠ b ↔ a.1 ≠ b.1 :=

⟨vne_of_ne, ne_of_vne⟩

@[simp, nolint simp_nf] -- built-in reduction doesn't always work

theorem mk_eq_mk {a h a' h'} : @mk n a h = @mk n a' h' ↔ a = a' :=

ext_iff

protected lemma mk.inj_iff {n a b : ℕ} {ha : a < n} {hb : b < n} :

(⟨a, ha⟩ : fin n) = ⟨b, hb⟩ ↔ a = b :=

eq_iff_veq _ _

lemma mk_val {m n : ℕ} (h : m < n) : (⟨m, h⟩ : fin n).val = m := rfl

lemma eq_mk_iff_coe_eq {k : ℕ} {hk : k < n} : a = ⟨k, hk⟩ ↔ (a : ℕ) = k :=

fin.eq_iff_veq a ⟨k, hk⟩

@[simp, norm_cast] lemma coe_mk {m n : ℕ} (h : m < n) : ((⟨m, h⟩ : fin n) : ℕ) = m := rfl

lemma mk_coe (i : fin n) : (⟨i, i.property⟩ : fin n) = i :=

fin.eta _ _

lemma coe_eq_val (a : fin n) : (a : ℕ) = a.val := rfl

@[simp] lemma val_eq_coe (a : fin n) : a.val = a := rfl

protected lemma heq_fun_iff {α : Sort*} {k l : ℕ} (h : k = l) {f : fin k → α} {g : fin l → α} :

f == g ↔ (∀ (i : fin k), f i = g ⟨(i : ℕ), h ▸ i.2⟩) :=

by { subst h, simp [function.funext_iff] }

protected lemma heq_ext_iff {k l : ℕ} (h : k = l) {i : fin k} {j : fin l} :

i == j ↔ (i : ℕ) = (j : ℕ) :=

by { subst h, simp [coe_eq_coe] }

lemma exists_iff {p : fin n → Prop} : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=

⟨λ h, exists.elim h (λ ⟨i, hi⟩ hpi, ⟨i, hi, hpi⟩),

λ h, exists.elim h (λ i hi, ⟨⟨i, hi.fst⟩, hi.snd⟩)⟩

lemma forall_iff {p : fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ :=

⟨λ h i hi, h ⟨i, hi⟩, λ h ⟨i, hi⟩, h i hi⟩

end coe

section order

lemma is_le (i : fin (n + 1)) : (i : ℕ) ≤ n := le_of_lt_succ i.is_lt

@[simp] lemma is_le' : (a : ℕ) ≤ n := le_of_lt a.is_lt

lemma lt_iff_coe_lt_coe : a < b ↔ (a : ℕ) < b := iff.rfl

lemma le_iff_coe_le_coe : a ≤ b ↔ (a : ℕ) ≤ b := iff.rfl

lemma mk_lt_of_lt_coe {a : ℕ} (h : a < b) : (⟨a, h.trans b.is_lt⟩ : fin n) < b := h

lemma mk_le_of_le_coe {a : ℕ} (h : a ≤ b) : (⟨a, h.trans_lt b.is_lt⟩ : fin n) ≤ b := h

@[norm_cast, simp] lemma coe_fin_lt {n : ℕ} {a b : fin n} : (a : ℕ) < (b : ℕ) ↔ a < b :=

iff.rfl

@[norm_cast, simp] lemma coe_fin_le {n : ℕ} {a b : fin n} : (a : ℕ) ≤ (b : ℕ) ↔ a ≤ b :=

iff.rfl

instance {n : ℕ} : linear_order (fin n) :=

@linear_order.lift (fin n) _ _ ⟨λ x y, ⟨max x y, max_rec' (< n) x.2 y.2⟩⟩

⟨λ x y, ⟨min x y, min_rec' (< n) x.2 y.2⟩⟩ fin.val fin.val_injective (λ _ _, rfl) (λ _ _, rfl)

@[simp] lemma mk_le_mk {x y : nat} {hx} {hy} : (⟨x, hx⟩ : fin n) ≤ ⟨y, hy⟩ ↔ x ≤ y := iff.rfl

@[simp] lemma mk_lt_mk {x y : nat} {hx} {hy} : (⟨x, hx⟩ : fin n) < ⟨y, hy⟩ ↔ x < y := iff.rfl

@[simp] lemma min_coe : min (a : ℕ) n = a := by simp

@[simp] lemma max_coe : max (a : ℕ) n = n := by simp

instance {n : ℕ} : partial_order (fin n) := by apply_instance

lemma coe_strict_mono : strict_mono (coe : fin n → ℕ) := λ _ _, id

def order_iso_subtype : fin n ≃o { i // i < n } :=

equiv_subtype.to_order_iso (by simp [monotone]) (by simp [monotone])

def coe_embedding : fin n ↪ ℕ :=

⟨coe, coe_injective⟩

@[simp] lemma equiv_subtype_symm_trans_val_embedding :

equiv_subtype.symm.to_embedding.trans coe_embedding = embedding.subtype (< n) :=

rfl

def coe_order_embedding (n) : (fin n) ↪o ℕ :=

⟨coe_embedding, λ a b, iff.rfl⟩

instance fin.lt.is_well_order (n) : is_well_order (fin n) (<) :=

(coe_order_embedding n).is_well_order

instance {n : ℕ} : has_well_founded (fin n) :=

⟨_, measure_wf coe⟩

instance has_zero_of_ne_zero [ne_zero n] : has_zero (fin n) :=

⟨⟨0, ne_zero.pos _⟩⟩

def of_nat' [ne_zero n] (i : ℕ) : fin n := ⟨i%n, mod_lt _ $ ne_zero.pos n⟩

instance has_one_of_ne_zero [ne_zero n] : has_one (fin n) :=

⟨of_nat' 1⟩

@[simp] lemma coe_zero (n : ℕ) [ne_zero n] : ((0 : fin n) : ℕ) = 0 := rfl

attribute [simp] val_zero

@[simp] lemma val_zero' (n) [ne_zero n] : (0 : fin n).val = 0 := rfl

@[simp] lemma mk_zero [ne_zero n] :

(⟨0, nat.pos_of_ne_zero (ne_zero.ne n)⟩ : fin n) = (0 : fin _) := rfl

@[simp] lemma zero_le [ne_zero n] (a : fin n) : 0 ≤ a := zero_le a.1

lemma zero_lt_one : (0 : fin (n + 2)) < 1 := nat.zero_lt_one

@[simp] lemma not_lt_zero (a : fin n.succ) : ¬a < 0.

lemma pos_iff_ne_zero [ne_zero n] (a : fin n) : 0 < a ↔ a ≠ 0 :=

by rw [← coe_fin_lt, coe_zero, pos_iff_ne_zero, ne.def, ne.def, ext_iff, coe_zero]

lemma eq_zero_or_eq_succ {n : ℕ} (i : fin (n+1)) : i = 0 ∨ ∃ j : fin n, i = j.succ :=

rcases i with ⟨_|j, h⟩,

{ left, refl, },

{ right, exact ⟨⟨j, nat.lt_of_succ_lt_succ h⟩, rfl⟩, }

lemma eq_succ_of_ne_zero {n : ℕ} {i : fin (n + 1)} (hi : i ≠ 0) : ∃ j : fin n, i = j.succ :=

(eq_zero_or_eq_succ i).resolve_left hi

def rev : equiv.perm (fin n) :=

involutive.to_perm (λ i, ⟨n - (i + 1), tsub_lt_self i.pos (nat.succ_pos _)⟩) $

λ i, ext $ by rw [coe_mk, coe_mk, ← tsub_tsub,

tsub_tsub_cancel_of_le (nat.add_one_le_iff.2 i.is_lt), add_tsub_cancel_right]

@[simp] lemma coe_rev (i : fin n) : (i.rev : ℕ) = n - (i + 1) := rfl

lemma rev_involutive : involutive (@rev n) := involutive.to_perm_involutive _

lemma rev_injective : injective (@rev n) := rev_involutive.injective

lemma rev_surjective : surjective (@rev n) := rev_involutive.surjective

lemma rev_bijective : bijective (@rev n) := rev_involutive.bijective

@[simp] lemma rev_inj {i j : fin n} : i.rev = j.rev ↔ i = j := rev_injective.eq_iff

@[simp] lemma rev_rev (i : fin n) : i.rev.rev = i := rev_involutive _

@[simp] lemma rev_symm : (@rev n).symm = rev := rfl

lemma rev_eq {n a : ℕ} (i : fin (n+1)) (h : n=a+i) :

i.rev = ⟨a, nat.lt_succ_iff.mpr (nat.le.intro (h.symm))⟩ :=

ext,

dsimp,

conv_lhs { congr, rw h, },

rw [add_assoc, add_tsub_cancel_right],

@[simp] lemma rev_le_rev {i j : fin n} : i.rev ≤ j.rev ↔ j ≤ i :=

by simp only [le_iff_coe_le_coe, coe_rev, tsub_le_tsub_iff_left (nat.add_one_le_iff.2 j.is_lt),

add_le_add_iff_right]

@[simp] lemma rev_lt_rev {i j : fin n} : i.rev < j.rev ↔ j < i :=

lt_iff_lt_of_le_iff_le rev_le_rev

@[simps apply to_equiv] def rev_order_iso {n} : (fin n)ᵒᵈ ≃o fin n :=

⟨order_dual.of_dual.trans rev, λ i j, rev_le_rev⟩

@[simp] lemma rev_order_iso_symm_apply (i : fin n) :

rev_order_iso.symm i = order_dual.to_dual i.rev := rfl

def last (n : ℕ) : fin (n+1) := ⟨_, n.lt_succ_self⟩

@[simp, norm_cast] lemma coe_last (n : ℕ) : (last n : ℕ) = n := rfl

lemma last_val (n : ℕ) : (last n).val = n := rfl

theorem le_last (i : fin (n+1)) : i ≤ last n :=

le_of_lt_succ i.is_lt

instance : bounded_order (fin (n+1)) :=

{ top := last n,

le_top := le_last,

bot := 0,

bot_le := zero_le }

instance : lattice (fin (n + 1)) := linear_order.to_lattice

lemma last_pos : (0 : fin (n + 2)) < last (n + 1) :=

by simp [lt_iff_coe_lt_coe]

lemma eq_last_of_not_lt {i : fin (n+1)} (h : ¬ (i : ℕ) < n) : i = last n :=

le_antisymm (le_last i) (not_lt.1 h)

lemma top_eq_last (n : ℕ) : ⊤ = fin.last n := rfl

lemma bot_eq_zero (n : ℕ) : ⊥ = (0 : fin (n+1)) := rfl

variables {α : Type*} [preorder α]

open set

@[simp] lemma coe_order_iso_apply (e : fin n ≃o fin m) (i : fin n) : (e i : ℕ) = i :=

rcases i with ⟨i, hi⟩,

rw [fin.coe_mk],

induction i using nat.strong_induction_on with i h,

refine le_antisymm (forall_lt_iff_le.1 $ λ j hj, _) (forall_lt_iff_le.1 $ λ j hj, _),

{ have := e.symm.lt_iff_lt.2 (mk_lt_of_lt_coe hj),

rw e.symm_apply_apply at this,

convert this,

simpa using h _ this (e.symm _).is_lt },

{ rwa [← h j hj (hj.trans hi), ← lt_iff_coe_lt_coe, e.lt_iff_lt] }

instance order_iso_subsingleton : subsingleton (fin n ≃o α) :=

⟨λ e e', by { ext i,

rw [← e.symm.apply_eq_iff_eq, e.symm_apply_apply, ← e'.trans_apply, ext_iff,

coe_order_iso_apply] }⟩

instance order_iso_subsingleton' : subsingleton (α ≃o fin n) :=

order_iso.symm_injective.subsingleton

instance order_iso_unique : unique (fin n ≃o fin n) := unique.mk' _

lemma strict_mono_unique {f g : fin n → α} (hf : strict_mono f) (hg : strict_mono g)

(h : range f = range g) : f = g :=

have (hf.order_iso f).trans (order_iso.set_congr _ _ h) = hg.order_iso g,

from subsingleton.elim _ _,

congr_arg (function.comp (coe : range g → α)) (funext $ rel_iso.ext_iff.1 this)

lemma order_embedding_eq {f g : fin n ↪o α} (h : range f = range g) : f = g :=

rel_embedding.ext $ funext_iff.1 $ strict_mono_unique f.strict_mono g.strict_mono h

end order

section add

lemma one_val {n : ℕ} : (1 : fin (n+1)).val = 1 % (n+1) := rfl

lemma coe_one' (n : ℕ) [ne_zero n] : ((1 : fin n) : ℕ) = 1 % n := rfl

@[simp] lemma val_one (n : ℕ) : (1 : fin (n+2)).val = 1 := rfl

@[simp] lemma coe_one (n : ℕ) : ((1 : fin (n+2)) : ℕ) = 1 := rfl

@[simp] lemma mk_one : (⟨1, nat.succ_lt_succ (nat.succ_pos n)⟩ : fin (n + 2)) = (1 : fin _) := rfl

instance {n : ℕ} : nontrivial (fin (n + 2)) := ⟨⟨0, 1, dec_trivial⟩⟩

lemma nontrivial_iff_two_le : nontrivial (fin n) ↔ 2 ≤ n :=

by rcases n with _|_|n; simp [fin.nontrivial, not_nontrivial, nat.succ_le_iff]

lemma subsingleton_iff_le_one : subsingleton (fin n) ↔ n ≤ 1 :=

by rcases n with _|_|n; simp [is_empty.subsingleton, unique.subsingleton, not_subsingleton]

section monoid

instance add_comm_semigroup (n : ℕ) : add_comm_semigroup (fin n) :=

{ add := (+),

add_assoc := by simp [eq_iff_veq, add_def, add_assoc],

add_comm := by simp [eq_iff_veq, add_def, add_comm] }

@[simp] protected lemma add_zero [ne_zero n] (k : fin n) : k + 0 = k :=

by simp [eq_iff_veq, add_def, mod_eq_of_lt (is_lt k)]

@[simp] protected lemma zero_add [ne_zero n] (k : fin n) : (0 : fin n) + k = k :=

by simp [eq_iff_veq, add_def, mod_eq_of_lt (is_lt k)]

instance add_comm_monoid (n : ℕ) [ne_zero n] : add_comm_monoid (fin n) :=

{ add := (+),

zero := 0,

zero_add := fin.zero_add,

add_zero := fin.add_zero,

..fin.add_comm_semigroup n }

instance [ne_zero n] : add_monoid_with_one (fin n) :=

{ one := 1,

nat_cast := fin.of_nat',

nat_cast_zero := rfl,

nat_cast_succ := λ i, eq_of_veq (add_mod _ _ _),

.. fin.add_comm_monoid n }

end monoid

lemma val_add {n : ℕ} : ∀ a b : fin n, (a + b).val = (a.val + b.val) % n

| ⟨_, _⟩ ⟨_, _⟩ := rfl

lemma coe_add {n : ℕ} : ∀ a b : fin n, ((a + b : fin n) : ℕ) = (a + b) % n

| ⟨_, _⟩ ⟨_, _⟩ := rfl

lemma coe_add_eq_ite {n : ℕ} (a b : fin n) :

(↑(a + b) : ℕ) = if n ≤ a + b then a + b - n else a + b :=

by rw [fin.coe_add, nat.add_mod_eq_ite,

nat.mod_eq_of_lt (show ↑a < n, from a.2), nat.mod_eq_of_lt (show ↑b < n, from b.2)]

lemma coe_bit0 {n : ℕ} (k : fin n) : ((bit0 k : fin n) : ℕ) = bit0 (k : ℕ) % n :=

by { cases k, refl }

lemma coe_bit1 {n : ℕ} [ne_zero n] (k : fin n) :

((bit1 k : fin n) : ℕ) = bit1 (k : ℕ) % n :=

by simp [bit1, coe_add, coe_bit0, coe_one']

lemma coe_add_one_of_lt {n : ℕ} {i : fin n.succ} (h : i < last _) :

(↑(i + 1) : ℕ) = i + 1 :=

-- First show that `((1 : fin n.succ) : ℕ) = 1`, because `n.succ` is at least 2.

cases n,

{ cases h },

-- Then just unfold the definitions.

rw [fin.coe_add, fin.coe_one, nat.mod_eq_of_lt (nat.succ_lt_succ _)],

exact h

@[simp] lemma last_add_one : ∀ n, last n + 1 = 0

| 0 := subsingleton.elim _ _

| (n + 1) := by { ext, rw [coe_add, coe_zero, coe_last, coe_one, nat.mod_self] }

lemma coe_add_one {n : ℕ} (i : fin (n + 1)) :

((i + 1 : fin (n + 1)) : ℕ) = if i = last _ then 0 else i + 1 :=

rcases (le_last i).eq_or_lt with rfl|h,

{ simp },

{ simpa [h.ne] using coe_add_one_of_lt h }

section bit

@[simp] lemma mk_bit0 {m n : ℕ} (h : bit0 m < n) :

(⟨bit0 m, h⟩ : fin n) = (bit0 ⟨m, (nat.le_add_right m m).trans_lt h⟩ : fin _) :=

eq_of_veq (nat.mod_eq_of_lt h).symm

@[simp] lemma mk_bit1 {m n : ℕ} [ne_zero n] (h : bit1 m < n) :

(⟨bit1 m, h⟩ : fin n) = (bit1 ⟨m, (nat.le_add_right m m).trans_lt

((m + m).lt_succ_self.trans h)⟩ : fin _) :=

ext,

simp only [bit1, bit0] at h,

simp only [bit1, bit0, coe_add, coe_one', coe_mk, ←nat.add_mod, nat.mod_eq_of_lt h],

end bit

@[simp] lemma val_two {n : ℕ} : (2 : fin (n+3)).val = 2 := rfl

@[simp] lemma coe_two {n : ℕ} : ((2 : fin (n+3)) : ℕ) = 2 := rfl

section of_nat_coe

lemma of_nat_eq_coe (n : ℕ) (a : ℕ) : (of_nat a : fin (n+1)) = a :=

rfl

lemma of_nat'_eq_coe (n : ℕ) [ne_zero n] (a : ℕ) : (of_nat' a : fin n) = a :=

rfl

lemma coe_val_of_lt {n : ℕ} [ne_zero n] {a : ℕ} (h : a < n) :

((a : fin n).val) = a :=

rw ←of_nat'_eq_coe,

exact nat.mod_eq_of_lt h

lemma coe_val_eq_self {n : ℕ} [ne_zero n] (a : fin n) : (a.val : fin n) = a :=

rw fin.eq_iff_veq,

exact coe_val_of_lt a.property

lemma coe_coe_of_lt {n : ℕ} [ne_zero n] {a : ℕ} (h : a < n) :

((a : fin n) : ℕ) = a :=

coe_val_of_lt h

@[simp] lemma coe_coe_eq_self {n : ℕ} [ne_zero n] (a : fin n) : ((a : ℕ) : fin n) = a :=

coe_val_eq_self a

lemma coe_nat_eq_last (n) : (n : fin (n + 1)) = fin.last n :=

by { rw [←fin.of_nat_eq_coe, fin.of_nat, fin.last], simp only [nat.mod_eq_of_lt n.lt_succ_self] }

lemma le_coe_last (i : fin (n + 1)) : i ≤ n :=

by { rw fin.coe_nat_eq_last, exact fin.le_last i }

end of_nat_coe

lemma add_one_pos (i : fin (n + 1)) (h : i < fin.last n) : (0 : fin (n + 1)) < i + 1 :=

cases n,

{ exact absurd h (nat.not_lt_zero _) },

{ rw [lt_iff_coe_lt_coe, coe_last, ←add_lt_add_iff_right 1] at h,

rw [lt_iff_coe_lt_coe, coe_add, coe_zero, coe_one, nat.mod_eq_of_lt h],

exact nat.zero_lt_succ _ }

lemma one_pos : (0 : fin (n + 2)) < 1 := succ_pos 0

lemma zero_ne_one : (0 : fin (n + 2)) ≠ 1 := ne_of_lt one_pos

@[simp] lemma zero_eq_one_iff [ne_zero n]: (0 : fin n) = 1 ↔ n = 1 :=

split,

{ intro h,

have := congr_arg (coe : fin n → ℕ) h,

simp only [fin.coe_zero, ← nat.dvd_iff_mod_eq_zero, fin.coe_one', @eq_comm _ 0] at this,

exact eq_one_of_dvd_one this },

{ unfreezingI { rintro rfl }, refl }

@[simp] lemma one_eq_zero_iff [ne_zero n]: (1 : fin n) = 0 ↔ n = 1 :=

by rw [eq_comm, zero_eq_one_iff]

end add

section succ

@[simp] lemma coe_succ (j : fin n) : (j.succ : ℕ) = j + 1 :=

by cases j; simp [fin.succ]

lemma succ_pos (a : fin n) : (0 : fin (n + 1)) < a.succ := by simp [lt_iff_coe_lt_coe]

def succ_embedding (n : ℕ) : fin n ↪o fin (n + 1) :=

order_embedding.of_strict_mono fin.succ $ λ ⟨i, hi⟩ ⟨j, hj⟩ h, succ_lt_succ h

@[simp] lemma coe_succ_embedding : ⇑(succ_embedding n) = fin.succ := rfl

@[simp] lemma succ_le_succ_iff : a.succ ≤ b.succ ↔ a ≤ b :=

(succ_embedding n).le_iff_le

@[simp] lemma succ_lt_succ_iff : a.succ < b.succ ↔ a < b :=

(succ_embedding n).lt_iff_lt

lemma succ_injective (n : ℕ) : injective (@fin.succ n) :=

(succ_embedding n).injective

@[simp] lemma succ_inj {a b : fin n} : a.succ = b.succ ↔ a = b :=

(succ_injective n).eq_iff

lemma succ_ne_zero {n} : ∀ k : fin n, fin.succ k ≠ 0

| ⟨k, hk⟩ heq := nat.succ_ne_zero k $ ext_iff.1 heq

@[simp] lemma succ_zero_eq_one [ne_zero n] : fin.succ (0 : fin n) = 1 :=

unfreezingI { cases n },

{ exact (ne_zero.ne 0 rfl).elim },

{ refl }

@[simp] lemma succ_zero_eq_one' : fin.succ (0 : fin (n+1)) = 1 := rfl

@[simp] lemma succ_one_eq_two [ne_zero n] : fin.succ (1 : fin (n + 1)) = 2 :=

unfreezingI { cases n },

{ exact (ne_zero.ne 0 rfl).elim },

{ refl }

@[simp] lemma succ_one_eq_two' : fin.succ (1 : fin (n + 2)) = 2 := rfl

@[simp] lemma succ_mk (n i : ℕ) (h : i < n) : fin.succ ⟨i, h⟩ = ⟨i + 1, nat.succ_lt_succ h⟩ :=

rfl

lemma mk_succ_pos (i : ℕ) (h : i < n) : (0 : fin (n + 1)) < ⟨i.succ, add_lt_add_right h 1⟩ :=

by { rw [lt_iff_coe_lt_coe, coe_zero], exact nat.succ_pos i }

lemma one_lt_succ_succ (a : fin n) : (1 : fin (n + 2)) < a.succ.succ :=

cases n,

{ exact fin_zero_elim a },

{ rw [←succ_zero_eq_one, succ_lt_succ_iff], exact succ_pos a }

@[simp] lemma add_one_lt_iff {n : ℕ} {k : fin (n + 2)} :

k + 1 < k ↔ k = last _ :=

simp only [lt_iff_coe_lt_coe, coe_add, coe_last, ext_iff],

cases k with k hk,

rcases (le_of_lt_succ hk).eq_or_lt with rfl|hk',

{ simp },

{ simp [hk'.ne, mod_eq_of_lt (succ_lt_succ hk'), le_succ _] }

@[simp] lemma add_one_le_iff {n : ℕ} {k : fin (n + 1)} :

k + 1 ≤ k ↔ k = last _ :=

cases n,

{ simp [subsingleton.elim (k + 1) k, subsingleton.elim (fin.last _) k] },

rw [←not_iff_not, ←add_one_lt_iff, lt_iff_le_and_ne, not_and'],

refine ⟨λ h _, h, λ h, h _⟩,

rw [ne.def, ext_iff, coe_add_one],

split_ifs with hk hk;

simp [hk, eq_comm],

@[simp] lemma last_le_iff {n : ℕ} {k : fin (n + 1)} :

last n ≤ k ↔ k = last n :=

top_le_iff

@[simp] lemma lt_add_one_iff {n : ℕ} {k : fin (n + 1)} :

k < k + 1 ↔ k < last n :=

rw ←not_iff_not,

simp

@[simp] lemma le_zero_iff {n : ℕ} [ne_zero n] {k : fin n} :

k ≤ 0 ↔ k = 0 :=

⟨λ h, fin.eq_of_veq $ by rw [nat.eq_zero_of_le_zero h]; refl, by rintro rfl; refl⟩

lemma succ_succ_ne_one (a : fin n) : fin.succ (fin.succ a) ≠ 1 := ne_of_gt (one_lt_succ_succ a)

def cast_lt (i : fin m) (h : i.1 < n) : fin n := ⟨i.1, h⟩

@[simp] lemma coe_cast_lt (i : fin m) (h : i.1 < n) : (cast_lt i h : ℕ) = i := rfl

@[simp] lemma cast_lt_mk (i n m : ℕ) (hn : i < n) (hm : i < m) : cast_lt ⟨i, hn⟩ hm = ⟨i, hm⟩ := rfl

def cast_le (h : n ≤ m) : fin n ↪o fin m :=

order_embedding.of_strict_mono (λ a, cast_lt a (lt_of_lt_of_le a.2 h)) $ λ a b h, h

@[simp] lemma coe_cast_le (h : n ≤ m) (i : fin n) : (cast_le h i : ℕ) = i := rfl

@[simp] lemma cast_le_mk (i n m : ℕ) (hn : i < n) (h : n ≤ m) :

cast_le h ⟨i, hn⟩ = ⟨i, lt_of_lt_of_le hn h⟩ := rfl

@[simp] lemma cast_le_zero {n m : ℕ} (h : n.succ ≤ m.succ) :

cast_le h 0 = 0 :=

by simp [eq_iff_veq]

@[simp] lemma range_cast_le {n k : ℕ} (h : n ≤ k) :

set.range (cast_le h) = {i | (i : ℕ) < n} :=

set.ext (λ x, ⟨λ ⟨y, hy⟩, hy ▸ y.2, λ hx, ⟨⟨x, hx⟩, fin.ext rfl⟩⟩)

@[simp] lemma coe_of_injective_cast_le_symm {n k : ℕ} (h : n ≤ k) (i : fin k) (hi) :

((equiv.of_injective _ (cast_le h).injective).symm ⟨i, hi⟩ : ℕ) = i :=

rw ← coe_cast_le,

exact congr_arg coe (equiv.apply_of_injective_symm _ _)

@[simp] lemma cast_le_succ {m n : ℕ} (h : (m + 1) ≤ (n + 1)) (i : fin m) :

cast_le h i.succ = (cast_le (nat.succ_le_succ_iff.mp h) i).succ :=

by simp [fin.eq_iff_veq]

@[simp] lemma cast_le_cast_le {k m n} (km : k ≤ m) (mn : m ≤ n) (i : fin k) :

fin.cast_le mn (fin.cast_le km i) = fin.cast_le (km.trans mn) i :=

fin.ext (by simp only [coe_cast_le])

@[simp] lemma cast_le_comp_cast_le {k m n} (km : k ≤ m) (mn : m ≤ n) :

fin.cast_le mn ∘ fin.cast_le km = fin.cast_le (km.trans mn) :=

funext (cast_le_cast_le km mn)

def cast (eq : n = m) : fin n ≃o fin m :=

{ to_equiv := ⟨cast_le eq.le, cast_le eq.symm.le, λ a, eq_of_veq rfl, λ a, eq_of_veq rfl⟩,

map_rel_iff' := λ a b, iff.rfl }

@[simp] lemma symm_cast (h : n = m) : (cast h).symm = cast h.symm := rfl

lemma coe_cast (h : n = m) (i : fin n) : (cast h i : ℕ) = i := rfl

@[simp] lemma cast_zero {n' : ℕ} [ne_zero n] {h : n = n'} :

cast h (0 : fin n) = by { haveI : ne_zero n' := by { rw ← h; apply_instance }, exact 0 } :=

ext rfl

@[simp] lemma cast_last {n' : ℕ} {h : n + 1 = n' + 1} :

cast h (last n) = last n' :=

ext (by rw [coe_cast, coe_last, coe_last, nat.succ_injective h])

@[simp] lemma cast_mk (h : n = m) (i : ℕ) (hn : i < n) :

cast h ⟨i, hn⟩ = ⟨i, lt_of_lt_of_le hn h.le⟩ := rfl

@[simp] lemma cast_trans {k : ℕ} (h : n = m) (h' : m = k) {i : fin n} :

cast h' (cast h i) = cast (eq.trans h h') i := rfl

@[simp] lemma cast_refl (h : n = n := rfl) : cast h = order_iso.refl (fin n) :=

by { ext, refl }

lemma cast_le_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} :

(cast_le h' : fin m → fin n) = fin.cast h :=

funext (λ _, rfl)

lemma cast_to_equiv (h : n = m) : (cast h).to_equiv = equiv.cast (h ▸ rfl) :=

by { subst h, simp }

lemma cast_eq_cast (h : n = m) : (cast h : fin n → fin m) = _root_.cast (h ▸ rfl) :=

by { subst h, ext, simp }

def cast_add (m) : fin n ↪o fin (n + m) := cast_le $ nat.le_add_right n m

@[simp] lemma coe_cast_add (m : ℕ) (i : fin n) : (cast_add m i : ℕ) = i := rfl

@[simp] lemma cast_add_zero : (cast_add 0 : fin n → fin (n + 0)) = cast rfl := rfl

lemma cast_add_lt {m : ℕ} (n : ℕ) (i : fin m) : (cast_add n i : ℕ) < m := i.2

@[simp] lemma cast_add_mk (m : ℕ) (i : ℕ) (h : i < n) :

cast_add m ⟨i, h⟩ = ⟨i, lt_add_right i n m h⟩ := rfl

@[simp] lemma cast_add_cast_lt (m : ℕ) (i : fin (n + m)) (hi : i.val < n) :

cast_add m (cast_lt i hi) = i :=

ext rfl

@[simp] lemma cast_lt_cast_add (m : ℕ) (i : fin n) :

cast_lt (cast_add m i) (cast_add_lt m i) = i :=

ext rfl

lemma cast_add_cast {n n' : ℕ} (m : ℕ) (i : fin n') (h : n' = n) :

cast_add m (fin.cast h i) = fin.cast (congr_arg _ h) (cast_add m i) :=

ext rfl

lemma cast_cast_add_left {n n' m : ℕ} (i : fin n') (h : n' + m = n + m) :

cast h (cast_add m i) = cast_add m (cast (add_right_cancel h) i) :=

ext rfl

@[simp] lemma cast_cast_add_right {n m m' : ℕ} (i : fin n) (h : n + m' = n + m) :

cast h (cast_add m' i) = cast_add m i :=

ext rfl

lemma cast_add_cast_add {m n p : ℕ} (i : fin m) :

cast_add p (cast_add n i) = cast (add_assoc _ _ _).symm (cast_add (n + p) i) :=

ext rfl

@[simp] lemma cast_succ_eq {n' : ℕ} (i : fin n) (h : n.succ = n'.succ) :

cast h i.succ = (cast (nat.succ.inj h) i).succ :=

ext $ by simp

lemma succ_cast_eq {n' : ℕ} (i : fin n) (h : n = n') : (cast h i).succ = cast (by rw h) i.succ :=

ext $ by simp

def cast_succ : fin n ↪o fin (n + 1) := cast_add 1

@[simp] lemma coe_cast_succ (i : fin n) : (i.cast_succ : ℕ) = i := rfl

@[simp] lemma cast_succ_mk (n i : ℕ) (h : i < n) : cast_succ ⟨i, h⟩ = ⟨i, nat.lt.step h⟩ := rfl

@[simp] lemma cast_cast_succ {n' : ℕ} {h : n + 1 = n' + 1} {i : fin n} :

cast h (cast_succ i) = cast_succ (cast (nat.succ_injective h) i) :=

by { ext, simp only [coe_cast, coe_cast_succ] }

lemma cast_succ_lt_succ (i : fin n) : i.cast_succ < i.succ :=

lt_iff_coe_lt_coe.2 $ by simp only [coe_cast_succ, coe_succ, nat.lt_succ_self]

lemma le_cast_succ_iff {i : fin (n + 1)} {j : fin n} : i ≤ j.cast_succ ↔ i < j.succ :=

by simpa [lt_iff_coe_lt_coe, le_iff_coe_le_coe] using nat.succ_le_succ_iff.symm

lemma cast_succ_lt_iff_succ_le {n : ℕ} {i : fin n} {j : fin (n+1)} :

i.cast_succ < j ↔ i.succ ≤ j :=

by simpa only [fin.lt_iff_coe_lt_coe, fin.le_iff_coe_le_coe, fin.coe_succ, fin.coe_cast_succ]

using nat.lt_iff_add_one_le

@[simp] lemma succ_last (n : ℕ) : (last n).succ = last (n.succ) := rfl

@[simp] lemma succ_eq_last_succ {n : ℕ} (i : fin n.succ) :

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

by rw [← succ_last, (succ_injective _).eq_iff]

@[simp] lemma cast_succ_cast_lt (i : fin (n + 1)) (h : (i : ℕ) < n) : cast_succ (cast_lt i h) = i :=

fin.eq_of_veq rfl

@[simp] lemma cast_lt_cast_succ {n : ℕ} (a : fin n) (h : (a : ℕ) < n) :

cast_lt (cast_succ a) h = a :=

by cases a; refl

@[simp] lemma cast_succ_lt_cast_succ_iff : a.cast_succ < b.cast_succ ↔ a < b :=

(@cast_succ n).lt_iff_lt

lemma cast_succ_injective (n : ℕ) : injective (@fin.cast_succ n) :=

(cast_succ : fin n ↪o _).injective

lemma cast_succ_inj {a b : fin n} : a.cast_succ = b.cast_succ ↔ a = b :=

(cast_succ_injective n).eq_iff

lemma cast_succ_lt_last (a : fin n) : cast_succ a < last n := lt_iff_coe_lt_coe.mpr a.is_lt

@[simp] lemma cast_succ_zero [ne_zero n] : cast_succ (0 : fin n) = 0 := rfl

@[simp] lemma cast_succ_one {n : ℕ} : fin.cast_succ (1 : fin (n + 2)) = 1 := rfl

lemma cast_succ_pos [ne_zero n] {i : fin n} (h : 0 < i) : 0 < cast_succ i :=

by simpa [lt_iff_coe_lt_coe] using h

@[simp] lemma cast_succ_eq_zero_iff [ne_zero n] (a : fin n) : a.cast_succ = 0 ↔ a = 0 :=

fin.ext_iff.trans $ (fin.ext_iff.trans $ by exact iff.rfl).symm

lemma cast_succ_ne_zero_iff [ne_zero n] (a : fin n) : a.cast_succ ≠ 0 ↔ a ≠ 0 :=

not_iff_not.mpr $ cast_succ_eq_zero_iff a

lemma cast_succ_fin_succ (n : ℕ) (j : fin n) :

cast_succ (fin.succ j) = fin.succ (cast_succ j) :=

by simp [fin.ext_iff]

@[norm_cast, simp] lemma coe_eq_cast_succ : (a : fin (n + 1)) = a.cast_succ :=

ext,

exact coe_val_of_lt (nat.lt.step a.is_lt),

@[simp] lemma coe_succ_eq_succ : a.cast_succ + 1 = a.succ :=

cases n,

{ exact fin_zero_elim a },

{ simp [a.is_lt, eq_iff_veq, add_def, nat.mod_eq_of_lt] }

lemma lt_succ : a.cast_succ < a.succ :=

by { rw [cast_succ, lt_iff_coe_lt_coe, coe_cast_add, coe_succ], exact lt_add_one a.val }

@[simp] lemma range_cast_succ {n : ℕ} :

set.range (cast_succ : fin n → fin n.succ) = {i | (i : ℕ) < n} :=

range_cast_le _

@[simp] lemma coe_of_injective_cast_succ_symm {n : ℕ} (i : fin (n+1)) (hi) :

((equiv.of_injective cast_succ (cast_succ_injective _)).symm ⟨i, hi⟩ : ℕ) = i :=

rw ← coe_cast_succ,

exact congr_arg coe (equiv.apply_of_injective_symm _ _)

lemma succ_cast_succ {n : ℕ} (i : fin n) :

i.cast_succ.succ = i.succ.cast_succ :=

fin.ext (by simp)

def add_nat (m) : fin n ↪o fin (n + m) :=

order_embedding.of_strict_mono (λ i, ⟨(i : ℕ) + m, add_lt_add_right i.2 _⟩) $

λ i j h, lt_iff_coe_lt_coe.2 $ add_lt_add_right h _

@[simp] lemma coe_add_nat (m : ℕ) (i : fin n) : (add_nat m i : ℕ) = i + m := rfl

@[simp] lemma add_nat_one {i : fin n} : add_nat 1 i = i.succ :=

by { ext, rw [coe_add_nat, coe_succ] }

lemma le_coe_add_nat (m : ℕ) (i : fin n) : m ≤ add_nat m i := nat.le_add_left _ _

@[simp] lemma add_nat_mk (n i : ℕ) (hi : i < m) :

add_nat n ⟨i, hi⟩ = ⟨i + n, add_lt_add_right hi n⟩ := rfl

@[simp] lemma cast_add_nat_zero {n n' : ℕ} (i : fin n) (h : n + 0 = n') :

cast h (add_nat 0 i) = cast ((add_zero _).symm.trans h) i :=

ext $ add_zero _

lemma add_nat_cast {n n' m : ℕ} (i : fin n') (h : n' = n) :

add_nat m (cast h i) = cast (congr_arg _ h) (add_nat m i) :=

ext rfl

lemma cast_add_nat_left {n n' m : ℕ} (i : fin n') (h : n' + m = n + m) :

cast h (add_nat m i) = add_nat m (cast (add_right_cancel h) i) :=

ext rfl

@[simp] lemma cast_add_nat_right {n m m' : ℕ} (i : fin n) (h : n + m' = n + m) :

cast h (add_nat m' i) = add_nat m i :=

ext $ (congr_arg ((+) (i : ℕ)) (add_left_cancel h) : _)

def nat_add (n) {m} : fin m ↪o fin (n + m) :=

order_embedding.of_strict_mono (λ i, ⟨n + (i : ℕ), add_lt_add_left i.2 _⟩) $

λ i j h, lt_iff_coe_lt_coe.2 $ add_lt_add_left h _

@[simp] lemma coe_nat_add (n : ℕ) {m : ℕ} (i : fin m) : (nat_add n i : ℕ) = n + i := rfl

@[simp] lemma nat_add_mk (n i : ℕ) (hi : i < m) :

nat_add n ⟨i, hi⟩ = ⟨n + i, add_lt_add_left hi n⟩ := rfl

lemma le_coe_nat_add (m : ℕ) (i : fin n) : m ≤ nat_add m i := nat.le_add_right _ _

lemma nat_add_zero {n : ℕ} : fin.nat_add 0 = (fin.cast (zero_add n).symm).to_rel_embedding :=

by { ext, apply zero_add }

lemma nat_add_cast {n n' : ℕ} (m : ℕ) (i : fin n') (h : n' = n) :

nat_add m (cast h i) = cast (congr_arg _ h) (nat_add m i) :=

ext rfl

lemma cast_nat_add_right {n n' m : ℕ} (i : fin n') (h : m + n' = m + n) :

cast h (nat_add m i) = nat_add m (cast (add_left_cancel h) i) :=

ext rfl

@[simp] lemma cast_nat_add_left {n m m' : ℕ} (i : fin n) (h : m' + n = m + n) :

cast h (nat_add m' i) = nat_add m i :=

ext $ (congr_arg (+ (i : ℕ)) (add_right_cancel h) : _)

lemma cast_add_nat_add (p m : ℕ) {n : ℕ} (i : fin n) :

cast_add p (nat_add m i) = cast (add_assoc _ _ _).symm (nat_add m (cast_add p i)) :=

ext rfl

lemma nat_add_cast_add (p m : ℕ) {n : ℕ} (i : fin n) :

nat_add m (cast_add p i) = cast (add_assoc _ _ _) (cast_add p (nat_add m i)) :=

ext rfl

lemma nat_add_nat_add (m n : ℕ) {p : ℕ} (i : fin p) :

nat_add m (nat_add n i) = cast (add_assoc _ _ _) (nat_add (m + n) i) :=

ext $ (add_assoc _ _ _).symm

@[simp] lemma cast_nat_add_zero {n n' : ℕ} (i : fin n) (h : 0 + n = n') :

cast h (nat_add 0 i) = cast ((zero_add _).symm.trans h) i :=

ext $ zero_add _

@[simp] lemma cast_nat_add (n : ℕ) {m : ℕ} (i : fin m) :

cast (add_comm _ _) (nat_add n i) = add_nat n i :=

ext $ add_comm _ _

@[simp] lemma cast_add_nat {n : ℕ} (m : ℕ) (i : fin n) :