Theorem: SimpleGraph.mp_deg_sum (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) * card (M.A \ MultiPart.P M i)
Tactic:
nth_rw 1 [M.uni]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i, degree (mp M) v =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i, degree (mp M) v =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)
Tactic:
rw [sum_biUnion (pair_disjoint M)]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), ∑ i in MultiPart.P M x, degree (mp M) i =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)

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

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = card (MultiPart.P M x) * card (M.A \ MultiPart.P M x)
Tactic:
rw [Finset.card_eq_sum_ones, sum_mul, one_mul]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = ∑ x_1 in MultiPart.P M x, card (M.A \ MultiPart.P M x)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = ∑ x_1 in MultiPart.P M x, card (M.A \ MultiPart.P M x)
Tactic:
apply Finset.sum_congr rfl _
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∀ (x_1 : α), x_1 ∈ MultiPart.P M x → degree (mp M) x_1 = card (M.A \ MultiPart.P M x)

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
v : α
hv : v ∈ MultiPart.P M x
⊢ degree (mp M) v = card (M.A \ MultiPart.P M x)
Tactic:
exact mp_deg ⟨hx, hv⟩
State after:
no goals