apply (mul_right_inj' (by norm_num : 2 ≠ 0)).mp
α : 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 α)
α : 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 α)