Theorem: SimpleGraph.bip_count_help' (Turan4/NbhdRes.lean)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ v in B, degRes G v A = ∑ v in B, ∑ w in A, if Adj G v w then 1 else 0
Tactic:
simp_rw [degRes_ones]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x A, 1 = ∑ v in B, ∑ w in A, if Adj G v w then 1 else 0

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x A, 1 = ∑ v in B, ∑ w in A, if Adj G v w then 1 else 0
Tactic:
congr
State after:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (fun x => ∑ x in nbhdRes G x A, 1) = fun v => ∑ w in A, if Adj G v w then 1 else 0

State before:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (fun x => ∑ x in nbhdRes G x A, 1) = fun v => ∑ w in A, if Adj G v w then 1 else 0
Tactic:
ext x
State after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
x : α
⊢ ∑ x in nbhdRes G x A, 1 = ∑ w in A, if Adj G x w then 1 else 0

State before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
x : α
⊢ ∑ x in nbhdRes G x A, 1 = ∑ w in A, if Adj G x w then 1 else 0
Tactic:
rw [nbhdRes_filter,sum_filter]
State after:
no goals