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

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

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

State before:
α : 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 α)
Tactic:
rw [Classical.not_not]
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 α)

State before:
α : 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 α)
Tactic:
intro iM
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Tactic:
apply (mul_right_inj' (by norm_num : 2 ≠ 0)).mp
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ 2 * card (edgeFinset (mp M)) = 2 * turanNumb t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ 2 * card (edgeFinset (mp M)) = 2 * turanNumb t (Fintype.card α)
Tactic:
rw [← sum_degrees_eq_twice_card_edges, ← hu, ← ht]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ ∑ v in M.A, degree (mp M) v = 2 * turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ ∑ v in M.A, degree (mp M) v = 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [mp_deg_sum_sq, ← card_univ, ← hu]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card M.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = 2 * turanNumb M.t (card M.A)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card M.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = 2 * turanNumb M.t (card M.A)
Tactic:
simp only [← bal_turan_bd (turan_bal iM), sumSq, add_tsub_cancel_left]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ 2 ≠ 0
Tactic:
norm_num
State after:
no goals