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

theorem Fin.unfold_ofNat2 {n : Nat} : 2 = (succ 0).succ

def Fin.cases1 {motive : Fin 1 → Sort u} (h : motive 0) (v : Fin 1) : motive v

Equations

• Fin.cases1 h v = Fin.induction h (fun (i : Fin 0) (a : motive i.castSucc) => i.elim0) v

def Fin.cases2 {motive : Fin 2 → Sort u} (h1 : motive 0) (h2 : motive 1) (v : Fin 2) : motive v

Equations

• One or more equations did not get rendered due to their size.

def Fin.cases3 {motive : Fin 3 → Sort u} (h1 : motive 0) (h2 : motive 1) (h3 : motive 2) (v : Fin 3) : motive v

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Vect.eta1 {T : Type u_1} (t : Vect 1 T) : ↑[t 0] ⋯ = t

@[simp]

theorem Vect.eta2 {T : Type u_1} (t : Vect 2 T) : ↑[t 0, t 1] ⋯ = t

@[simp]

theorem Vect.eta3 {T : Type u_1} (t : Vect 3 T) : ↑[t 0, t 1, t 2] ⋯ = t

@[simp]

theorem Vect.inv1 {T : Sort u_1} {a b : Vect 1 T} : a = b ↔ a 0 = b 0

@[simp]

theorem Vect.inv2 {T : Sort u_1} {a b : Vect 2 T} : a = b ↔ a 0 = b 0 ∧ a 1 = b 1

@[simp]

theorem Vect.inv3 {T : Sort u_1} {a b : Vect 3 T} : a = b ↔ a 0 = b 0 ∧ a 1 = b 1 ∧ a 2 = b 2