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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A
Tactic:
set H : SimpleGraph α := mp (minsert M h) with hH
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A
Tactic:
simp [insert_AB]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C = ∑ x in M.A ∪ C, degRes (mp (minsert M h)) x (M.A ∪ C)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C = ∑ x in M.A ∪ C, degRes (mp (minsert M h)) x (M.A ∪ C)
Tactic:
rw [sum_union h]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ x in M.A, degRes (mp (minsert M h)) x (M.A ∪ C) + ∑ x in C, degRes (mp (minsert M h)) x (M.A ∪ C)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ x in M.A, degRes (mp (minsert M h)) x (M.A ∪ C) + ∑ x in C, degRes (mp (minsert M h)) x (M.A ∪ C)
Tactic:
rw [H.degRes_add_sum' h, H.degRes_add_sum' h]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + (∑ v in C, degRes H v M.A + ∑ v in C, degRes H v C)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + (∑ v in C, degRes H v M.A + ∑ v in C, degRes H v C)
Tactic:
rw [add_assoc, mp_int_sum M h, add_zero]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + (∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + (∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A)
Tactic:
rw [←add_assoc, card_eq_sum_ones C, mul_sum]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + ∑ x in C, 2 * card M.A * 1 =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + ∑ x in C, 2 * card M.A * 1 =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A
Tactic:
rw [mp_old_sum M h,add_assoc, add_right_inj,mul_one]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A
Tactic:
rw [ H.bip_count',← sum_add_distrib]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ x in C, (degRes H x M.A + degRes H x M.A)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ x in C, (degRes H x M.A + degRes H x M.A)
Tactic:
apply sum_congr rfl
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∀ (x : α), x ∈ C → 2 * card M.A = degRes H x M.A + degRes H x M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∀ (x : α), x ∈ C → 2 * card M.A = degRes H x M.A + degRes H x M.A
Tactic:
intro x hx
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ 2 * card M.A = degRes H x M.A + degRes H x M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ 2 * card M.A = degRes H x M.A + degRes H x M.A
Tactic:
rw [(by norm_num : 2 = 1 + 1), add_mul, one_mul]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ card M.A + card M.A = degRes H x M.A + degRes H x M.A

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ card M.A + card M.A = degRes H x M.A + degRes H x M.A
Tactic:
rw [mp_com M h x hx]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ 2 = 1 + 1
Tactic:
norm_num
State after:
no goals