rw [turanPartition_iff_not_moveable,  Moveable, Balanced] at h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h : ¬TuranPartition M
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
h :
  ¬¬¬∀ (i : ℕ),
          i ∈ range (M.t + 1) → ∀ (j : ℕ), j ∈ range (M.t + 1) → card (MultiPart.P M i) ≤ card (MultiPart.P M j) + 1
⊢ ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j, j ∈ range (M.t + 1) ∧ ∃ v, v ∈ MultiPart.P M i ∧ j ≠ i ∧ card (MultiPart.P M j) + 1 < card (MultiPart.P M i)