rw[←mul_add b,hb2,mul_comm c a,mul_pow,←pow_two c,add_assoc,add_assoc,
  add_right_inj,mul_pow,mul_add,pow_two,mul_add,mul_one,add_mul,mul_one,pow_two,mul_add,add_mul,
  add_mul,add_mul,add_mul,one_mul,mul_one,add_mul,one_mul,mul_add,mul_add,mul_add,mul_add,mul_add,mul_one,
  ← add_assoc,← add_assoc,← add_assoc,← add_assoc,←add_assoc,add_left_inj,mul_comm a (b*b),add_left_inj,
  ←add_assoc,add_left_inj,mul_comm (b*b), add_left_inj,mul_assoc 2 _ b,mul_assoc a c b,mul_comm c b,
  ←mul_assoc a,add_left_inj,mul_assoc 2,mul_assoc,mul_assoc,mul_assoc,mul_comm b a,mul_comm c,mul_assoc]
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 * 1) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
no goals