rw [add_comm (b*(a+1)^2),add_assoc,mul_comm b ((a+1)^2),←mul_add ((a+1)^2)]
case inr.inr
t n : ℕ
t1 : t + 1 - 1 = t
a : ℕ := n / (t + 1)
b : ℕ := n % (t + 1)
n2 : b < t + 1
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
c : ℕ := t + 1 - b
n3 : c + b = t + 1
n1 : c * a + b * (a + 1) = n
hc2 : c - 1 + 1 = c
hb2 : b - 1 + 1 = b
⊢ b * (a + 1) ^ 2 + (a ^ 2 * (c * c) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
case inr.inr
t n : ℕ
t1 : t + 1 - 1 = t
a : ℕ := n / (t + 1)
b : ℕ := n % (t + 1)
n2 : b < t + 1
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
c : ℕ := t + 1 - b
n3 : c + b = t + 1
n1 : c * a + b * (a + 1) = n
hc2 : c - 1 + 1 = c
hb2 : b - 1 + 1 = b
⊢ a ^ 2 * (c * c) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1) + b) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2