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

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ degRes G v univ = degree G v
Tactic:
rw [degRes, degree]
State after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ card (nbhdRes G v univ) = card (neighborFinset G v)

State before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ card (nbhdRes G v univ) = card (neighborFinset G v)
Tactic:
congr
State after:
case e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ nbhdRes G v univ = neighborFinset G v

State before:
case e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ nbhdRes G v univ = neighborFinset G v
Tactic:
rw [nbhdRes, univ_inter]
State after:
no goals