induction i with
| zero =>
  intro arr isLt hLen
  simp [insertSorted, hLen]
| succ i' ih =>
  intro arr isLt hLen
  simp [insertSorted]
  split <;> try 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