import ProofExplorer.Jacobian.Library

namespace ProofExplorer.Jacobian.VectorLibrary

@[simp] theorem eight_0 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 0 = a := rfl

@[simp] theorem eight_1 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 1 = b := rfl

@[simp] theorem eight_2 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 2 = c := rfl

@[simp] theorem eight_3 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 3 = d := rfl

@[simp] theorem eight_4 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 4 = e := rfl

@[simp] theorem eight_5 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 5 = f := rfl

@[simp] theorem eight_6 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 6 = g := rfl

@[simp] theorem eight_7 {K : Type*} (a b c d e f g h : K) :
    (![a,b,c,d,e,f,g,h] : Fin 8 → K) 7 = h := rfl

end ProofExplorer.Jacobian.VectorLibrary