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

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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x (A \ B), 1 = ∑ v in B, ∑ w in A \ B, 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
A B : Finset α
⊢ (fun x => ∑ x in nbhdRes G x (A \ B), 1) = fun v => ∑ w in A \ B, 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
A B : Finset α
⊢ (fun x => ∑ x in nbhdRes G x (A \ B), 1) = fun v => ∑ w in A \ B, 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
A B : Finset α
x : α
⊢ ∑ x in nbhdRes G x (A \ B), 1 = ∑ w in A \ B, 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
A B : Finset α
x : α
⊢ ∑ x in nbhdRes G x (A \ B), 1 = ∑ w in A \ B, if Adj G x w then 1 else 0
Tactic:
simp only [sum_const, Algebra.id.smul_eq_mul, mul_one, sum_boole, cast_id]
State after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ card (nbhdRes G x (A \ B)) = card (filter (fun x_1 => Adj G x x_1) (A \ B))

State before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ card (nbhdRes G x (A \ B)) = card (filter (fun x_1 => Adj G x x_1) (A \ B))
Tactic:
congr
State after:
case e_f.h.e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ nbhdRes G x (A \ B) = filter (fun x_1 => Adj G x x_1) (A \ B)

State before:
case e_f.h.e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ nbhdRes G x (A \ B) = filter (fun x_1 => Adj G x x_1) (A \ B)
Tactic:
ext
State after:
case e_f.h.e_s.a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x a✝ : α
⊢ a✝ ∈ nbhdRes G x (A \ B) ↔ a✝ ∈ filter (fun x_1 => Adj G x x_1) (A \ B)

State before:
case e_f.h.e_s.a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x a✝ : α
⊢ a✝ ∈ nbhdRes G x (A \ B) ↔ a✝ ∈ filter (fun x_1 => Adj G x x_1) (A \ B)
Tactic:
rw [mem_res_nbhd_iff, mem_filter, mem_neighborFinset]
State after:
no goals