induction i with
| zero =>
  intro arr isLt hLen
  simp [insertSorted', *]
| succ i' ih =>
  intro arr isLt hLen
  simp [insertSorted', dbgTraceIfShared]
  split <;> simp [*]
α : Type u_1
inst✝ : Ord α
len i : Nat
⊢ ∀ (arr : Array α) (isLt : i < Array.size arr),
    Array.size arr = len → Array.size (insertSorted' arr { val := i, isLt := isLt }) = len
no goals