Theorem: SimpleGraph.turanPartition_deg_sum_eq (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
⊢ M.A = N.A → M.t = N.t → TuranPartition M → TuranPartition N → mpDsum M = mpDsum N
Tactic:
intro hA ht iM iN
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ mpDsum M = mpDsum N

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ mpDsum M = mpDsum N
Tactic:
unfold mpDsum
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ ∑ v in M.A, degree (mp M) v = ∑ v in N.A, degree (mp N) v

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ ∑ v in M.A, degree (mp M) v = ∑ v in N.A, degree (mp N) v
Tactic:
rw [mp_deg_sum_sq, mp_deg_sum_sq, hA]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
rw [turanPartition_iff_not_moveable, Moveable, Classical.not_not] at *
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
apply congr_arg _
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
have hN := turan_bal iN
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal N.t (card N.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal N.t (card N.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
rw [← ht, ← hA] at hN
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
have := bal_turan_help' (turan_bal iM) hN
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
this : (sumSq M.t fun i => card (MultiPart.P M i)) = sumSq M.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
this : (sumSq M.t fun i => card (MultiPart.P M i)) = sumSq M.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
rwa [← ht]
State after:
no goals