Theorem: Turanpartition.tn_turanNumb' (Turan4/Turanpartition.lean)

State before:
t n : ℕ
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2
Tactic:
rw [tN,tN']
State after:
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

State before:
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
Tactic:
have t1 : t + 1 - 1 = t := tsub_eq_of_eq_add rfl
State after:
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

State before:
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
Tactic:
have n1 := div_add_mod n (t + 1)
State after:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = 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

State before:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = 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
Tactic:
have n2 := mod_lt n (succ_pos t)
State after:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % succ t < succ 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

State before:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % succ t < succ 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
Tactic:
rw [succ_eq_add_one] at n2
State after:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % (t + 1) < t + 1
⊢ (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

State before:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % (t + 1) < t + 1
⊢ (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
Tactic:
have n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1 := tsub_add_cancel_of_le (le_of_lt n2)
State after:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % (t + 1) < t + 1
n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1
⊢ (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

State before:
t n : ℕ
t1 : t + 1 - 1 = t
n1 : (t + 1) * (n / (t + 1)) + n % (t + 1) = n
n2 : n % (t + 1) < t + 1
n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1
⊢ (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
Tactic:
set a := n / (t + 1)
State after:
t n : ℕ
t1 : t + 1 - 1 = t
n2 : n % (t + 1) < t + 1
n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1
a : ℕ := n / (t + 1)
n1 : (t + 1) * a + n % (t + 1) = n
⊢ (t + 1 - n % (t + 1)) * a ^ 2 + n % (t + 1) * (a + 1) ^ 2 +
      2 *
        (a ^ 2 * Nat.choose (t + 1 - n % (t + 1)) 2 + a * (a + 1) * (n % (t + 1)) * (t + 1 - n % (t + 1)) +
          (a + 1) ^ 2 * Nat.choose (n % (t + 1)) 2) =
    n ^ 2

State before:
t n : ℕ
t1 : t + 1 - 1 = t
n2 : n % (t + 1) < t + 1
n3 : t + 1 - n % (t + 1) + n % (t + 1) = t + 1
a : ℕ := n / (t + 1)
n1 : (t + 1) * a + n % (t + 1) = n
⊢ (t + 1 - n % (t + 1)) * a ^ 2 + n % (t + 1) * (a + 1) ^ 2 +
      2 *
        (a ^ 2 * Nat.choose (t + 1 - n % (t + 1)) 2 + a * (a + 1) * (n % (t + 1)) * (t + 1 - n % (t + 1)) +
          (a + 1) ^ 2 * Nat.choose (n % (t + 1)) 2) =
    n ^ 2
Tactic:
set b := n % (t + 1) with hb
State after:
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

State before:
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
Tactic:
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]
State after:
no goals

State before:
case 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 + b = n
hb : b = n % (t + 1)
hn : n = 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
Tactic:
rw [hn] at hb n1 ⊢
State after:
case 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 + b = 0
hb : b = 0 % (t + 1)
hn : n = 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) =
    0 ^ 2

State before:
case 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 + b = 0
hb : b = 0 % (t + 1)
hn : n = 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) =
    0 ^ 2
Tactic:
rw [Nat.zero_mod] at hb
State after:
case 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 + b = 0
hb : b = 0
hn : n = 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) =
    0 ^ 2

State before:
case 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 + b = 0
hb : b = 0
hn : n = 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) =
    0 ^ 2
Tactic:
rw [hb] at n3 n1 ⊢
State after:
case inl
t n : ℕ
t1 : t + 1 - 1 = t
a : ℕ := n / (t + 1)
b : ℕ := n % (t + 1)
n2 : b < t + 1
n3 : t + 1 - 0 + 0 = t + 1
n1 : (t + 1) * a + 0 = 0
hb : b = 0
hn : n = 0
⊢ (t + 1 - 0) * a ^ 2 + 0 * (a + 1) ^ 2 +
      2 * (a ^ 2 * Nat.choose (t + 1 - 0) 2 + a * (a + 1) * 0 * (t + 1 - 0) + (a + 1) ^ 2 * Nat.choose 0 2) =
    0 ^ 2

State before:
case inl
t n : ℕ
t1 : t + 1 - 1 = t
a : ℕ := n / (t + 1)
b : ℕ := n % (t + 1)
n2 : b < t + 1
n3 : t + 1 - 0 + 0 = t + 1
n1 : (t + 1) * a + 0 = 0
hb : b = 0
hn : n = 0
⊢ (t + 1 - 0) * a ^ 2 + 0 * (a + 1) ^ 2 +
      2 * (a ^ 2 * Nat.choose (t + 1 - 0) 2 + a * (a + 1) * 0 * (t + 1 - 0) + (a + 1) ^ 2 * Nat.choose 0 2) =
    0 ^ 2
Tactic:
simp_rw [tsub_zero,hn,Nat.choose_zero_succ,Nat.zero_div,zero_mul,mul_zero,add_zero,zero_pow' ,zero_mul,mul_zero]
State after:
no goals

State before:
case 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) * a + b = n
hb : b = n % (t + 1)
hn : n > 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
Tactic:
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]
State after:
no goals

State before:
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 + 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
Tactic:
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]
State after:
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 + b = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b = 0
⊢ (t + 1) * a ^ 2 + a ^ 2 * ((t + 1) * t) = n ^ 2

State before:
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 + b = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b = 0
⊢ (t + 1) * a ^ 2 + a ^ 2 * ((t + 1) * t) = n ^ 2
Tactic:
rw [hb',add_zero] at n1
State after:
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

State before:
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
Tactic:
rw [←n1,mul_pow,mul_comm (a^2),←add_mul]
State after:
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

State before:
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
Tactic:
nth_rw 1 [←mul_one (t+1)]
State after:
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) * 1 + (t + 1) * t) * a ^ 2 = (t + 1) ^ 2 * a ^ 2

