case intro
ι : Sort ?u.296737
𝕜 : Type ?u.296740
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ maxDegree G < Fintype.card V
ι : Sort ?u.296737
𝕜 : Type ?u.296740
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ maxDegree G < Fintype.card V
cases' G.exists_maximal_degree_vertex with v hv
case intro
ι : Sort ?u.296737
𝕜 : Type ?u.296740
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ degree G v < Fintype.card V
case intro
ι : Sort ?u.296737
𝕜 : Type ?u.296740
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ maxDegree G < Fintype.card V
rw [hv]
no goals
case intro
ι : Sort ?u.296737
𝕜 : Type ?u.296740
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w : V
e : Sym2 V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ degree G v < Fintype.card V
apply G.degree_lt_card_verts v