cases Nat.eq_zero_or_pos n with
| inl hn =>
  rw [hn] at hb n1 ⊢
  rw [Nat.zero_mod] at hb
  rw [hb] at n3 n1 ⊢
  simp_rw [tsub_zero,hn,Nat.choose_zero_succ,Nat.zero_div,zero_mul,mul_zero,add_zero,zero_pow' ,zero_mul,mul_zero]      
| inr hn =>
  cases Nat.eq_zero_or_pos b with
  | inl hb' => 
    rw [hb', tsub_zero,mul_add,mul_add,zero_mul,←mul_assoc 2,mul_comm 2 (a^2),
        mul_assoc,two,t1,mul_zero, zero_mul,mul_zero,add_zero,add_zero,Nat.choose_zero_succ,mul_zero,mul_zero,add_zero]; 
    rw [hb',add_zero] at n1
    rw [←n1,mul_pow,mul_comm (a^2),←add_mul]
    nth_rw 1 [←mul_one (t+1)]; rw [←mul_add,add_comm 1,←pow_two]
  |inr hb' =>
    rw [← n3, add_mul] at n1 ; nth_rw 3 [← mul_one b] at n1 ; rw [add_assoc, ← mul_add b] at n1 
    rw [← n1]; rw [mul_add, mul_add, ← mul_assoc 2, ← mul_assoc 2 ((a + 1) ^ 2)]
    nth_rw 1 [mul_comm 2 _]; 
    rw [mul_assoc, two,mul_comm 2 ((a+1)^2),mul_assoc ((a+1)^2) 2,two, square ((t + 1 - b) * a) (b * (a + 1)),
      mul_comm _ (a ^ 2)]
    set c := t + 1 - b; 
    have hc2 : c - 1 + 1 = c := tsub_add_cancel_of_le (tsub_pos_of_lt n2)
    have hb2 : b - 1 + 1 = b := tsub_add_cancel_of_le hb'
    rw [add_comm (a^2*c),add_assoc,←add_assoc (a^2*c),←add_assoc (a^2*c),← mul_add (a^2)]
    nth_rw 1 [←mul_one c,←mul_add c,add_comm _ (c-1),hc2]
    rw [add_comm (b*(a+1)^2),add_assoc,mul_comm b ((a+1)^2),←mul_add ((a+1)^2)]
    nth_rw 4 [←mul_one b]; 
    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]
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 + b = n
hb : b = n % (t + 1)
⊢ (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
no goals