Theorem: SimpleGraph.degOn_union (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Degree.lean)

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ G.degOn (s ∪ t) a = G.degOn s a + G.degOn t a
Tactic:
unfold degOn
State after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ ((s ∪ t) ∩ G.neighborFinset a).card = (s ∩ G.neighborFinset a).card + (t ∩ G.neighborFinset a).card

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ ((s ∪ t) ∩ G.neighborFinset a).card = (s ∩ G.neighborFinset a).card + (t ∩ G.neighborFinset a).card
Tactic:
rw [← card_union_of_disjoint, ← union_inter_distrib_right]
State after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ Disjoint (s ∩ G.neighborFinset a) (t ∩ G.neighborFinset a)

State before:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t : Finset α
a✝ : α
h : Disjoint s t
a : α
⊢ Disjoint (s ∩ G.neighborFinset a) (t ∩ G.neighborFinset a)
Tactic:
exact h.mono inter_subset_left inter_subset_left
State after:
no goals