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