Theorem: Turanpartition.turanPartition_iff_not_moveable (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ ¬Moveable M
Tactic:
rw [Moveable, not_not]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ Balanced M.t fun i => card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ TuranPartition M ↔ Balanced M.t fun i => card (MultiPart.P M i)
Tactic:
rfl
State after:
no goals