-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem maxDegree_le_of_forall_degree_le [DecidableRel G.Adj] (k : ℕ) (h : ∀ v, G.degree v ≤ k) :
    G.maxDegree ≤ k

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : ¬univ.Nonempty
⊢ G.maxDegree ≤ k

Tactic:
rw [not_nonempty_iff_eq_empty] at hV

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ = ∅
⊢ G.maxDegree ≤ k

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
⊢ G.maxDegree ≤ k

Tactic:
by_cases hV : (univ : Finset V).Nonempty

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
⊢ G.maxDegree ≤ k

case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : ¬univ.Nonempty
⊢ G.maxDegree ≤ k

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
⊢ G.maxDegree ≤ k

Tactic:
haveI : Nonempty V := univ_nonempty_iff.mp hV

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
this : Nonempty V
⊢ G.maxDegree ≤ k

Proof state:
case pos.intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
this : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v ≤ k

Tactic:
apply h

Result:
no goals

Proof state:
case pos.intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
this : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.maxDegree ≤ k

Tactic:
rw [hv]

Result:
case pos.intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
this : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v ≤ k

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ = ∅
⊢ Option.getD ∅.max 0 ≤ k

Tactic:
exact k.zero_le

Result:
no goals

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
this : Nonempty V
⊢ G.maxDegree ≤ k

Tactic:
obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex

Result:
case pos.intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ.Nonempty
this : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.maxDegree ≤ k

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ = ∅
⊢ G.maxDegree ≤ k

Tactic:
rw [maxDegree, hV, image_empty]

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
k : ℕ
h : ∀ (v : V), G.degree v ≤ k
hV : univ = ∅
⊢ Option.getD ∅.max 0 ≤ k