internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.moved_max
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
him : TuranPartition M
h1 : ¬TuranPartition N
i : ℕ
hi : i ∈ range (N.t + 1)
j : ℕ
hj : j ∈ range (N.t + 1)
v : α
hv : v ∈ MultiPart.P N i
ne : j ≠ i
hc : card (MultiPart.P N j) + 1 < card (MultiPart.P N i)
O : MultiPart α := move N (_ : i ∈ range (N.t + 1) ∧ v ∈ MultiPart.P N i) (_ : j ∈ range (N.t + 1) ∧ j ≠ i)
Ns : mpDsum N < mpDsum O
Q : MultiPart α
QA : Q.A = O.A
Qt : Q.t = O.t
Qim : TuranPartition Q
Qs : mpDsum O ≤ mpDsum Q
this : M.A = Q.A → M.t = Q.t → TuranPartition M → TuranPartition Q → mpDsum M = mpDsum Q
⊢ TuranPartition Q
Tactic:
exact Qim
Proof state after:
no goals
Theorem: SimpleGraph.turan_bound_M
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ mpDsum M ≤ 2 * turanNumb M.t (card M.A)
Tactic:
obtain ⟨N, hA, ht, iN, sN⟩ := moved M
Proof state after:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum M ≤ 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum M ≤ 2 * turanNumb M.t (card M.A)
Tactic:
apply le_trans sN _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N ≤ 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N ≤ 2 * turanNumb M.t (card M.A)
Tactic:
apply le_of_eq
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : TuranPartition N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Tactic:
rw [turanPartition_iff_not_moveable] at iN
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : ¬Moveable N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : ¬Moveable N
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Tactic:
rw [Moveable] at iN
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : ¬¬Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : ¬¬Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Tactic:
rw [Classical.not_not] at iN
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card M.A)
Tactic:
rw [← hA]
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb M.t (card N.A)
Tactic:
rw [← ht]
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb N.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
⊢ mpDsum N = 2 * turanNumb N.t (card N.A)
Tactic:
have := bal_turan_bd (turan_bal iN)
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : (sumSq N.t fun i => card (MultiPart.P N i)) + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ mpDsum N = 2 * turanNumb N.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : (sumSq N.t fun i => card (MultiPart.P N i)) + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ mpDsum N = 2 * turanNumb N.t (card N.A)
Tactic:
rw [sumSq] at this
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ mpDsum N = 2 * turanNumb N.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ mpDsum N = 2 * turanNumb N.t (card N.A)
Tactic:
rw [mpDsum]
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ ∑ v in N.A, degree (mp N) v = 2 * turanNumb N.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ ∑ v in N.A, degree (mp N) v = 2 * turanNumb N.t (card N.A)
Tactic:
rw [mp_deg_sum_sq]
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 = 2 * turanNumb N.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 = 2 * turanNumb N.t (card N.A)
Tactic:
rw [← this, add_comm]
Proof state after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ 2 * turanNumb N.t (card N.A) + ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 -
      ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 =
    2 * turanNumb N.t (card N.A)
Theorem: SimpleGraph.turan_bound_M
Proof state before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : N.A = M.A
ht : N.t = M.t
iN : Balanced N.t fun i => card (MultiPart.P N i)
sN : mpDsum M ≤ mpDsum N
this : ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 + 2 * turanNumb N.t (card N.A) = card N.A ^ 2
⊢ 2 * turanNumb N.t (card N.A) + ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 -
      ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2 =
    2 * turanNumb N.t (card N.A)
Tactic:
simp only [add_tsub_cancel_right]
Proof state after:
no goals
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ M.A = univ → card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)
Tactic:
intro hA
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)
Tactic:
apply (mul_le_mul_left (by norm_num : 0 < 2)).mp
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 2 * card (edgeFinset (mp M)) ≤ 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 2 * card (edgeFinset (mp M)) ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [← sum_degrees_eq_twice_card_edges]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
have := turan_bound_M M
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : mpDsum M ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : mpDsum M ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
unfold mpDsum at this
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v in M.A, degree (mp M) v ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v in M.A, degree (mp M) v ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [hA] at this
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
rwa [card_univ] at this
Proof state after:
no goals
Theorem: SimpleGraph.turan_max_edges
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
⊢ card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α) → TuranPartition M
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
⊢ TuranPartition M
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
⊢ TuranPartition M
Tactic:
contrapose h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ ¬card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ ¬card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
Tactic:
apply Nat.ne_of_lt
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)
Tactic:
obtain ⟨N, NA, Nt, iN, le⟩ := moved M
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)
Tactic:
apply (mul_lt_mul_left (by norm_num : 0 < 2)).mp
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ 2 * card (edgeFinset (mp M)) < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ 2 * card (edgeFinset (mp M)) < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [← sum_degrees_eq_twice_card_edges]
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
have lt := moved_max N M NA Nt iN h
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
have le2 := turan_bound_M N
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
le2 : mpDsum N ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
le2 : mpDsum N ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
unfold mpDsum at *
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v in M.A, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v in M.A, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v in M.A, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v in M.A, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [hu] at *
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [NA] at *
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb N.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb N.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [Nt] at *
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [card_univ] at *
Proof state after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (Fintype.card α)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (Fintype.card α)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
exact lt_of_lt_of_le lt le2
Proof state after:
no goals
Theorem: SimpleGraph.turan_eq_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ TuranPartition M → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Tactic:
rw [turanPartition_iff_not_moveable]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ ¬Moveable M → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ ¬Moveable M → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Tactic:
unfold Moveable
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ (¬¬Balanced M.t fun i => card (MultiPart.P M i)) → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)