intro hA
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ M.A = univ → card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)