rwa [maxDegRes, ht]
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this✝ : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
this : (fun v => degRes G v A) v ≤ t
⊢ degRes G v A ≤ maxDegRes G A
no goals