case intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
t : ℕ
ht : Finset.max (image (fun v => degree G v) univ) = ↑t
⊢ ∃ v, maxDegree G = degree G v
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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, maxDegree G = degree G v
obtain ⟨t, ht⟩ := max_of_nonempty (univ_nonempty.image fun v => G.degree v)
case intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
t : ℕ
ht : Finset.max (image (fun v => degree G v) univ) = ↑t
ht₂ : t ∈ image (fun v => degree G v) univ
⊢ ∃ v, maxDegree G = degree G v
case intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
t : ℕ
ht : Finset.max (image (fun v => degree G v) univ) = ↑t
⊢ ∃ v, maxDegree G = degree G v
have ht₂ := mem_of_max ht
case intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
t : ℕ
ht : Finset.max (image (fun v => degree G v) univ) = ↑t
ht₂ : ∃ a, True ∧ degree G a = t
⊢ ∃ v, maxDegree G = degree G v
case intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
t : ℕ
ht : Finset.max (image (fun v => degree G v) univ) = ↑t
ht₂ : t ∈ image (fun v => degree G v) univ
⊢ ∃ v, maxDegree G = degree G v
simp only [mem_image, mem_univ, exists_prop_of_true] at ht₂
case intro.intro.intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
left✝ : True
ht : Finset.max (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ ∃ v, maxDegree G = degree G v
case intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
t : ℕ
ht : Finset.max (image (fun v => degree G v) univ) = ↑t
ht₂ : ∃ a, True ∧ degree G a = t
⊢ ∃ v, maxDegree G = degree G v
rcases ht₂ with ⟨v, _, rfl⟩
case intro.intro.intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
left✝ : True
ht : Finset.max (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ maxDegree G = degree G v
case intro.intro.intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
left✝ : True
ht : Finset.max (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ ∃ v, maxDegree G = degree G v
refine' ⟨v, _⟩
case intro.intro.intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
left✝ : True
ht : Finset.max (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ Option.getD (↑(degree G v)) 0 = degree G v
case intro.intro.intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
left✝ : True
ht : Finset.max (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ maxDegree G = degree G v
rw [maxDegree, ht]
no goals
case intro.intro.intro
ι : Sort ?u.292636
𝕜 : Type ?u.292639
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
left✝ : True
ht : Finset.max (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ Option.getD (↑(degree G v)) 0 = degree G v
rfl