State before:
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) * 1 + (t + 1) * t) * a ^ 2 = (t + 1) ^ 2 * a ^ 2
Tactic:
rw [←mul_add,add_comm 1,←pow_two]
State after:
no goals

State before:
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) * 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
Tactic:
rw [← n3, add_mul] at n1
State after:
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

State before:
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
Tactic:
nth_rw 3 [← mul_one b] at n1
State after:
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

State before:
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
Tactic:
rw [add_assoc, ← mul_add b] at n1
State after:
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 + 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

State before:
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 + 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
Tactic:
rw [← n1]
State after:
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 + 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) =
    ((t + 1 - b) * a + b * (a + 1)) ^ 2

State before:
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 + 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) =
    ((t + 1 - b) * a + b * (a + 1)) ^ 2
Tactic:
rw [mul_add, mul_add, ← mul_assoc 2, ← mul_assoc 2 ((a + 1) ^ 2)]
State after:
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 + 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 + 2 * (a * (a + 1) * b * (t + 1 - b)) + 2 * (a + 1) ^ 2 * Nat.choose b 2) =
    ((t + 1 - b) * a + b * (a + 1)) ^ 2

State before:
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 + 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 + 2 * (a * (a + 1) * b * (t + 1 - b)) + 2 * (a + 1) ^ 2 * Nat.choose b 2) =
    ((t + 1 - b) * a + b * (a + 1)) ^ 2
Tactic:
nth_rw 1 [mul_comm 2 _]
State after:
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 + 1) = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
⊢ (t + 1 - b) * a ^ 2 + b * (a + 1) ^ 2 +
      (a ^ 2 * 2 * Nat.choose (t + 1 - b) 2 + 2 * (a * (a + 1) * b * (t + 1 - b)) + 2 * (a + 1) ^ 2 * Nat.choose b 2) =
    ((t + 1 - b) * a + b * (a + 1)) ^ 2

State before:
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 + 1) = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
⊢ (t + 1 - b) * a ^ 2 + b * (a + 1) ^ 2 +
      (a ^ 2 * 2 * Nat.choose (t + 1 - b) 2 + 2 * (a * (a + 1) * b * (t + 1 - b)) + 2 * (a + 1) ^ 2 * Nat.choose b 2) =
    ((t + 1 - b) * a + b * (a + 1)) ^ 2
Tactic:
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)]
State after:
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 + 1) = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
⊢ a ^ 2 * (t + 1 - b) + b * (a + 1) ^ 2 +
      (a ^ 2 * ((t + 1 - b) * (t + 1 - b - 1)) + 2 * (a * (a + 1) * b * (t + 1 - b)) + (a + 1) ^ 2 * (b * (b - 1))) =
    ((t + 1 - b) * a) ^ 2 + 2 * ((t + 1 - b) * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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 + 1) = n
hb : b = n % (t + 1)
hn : n > 0
hb' : b > 0
⊢ a ^ 2 * (t + 1 - b) + b * (a + 1) ^ 2 +
      (a ^ 2 * ((t + 1 - b) * (t + 1 - b - 1)) + 2 * (a * (a + 1) * b * (t + 1 - b)) + (a + 1) ^ 2 * (b * (b - 1))) =
    ((t + 1 - b) * a) ^ 2 + 2 * ((t + 1 - b) * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
set c := t + 1 - b
State after:
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
⊢ a ^ 2 * c + b * (a + 1) ^ 2 + (a ^ 2 * (c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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
⊢ a ^ 2 * c + b * (a + 1) ^ 2 + (a ^ 2 * (c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
have hc2 : c - 1 + 1 = c := tsub_add_cancel_of_le (tsub_pos_of_lt n2)
State after:
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
⊢ a ^ 2 * c + b * (a + 1) ^ 2 + (a ^ 2 * (c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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
⊢ a ^ 2 * c + b * (a + 1) ^ 2 + (a ^ 2 * (c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
have hb2 : b - 1 + 1 = b := tsub_add_cancel_of_le hb'
State after:
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 + b * (a + 1) ^ 2 + (a ^ 2 * (c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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 + b * (a + 1) ^ 2 + (a ^ 2 * (c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
rw [add_comm (a^2*c),add_assoc,←add_assoc (a^2*c),←add_assoc (a^2*c),← mul_add (a^2)]
State after:
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
⊢ b * (a + 1) ^ 2 + (a ^ 2 * (c + c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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
⊢ b * (a + 1) ^ 2 + (a ^ 2 * (c + c * (c - 1)) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
nth_rw 1 [←mul_one c,←mul_add c,add_comm _ (c-1),hc2]
State after:
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
⊢ b * (a + 1) ^ 2 + (a ^ 2 * (c * c) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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
⊢ b * (a + 1) ^ 2 + (a ^ 2 * (c * c) + 2 * (a * (a + 1) * b * c) + (a + 1) ^ 2 * (b * (b - 1))) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
rw [add_comm (b*(a+1)^2),add_assoc,mul_comm b ((a+1)^2),←mul_add ((a+1)^2)]
State after:
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) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2

State before:
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) =
    (c * a) ^ 2 + 2 * (c * a) * (b * (a + 1)) + (b * (a + 1)) ^ 2
Tactic:
nth_rw 4 [←mul_one b]
State after:
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

State before:
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
Tactic:
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]
State after:
no goals