Where to put lemmas

Stream: std4

[Alex Keizer]

I'm working on std4#400, which add some lemmas about bitvectors, and I'm wondering where to put them.
I've previously been told that simple rfl-proven lemmas should just go in the Basic file, but I wonder where the line is for when a separate Lemmas file is warranted.

For context, these are the lemmas in question:

theorem getLsb_eq_getLsbD (x : BitVec w) (i : Fin w) :
    x.getLsb i = x.getLsbD i.val :=
  rfl

theorem getLsbD_eq_getLsb (x : BitVec w) (i : Nat) (h : i < w) :
    x.getLsbD i = x.getLsb ⟨i, h⟩ :=
  rfl

theorem getMsb_eq_getMsbD (x : BitVec w) (i : Fin w) :
    x.getMsb i = x.getMsbD i.val := by
  simp only [getMsb, Fin.rev, getLsb_eq_getLsbD, getMsbD, i.2, decide_True, Bool.true_and]
  rw [Nat.add_comm, Nat.sub_add_eq]

theorem getMsbD_eq_getMsb (x : BitVec w) (i : Nat) (h : i < w) :
    x.getMsbD i = x.getMsb ⟨i, h⟩ := by
  rw [getMsb_eq_getMsbD]

[Joe Hendrix]

For location, I'd match array and put these in a standard lemma file.