Theorem: SimpleGraph.degOn_univ (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✝ a : α
⊢ G.degOn univ a = G.degree a
Tactic:
rw [degOn, degree, univ_inter]
State after:
no goals