have t1 : t + 1 - 1 = t := tsub_eq_of_eq_add rfl
t n : ℕ
⊢ (t + 1 - n % (t + 1)) * (n / (t + 1)) ^ 2 + n % (t + 1) * (n / (t + 1) + 1) ^ 2 +
      2 *
        ((n / (t + 1)) ^ 2 * Nat.choose (t + 1 - n % (t + 1)) 2 +
            n / (t + 1) * (n / (t + 1) + 1) * (n % (t + 1)) * (t + 1 - n % (t + 1)) +
          (n / (t + 1) + 1) ^ 2 * Nat.choose (n % (t + 1)) 2) =
    n ^ 2
t n : ℕ
t1 : t + 1 - 1 = t
⊢ (t + 1 - n % (t + 1)) * (n / (t + 1)) ^ 2 + n % (t + 1) * (n / (t + 1) + 1) ^ 2 +
      2 *
        ((n / (t + 1)) ^ 2 * Nat.choose (t + 1 - n % (t + 1)) 2 +
            n / (t + 1) * (n / (t + 1) + 1) * (n % (t + 1)) * (t + 1 - n % (t + 1)) +
          (n / (t + 1) + 1) ^ 2 * Nat.choose (n % (t + 1)) 2) =
    n ^ 2