if hil : i < l.length
then rw [dif_pos hil]; apply List.get_append_left
else
  rw [dif_neg hil]
  have : i = l.length := by
    refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
    rw [l.length_concat a] at h
    exact Nat.le_of_succ_le_succ h
  simp only [this]
  exact l.get_concat_length a _
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
no goals