internlm/Lean-Github huggingface dataset:
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 * 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
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 + 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
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 + 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]
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 + 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
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 + 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)]
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 + 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
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 + 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 _]
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 + 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
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 + 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)]
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 + 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
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 + 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
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
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
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
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)
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
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
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
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'
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
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
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
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)]
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
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
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
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]
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
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
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
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)]
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
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
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
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]
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
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
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
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]
Proof state after:
no goals
Theorem: Turanpartition.tn_turanNumb'_2
Proof state before:
t n : ℕ
⊢ 2 * turanNumb t n = n ^ 2 - turanNumb' t n
Tactic:
rw [← tn_turanNumb' t n]
Proof state after:
t n : ℕ
⊢ 2 * turanNumb t n = turanNumb' t n + 2 * turanNumb t n - turanNumb' t n
Theorem: Turanpartition.tn_turanNumb'_2
Proof state before:
t n : ℕ
⊢ 2 * turanNumb t n = turanNumb' t n + 2 * turanNumb t n - turanNumb' t n
Tactic:
exact (add_tsub_cancel_left _ _).symm
Proof state after:
no goals
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
⊢ a = b ∧ c = d
Tactic:
have mc : c % (t + 1) = c := mod_eq_of_lt (succ_le_succ hc )
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
⊢ a = b ∧ c = d
Tactic:
have md : d % (t + 1) = d := mod_eq_of_lt (succ_le_succ hd)
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : (t + 1) * a + c = (t + 1) * b + d
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
Tactic:
rw [add_comm, add_comm _ d] at ht
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
⊢ a = b ∧ c = d
Tactic:
have hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1) := add_mul_mod_self_left c (t + 1) a
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
⊢ a = b ∧ c = d
Tactic:
have hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1) := add_mul_mod_self_left d (t + 1) b
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (c + (t + 1) * a) % (t + 1) = c % (t + 1)
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d
Tactic:
rw [mc,ht] at hmtl
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : (d + (t + 1) * b) % (t + 1) = d % (t + 1)
⊢ a = b ∧ c = d
Tactic:
rw [md,hmtl] at hmtr
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b ∧ c = d
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b ∧ c = d
Tactic:
refine' ⟨_, hmtr⟩
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : c + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Tactic:
rw [hmtr] at ht
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : d + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : d + (t + 1) * a = d + (t + 1) * b
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Tactic:
rw [add_right_inj, mul_eq_mul_left_iff] at ht
Proof state after:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : a = b ∨ t + 1 = 0
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Theorem: Turanpartition.mod_tplus1
Proof state before:
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
ht : a = b ∨ t + 1 = 0
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
⊢ a = b
Tactic:
cases ht with
| inl h => exact h
| inr h => contradiction
Proof state after:
no goals
Theorem: Turanpartition.mod_tplus1
Proof state before:
case inl
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
h : a = b
⊢ a = b
Tactic:
exact h
Proof state after:
no goals
Theorem: Turanpartition.mod_tplus1
Proof state before:
case inr
c t d a b : ℕ
hc : c ≤ t
hd : d ≤ t
mc : c % (t + 1) = c
md : d % (t + 1) = d
hmtl : (d + (t + 1) * b) % (t + 1) = c
hmtr : c = d
h : t + 1 = 0
⊢ a = b
Tactic:
contradiction
Proof state after:
no goals
Theorem: Turanpartition.small_nonempty
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (smallParts h)
Tactic:
rw [smallParts]
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Theorem: Turanpartition.small_nonempty
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
have nem : ((range (t + 1)).image fun i => P i).Nonempty :=
  (Nonempty.image_iff _).mpr nonempty_range_succ
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Theorem: Turanpartition.small_nonempty
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
set a : ℕ := min' ((range (t + 1)).image fun i => P i) nem with ha
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Theorem: Turanpartition.small_nonempty
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
have ain := min'_mem ((range (t + 1)).image fun i => P i) nem
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Theorem: Turanpartition.small_nonempty
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
ain : min' (image (fun i => P i) (range (t + 1))) nem ∈ image (fun i => P i) (range (t + 1))
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
rw [← ha, mem_image] at ain
Proof state after:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
ain : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Theorem: Turanpartition.small_nonempty
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
ain : ∃ a_1, a_1 ∈ range (t + 1) ∧ P a_1 = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
obtain ⟨k, hk1, hk2⟩ := ain
Proof state after:
case intro.intro
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Theorem: Turanpartition.small_nonempty
Proof state before:
case intro.intro
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ Finset.Nonempty (filter (fun i => P i = minP t P) (range (t + 1)))
Tactic:
use k
Proof state after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ filter (fun i => P i = minP t P) (range (t + 1))
Theorem: Turanpartition.small_nonempty
Proof state before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ filter (fun i => P i = minP t P) (range (t + 1))
Tactic:
rw [mem_filter]
Proof state after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ range (t + 1) ∧ P k = minP t P
Theorem: Turanpartition.small_nonempty
Proof state before:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ k ∈ range (t + 1) ∧ P k = minP t P
Tactic:
refine' ⟨hk1, _⟩
Proof state after:
case h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
nem : Finset.Nonempty (image (fun i => P i) (range (t + 1)))
a : ℕ := min' (image (fun i => P i) (range (t + 1))) nem
ha : a = min' (image (fun i => P i) (range (t + 1))) nem
k : ℕ
hk1 : k ∈ range (t + 1)
hk2 : P k = a
⊢ P k = minP t P