-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem exists_maximal_degree_vertex [DecidableRel G.Adj] [Nonempty V] :
    ∃ v, G.maxDegree = G.degree v

Proof state:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : True
ht : (image (fun v => G.degree v) univ).max = ↑(G.degree v)
⊢ ∃ v, G.maxDegree = G.degree v

Tactic:
refine ⟨v, ?_⟩

Result:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : True
ht : (image (fun v => G.degree v) univ).max = ↑(G.degree v)
⊢ G.maxDegree = G.degree v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
⊢ ∃ v, G.maxDegree = G.degree v

Tactic:
have ht₂ := mem_of_max ht

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
ht₂ : t ∈ image (fun v => G.degree v) univ
⊢ ∃ v, G.maxDegree = G.degree v

Proof state:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : True
ht : (image (fun v => G.degree v) univ).max = ↑(G.degree v)
⊢ Option.getD (↑(G.degree v)) 0 = G.degree v

Tactic:
rfl

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
ht₂ : ∃ a, True ∧ G.degree a = t
⊢ ∃ v, G.maxDegree = G.degree v

Tactic:
rcases ht₂ with ⟨v, _, rfl⟩

Result:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : True
ht : (image (fun v => G.degree v) univ).max = ↑(G.degree v)
⊢ ∃ v, G.maxDegree = G.degree v

Proof state:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : True
ht : (image (fun v => G.degree v) univ).max = ↑(G.degree v)
⊢ G.maxDegree = G.degree v

Tactic:
rw [maxDegree, ht]

Result:
case intro.intro.intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
left✝ : True
ht : (image (fun v => G.degree v) univ).max = ↑(G.degree v)
⊢ Option.getD (↑(G.degree v)) 0 = G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ ∃ v, G.maxDegree = G.degree v

Tactic:
obtain ⟨t, ht⟩ := max_of_nonempty (univ_nonempty.image fun v => G.degree v)

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
⊢ ∃ v, G.maxDegree = G.degree v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
ht₂ : t ∈ image (fun v => G.degree v) univ
⊢ ∃ v, G.maxDegree = G.degree v

Tactic:
simp only [mem_image, mem_univ, exists_prop_of_true] at ht₂

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
t : ℕ
ht : (image (fun v => G.degree v) univ).max = ↑t
ht₂ : ∃ a, True ∧ G.degree a = t
⊢ ∃ v, G.maxDegree = G.degree v