internlm/Lean-Github huggingface dataset:
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ smallParts h = smallParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)
Tactic:
rfl
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ smallParts h → f (P x) = f (minP t P)
Tactic:
rw [smallParts]
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)
Tactic:
intro x
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P) (range (t + 1)) → f (P x) = f (minP t P)
Tactic:
rw [mem_filter]
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P → f (P x) = f (minP t P)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P → f (P x) = f (minP t P)
Tactic:
intro hx
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P
⊢ f (P x) = f (minP t P)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P
⊢ f (P x) = f (minP t P)
Tactic:
rw [hx.2]
Proof state after:
no goals
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = card (largeParts h) * f (minP t P + 1)
Tactic:
rw [card_eq_sum_ones, sum_mul, one_mul]
Proof state after:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = ∑ x in largeParts h, f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∑ x in largeParts h, f (P x) = ∑ x in largeParts h, f (minP t P + 1)
Tactic:
apply sum_congr
Proof state after:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ largeParts h = largeParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.h
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ largeParts h = largeParts h

case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)
Tactic:
rfl
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ largeParts h → f (P x) = f (minP t P + 1)
Tactic:
rw [largeParts]
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
⊢ ∀ (x : ℕ), x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)
Tactic:
intro x
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ filter (fun i => P i = minP t P + 1) (range (t + 1)) → f (P x) = f (minP t P + 1)
Tactic:
rw [mem_filter]
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P + 1 → f (P x) = f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P + 1 → f (P x) = f (minP t P + 1)
Tactic:
intro hx
Proof state after:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P + 1
⊢ f (P x) = f (minP t P + 1)
Theorem: Turanpartition.bal_sum_f
Proof state before:
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P + 1
⊢ f (P x) = f (minP t P + 1)
Tactic:
rw [hx.2]
Proof state after:
no goals
Theorem: Turanpartition.bal_sum'
Proof state before:
t : ℕ
P : ℕ → ℕ
h : Balanced t P
⊢ psum t P = (t + 1) * minP t P + card (largeParts h)
Tactic:
rw [bal_sum h, mul_add, mul_one, ← add_assoc, ← add_mul, parts_card_add h]
Proof state after:
no goals
Theorem: Turanpartition.bal_sum_n
Proof state before:
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
unfold Bal at hb
Proof state after:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Theorem: Turanpartition.bal_sum_n
Proof state before:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
cases' hb with hb1 hb2
Proof state after:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2 : psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Theorem: Turanpartition.bal_sum_n
Proof state before:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2 : psum t P = n
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
rw [bal_sum' hb1, ← div_add_mod n (t + 1)] at hb2
Proof state after:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2✝ : psum t P = n
hb2 : (t + 1) * minP t P + card (largeParts hb1) = (t + 1) * (n / (t + 1)) + n % (t + 1)
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Theorem: Turanpartition.bal_sum_n
Proof state before:
case intro
t n : ℕ
P : ℕ → ℕ
hb1 : Balanced t P
hb2✝ : psum t P = n
hb2 : (t + 1) * minP t P + card (largeParts hb1) = (t + 1) * (n / (t + 1)) + n % (t + 1)
⊢ minP t P = n / (t + 1) ∧ card (largeParts (_ : Balanced t P)) = n % (t + 1)
Tactic:
exact mod_tplus1 (largeParts_card hb1) (le_of_lt_succ (mod_lt n (succ_pos t))) hb2
Proof state after:
no goals
Theorem: Turanpartition.bal_sum_n_f
Proof state before:
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
unfold Bal at hb
Proof state after:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Theorem: Turanpartition.bal_sum_n_f
Proof state before:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
obtain hf := bal_sum_f hb.1
Proof state after:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Theorem: Turanpartition.bal_sum_n_f
Proof state before:
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
obtain ⟨mn, ln⟩ := bal_sum_n hb
Proof state after:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Theorem: Turanpartition.bal_sum_n_f
Proof state before:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
hf :
  ∀ (f : ℕ → ℕ),
    ∑ i in range (t + 1), f (P i) =
      card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
specialize hf f
Proof state after:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
hf :
  ∑ i in range (t + 1), f (P i) =
    card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Theorem: Turanpartition.bal_sum_n_f
Proof state before:
case intro
t n : ℕ
P : ℕ → ℕ
hb : Balanced t P ∧ psum t P = n
f : ℕ → ℕ
mn : minP t P = n / (t + 1)
ln : card (largeParts (_ : Balanced t P)) = n % (t + 1)
hf :
  ∑ i in range (t + 1), f (P i) =
    card (smallParts (_ : Balanced t P)) * f (minP t P) + card (largeParts (_ : Balanced t P)) * f (minP t P + 1)
⊢ ∑ i in range (t + 1), f (P i) = (t + 1 - n % (t + 1)) * f (n / (t + 1)) + n % (t + 1) * f (n / (t + 1) + 1)
Tactic:
rwa [mn, smallParts_card, ln] at hf
Proof state after:
no goals
Theorem: Turanpartition.bal_turan_help
Proof state before:
t n : ℕ
P : ℕ → ℕ
hb : Bal t n P
⊢ sumSq t P = turanNumb' t n
Tactic:
rw [tN',sumSq,bal_sum_n_f hb fun i => i ^ 2]
Proof state after:
no goals
Theorem: Turanpartition.bal_turan_help'
Proof state before:
t n : ℕ
P Q : ℕ → ℕ
hp : Bal t n P
hq : Bal t n Q
⊢ sumSq t P = sumSq t Q
Tactic:
rw [bal_turan_help hp]
Proof state after:
t n : ℕ
P Q : ℕ → ℕ
hp : Bal t n P
hq : Bal t n Q
⊢ turanNumb' t n = sumSq t Q
Theorem: Turanpartition.bal_turan_help'
Proof state before:
t n : ℕ
P Q : ℕ → ℕ
hp : Bal t n P
hq : Bal t n Q
⊢ turanNumb' t n = sumSq t Q
Tactic:
rw [bal_turan_help hq]
Proof state after:
no goals
Theorem: Turanpartition.bal_turan_bd
Proof state before:
t n : ℕ
P : ℕ → ℕ
hp : Bal t n P
⊢ sumSq t P + 2 * turanNumb t n = n ^ 2
Tactic:
rw [bal_turan_help hp]
Proof state after:
t n : ℕ
P : ℕ → ℕ
hp : Bal t n P
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2
Theorem: Turanpartition.bal_turan_bd
Proof state before:
t n : ℕ
P : ℕ → ℕ
hp : Bal t n P
⊢ turanNumb' t n + 2 * turanNumb t n = n ^ 2
Tactic:
exact tn_turanNumb' t n
Proof state after:
no goals
Theorem: Turanpartition.disjoint_insert_erase
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ Disjoint (erase A v) (insert v B)
Tactic:
rw [disjoint_insert_right, mem_erase]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A) ∧ Disjoint (erase A v) B
Theorem: Turanpartition.disjoint_insert_erase
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A) ∧ Disjoint (erase A v) B
Tactic:
refine ⟨?_, disjoint_of_subset_left (erase_subset v A) hd⟩
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A)
Theorem: Turanpartition.disjoint_insert_erase
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ ¬(v ≠ v ∧ v ∈ A)
Tactic:
push_neg
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ v ≠ v → ¬v ∈ A
Theorem: Turanpartition.disjoint_insert_erase
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
⊢ v ≠ v → ¬v ∈ A
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
h : v ≠ v
⊢ ¬v ∈ A
Theorem: Turanpartition.disjoint_insert_erase
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
A : Finset α
hd : Disjoint A B
h : v ≠ v
⊢ ¬v ∈ A
Tactic:
contradiction
Proof state after:
no goals
Theorem: Turanpartition.turanPartition_iff_not_moveable
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ ¬Moveable M
Tactic:
rw [Moveable, not_not]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ Balanced M.t fun i => card (MultiPart.P M i)
Theorem: Turanpartition.turanPartition_iff_not_moveable
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ Balanced M.t fun i => card (MultiPart.P M i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ¬TuranPartition M
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
rw [turanPartition_iff_not_moveable,  Moveable, Balanced] at h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h :
  ¬¬¬∀ (i : ℕ),
          i ∈ range (M.t + 1) → ∀ (j : ℕ), j ∈ range (M.t + 1) → card (MultiPart.P M i) ≤ card (MultiPart.P M j) + 1
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h :
  ¬¬¬∀ (i : ℕ),
          i ∈ range (M.t + 1) → ∀ (j : ℕ), j ∈ range (M.t + 1) → card (MultiPart.P M i) ≤ card (MultiPart.P M j) + 1
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
push_neg at h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ∃ i, i ∈ range (M.t + 1) ∧ ∃ j, j ∈ range (M.t + 1) ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ∃ i, i ∈ range (M.t + 1) ∧ ∃ j, j ∈ range (M.t + 1) ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
obtain ⟨i, hi, j, hj, hc⟩ := h
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
refine ⟨i,hi,j,hj,?_⟩
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
obtain ⟨v,hv⟩:= card_pos.1 <| pos_of_gt hc
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
have cne :=((lt_succ_self _).trans hc).ne.symm
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
⊢ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
Tactic:
refine ⟨v, hv, λ eq => ?_, hc⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
eq : j = i
⊢ False
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M j)
eq : j = i
⊢ False
Tactic:
rw [eq] at cne
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M i)
eq : j = i
⊢ False
Theorem: Turanpartition.not_turanPartition_imp
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
v : α
hv : v ∈ MultiPart.P M i
cne : card (MultiPart.P M i) ≠ card (MultiPart.P M i)
eq : j = i
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Turanpartition.insert_P'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
⊢ ∀ (v : α), v ∈ B → v ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
intro v hv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1)
Theorem: Turanpartition.insert_P'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
rw [insert_P]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else B
Theorem: Turanpartition.insert_P'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
⊢ v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else B
Tactic:
split_ifs with h_1
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1)

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ B
Theorem: Turanpartition.insert_P'
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1)
Tactic:
contradiction
Proof state after:
no goals
Theorem: Turanpartition.insert_P'
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
M : MultiPart α
h : Disjoint M.A B
v : α
hv : v ∈ B
h_1 : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ B
Tactic:
exact hv
Proof state after:
no goals
Theorem: Turanpartition.insert_C
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1) → v ∈ B
Tactic:
intro h1
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h1 : v ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ v ∈ B
Theorem: Turanpartition.insert_C
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h1 : v ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ v ∈ B
Tactic:
rw [insert_P] at h1
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h1 : v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else B
⊢ v ∈ B
Theorem: Turanpartition.insert_C
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h1 : v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else B
⊢ v ∈ B
Tactic:
split_ifs at h1 with h2
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h2 : M.t + 1 ≠ M.t + 1
h1 : v ∈ MultiPart.P M (M.t + 1)
⊢ v ∈ B

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h2 : ¬M.t + 1 ≠ M.t + 1
h1 : v ∈ B
⊢ v ∈ B
Theorem: Turanpartition.insert_C
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Finset α
v : α
M : MultiPart α
h : Disjoint M.A B
h2 : M.t + 1 ≠ M.t + 1
h1 : v ∈ MultiPart.P M (M.t + 1)
⊢ v ∈ B
Tactic:
contradiction
Proof state after:
no goals