obtain ⟨t, ht⟩ := max_of_nonempty (Nonempty.image hA (fun v => G.degRes v A))
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A