simp only [
  Nat.add_succ, add_zero, Nat.succ_add, sum_succ, ih, Nat.mul_succ, Nat.succ.injEq
]
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
⊢ sum (fun i => i + i / 2 + 1) (Nat.succ j + Nat.succ j) = 3 * (Nat.succ j * Nat.succ j + Nat.succ j) + 1
case succ
j : ℕ
ih : sum (fun i => i + i / 2 + 1) (j + j) = 3 * (j * j + j) + 1
hlt : 0 < 2
⊢ 3 * (j * j + j) + (j + j + Nat.succ (j + j) / 2) + (j + j + Nat.succ (Nat.succ (j + j)) / 2) =
    Nat.succ (3 * (Nat.succ j * j + j + j))