Theorem: SimpleGraph.turan_bound_M (Turan4/Multipartite.lean)

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
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)

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 _
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)

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
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)

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
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)

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
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)

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
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)

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]
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)

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]
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)

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)
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)

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
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)

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]
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)

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]
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)

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]
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)

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