nth_rw 3 [← mul_one b] at n1
case inr.inr
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 - b) * a + b * a + b = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
⊢ (t + 1 - b) * a ^ 2 + b * (a + 1) ^ 2 +
      2 * (a ^ 2 * Nat.choose (t + 1 - b) 2 + a * (a + 1) * b * (t + 1 - b) + (a + 1) ^ 2 * Nat.choose b 2) =
    n ^ 2
case inr.inr
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 - b) * a + b * a + b * 1 = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
⊢ (t + 1 - b) * a ^ 2 + b * (a + 1) ^ 2 +
      2 * (a ^ 2 * Nat.choose (t + 1 - b) 2 + a * (a + 1) * b * (t + 1 - b) + (a + 1) ^ 2 * Nat.choose b 2) =
    n ^ 2