case pos
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
⊢ maxDegree G ≤ k

case neg
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : ¬Finset.Nonempty univ
⊢ maxDegree G ≤ k
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
⊢ maxDegree G ≤ k
by_cases hV : (univ : Finset V).Nonempty
case pos
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
this : Nonempty V
⊢ maxDegree G ≤ k
case pos
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
⊢ maxDegree G ≤ k
haveI : Nonempty V := univ_nonempty_iff.mp hV
case pos.intro
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
this : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ maxDegree G ≤ k
case pos
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
this : Nonempty V
⊢ maxDegree G ≤ k
obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex
case pos.intro
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
this : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ degree G v ≤ k
case pos.intro
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
this : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ maxDegree G ≤ k
rw [hv]
no goals
case pos.intro
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : Finset.Nonempty univ
this : Nonempty V
v : V
hv : maxDegree G = degree G v
⊢ degree G v ≤ k
apply h
case neg
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : univ = ∅
⊢ maxDegree G ≤ k
case neg
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : ¬Finset.Nonempty univ
⊢ maxDegree G ≤ k
rw [not_nonempty_iff_eq_empty] at hV
case neg
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : univ = ∅
⊢ Option.getD (Finset.max ∅) 0 ≤ k
case neg
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : univ = ∅
⊢ maxDegree G ≤ k
rw [maxDegree, hV, image_empty]
no goals
case neg
ι : Sort ?u.294725
𝕜 : Type ?u.294728
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
k : ℕ
h : ∀ (v : V), degree G v ≤ k
hV : univ = ∅
⊢ Option.getD (Finset.max ∅) 0 ≤ k
exact zero_le k