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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∑ v in C, degRes (mp (minsert M h)) v C = 0
Tactic:
simp only [sum_eq_zero_iff]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (x : α), x ∈ C → degRes (mp (minsert M h)) x C = 0

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
x : α
hx : x ∈ C
⊢ degRes (mp (minsert M h)) x C = 0
Tactic:
exact mp_int_degRes M h x hx
State after:
no goals