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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ degRes G v A = degRes G v B + degRes G v (A \ B)
Tactic:
simp_rw [degRes, nbhdRes]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (A ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (A ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
Tactic:
nth_rw 1 [← union_sdiff_of_subset hB]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card ((B ∪ A \ B) ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card ((B ∪ A \ B) ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
Tactic:
rw [inter_distrib_right B (A \ B) _]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (B ∩ neighborFinset G v ∪ A \ B ∩ neighborFinset G v) =
    card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (B ∩ neighborFinset G v ∪ A \ B ∩ neighborFinset G v) =
    card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
Tactic:
exact card_disjoint_union (sdiff_inter_disj A B _)
State after:
no goals