obtain ⟨N, NA, Nt, iN, le⟩ := moved M
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 α)
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 α)