Theorem: SimpleGraph.mp_deg_sum_sq' (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
Tactic:
rw [mp_deg_sum M]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A ^ 2

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A ^ 2
Tactic:
rw [pow_two]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A * card M.A
Tactic:
nth_rw 1 [card_uni]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A
Tactic:
rw [← sum_add_distrib]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A
Tactic:
rw [sum_mul]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    ∑ x in range (M.t + 1), card (MultiPart.P M x) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    ∑ x in range (M.t + 1), card (MultiPart.P M x) * card M.A
Tactic:
refine' Finset.sum_congr rfl _
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 =
        card (MultiPart.P M x) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 =
        card (MultiPart.P M x) * card M.A
Tactic:
intro x hx
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 = card (MultiPart.P M x) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 = card (MultiPart.P M x) * card M.A
Tactic:
rw [pow_two]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) * card (MultiPart.P M x) =
    card (MultiPart.P M x) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) * card (MultiPart.P M x) =
    card (MultiPart.P M x) * card M.A
Tactic:
rw [← mul_add]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * (card (M.A \ MultiPart.P M x) + card (MultiPart.P M x)) = card (MultiPart.P M x) * card M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * (card (M.A \ MultiPart.P M x) + card (MultiPart.P M x)) = card (MultiPart.P M x) * card M.A
Tactic:
rw [card_part_uni hx]
State after:
no goals