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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : TuranPartition M
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
rw [turanPartition_iff_not_moveable] at hM
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬Moveable M
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬Moveable M
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
unfold Moveable at hM
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : ¬¬Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (card M.A) fun i => card (MultiPart.P M i)
Tactic:
rw [card_uni]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (∑ i in range (M.t + 1), card (MultiPart.P M i)) fun i => card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ Bal M.t (∑ i in range (M.t + 1), card (MultiPart.P M i)) fun i => card (MultiPart.P M i)
Tactic:
exact ⟨hM, rfl⟩
State after:
no goals