internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.t_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : CliqueFreeSet A (t + 2)
hv : v ∈ A
⊢ CliqueFreeSet (nbhdRes G v A) (t + 1)
Tactic:
rw [CliqueFreeSet] at *
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
⊢ ∀ (B : Finset α), B ⊆ nbhdRes G v A → ¬IsNClique G (t + 1) B
Theorem: SimpleGraph.t_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
⊢ ∀ (B : Finset α), B ⊆ nbhdRes G v A → ¬IsNClique G (t + 1) B
Tactic:
intro B hB
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
⊢ ¬IsNClique G (t + 1) B
Theorem: SimpleGraph.t_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
⊢ ¬IsNClique G (t + 1) B
Tactic:
contrapose! hA
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ ∃ B, B ⊆ A ∧ IsNClique G (t + 2) B
Theorem: SimpleGraph.t_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ ∃ B, B ⊆ A ∧ IsNClique G (t + 2) B
Tactic:
refine ⟨insert v B,?_, isSuccClique hv hB hA⟩
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ insert v B ⊆ A
Theorem: SimpleGraph.t_clique_free
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
hA : IsNClique G (t + 1) B
⊢ insert v B ⊆ A
Tactic:
exact insert_subset hv (subset_trans hB (G.sub_res_nbhd_A v A))
Proof state after:
no goals
Theorem: Turanpartition.two
Proof state before:
a : ℕ
⊢ 2 * Nat.choose a 2 = a * (a - 1)
Tactic:
induction a with
| zero => rfl
| succ n ih => 
  cases n with
  | zero => rfl
  | succ n =>
    rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
    rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul];
    congr; rw [add_comm]
Proof state after:
no goals
Theorem: Turanpartition.two
Proof state before:
case zero

⊢ 2 * Nat.choose zero 2 = zero * (zero - 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Turanpartition.two
Proof state before:
case succ
n : ℕ
ih : 2 * Nat.choose n 2 = n * (n - 1)
⊢ 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
Tactic:
cases n with
| zero => rfl
| succ n =>
  rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
  rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul];
  congr; rw [add_comm]
Proof state after:
no goals
Theorem: Turanpartition.two
Proof state before:
case succ.zero
ih : 2 * Nat.choose zero 2 = zero * (zero - 1)
⊢ 2 * Nat.choose (succ zero) 2 = succ zero * (succ zero - 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Turanpartition.two
Proof state before:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * Nat.choose (succ (succ n)) 2 = succ (succ n) * (succ (succ n) - 1)
Tactic:
rw [Nat.choose,Nat.choose_one_right,mul_add,ih]
Proof state after:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * (n + 1) + succ n * (succ n - 1) = succ (succ n) * (succ (succ n) - 1)
Theorem: Turanpartition.two
Proof state before:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 * (n + 1) + succ n * (succ n - 1) = succ (succ n) * (succ (succ n) - 1)
Tactic:
rw [succ_sub_succ_eq_sub,tsub_zero,mul_comm _ n,← add_mul]
Proof state after:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ (2 + n) * (n + 1) = succ (succ n) * (succ (succ n) - 1)
Theorem: Turanpartition.two
Proof state before:
case succ.succ
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ (2 + n) * (n + 1) = succ (succ n) * (succ (succ n) - 1)
Tactic:
congr
Proof state after:
case succ.succ.e_a
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 + n = succ (succ n)
Theorem: Turanpartition.two
Proof state before:
case succ.succ.e_a
n : ℕ
ih : 2 * Nat.choose (succ n) 2 = succ n * (succ n - 1)
⊢ 2 + n = succ (succ n)
Tactic:
rw [add_comm]
Proof state after:
no goals
Theorem: Turanpartition.square
Proof state before:
b c : ℕ
⊢ (b + c) ^ 2 = b ^ 2 + 2 * b * c + c ^ 2
Tactic:
rw [pow_two,add_mul, mul_add,mul_add,pow_two,pow_two,mul_comm c,two_mul,add_mul,add_assoc,add_assoc,add_assoc]
Proof state after:
no goals
Theorem: Turanpartition.tn_turanNumb'
Proof state before:
t n : ℕ
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2
Tactic:
rw [tN,tN']
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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)
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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)
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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)
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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)
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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]
Proof state after:
no goals
Theorem: Turanpartition.tn_turanNumb'
Proof 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 ⊢
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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 ⊢
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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]
Proof state after:
no goals
Theorem: Turanpartition.tn_turanNumb'
Proof 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]
Proof state after:
no goals
Theorem: Turanpartition.tn_turanNumb'
Proof 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]
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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]
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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)]
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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]
Proof state after:
no goals
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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
Theorem: Turanpartition.tn_turanNumb'
Proof 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
Proof 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