case intro
ι : Sort ?u.289282
𝕜 : Type ?u.289285
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.min (image (fun v => degree G v) univ) = ↑t
⊢ ∃ v, minDegree G = degree G v
ι : Sort ?u.289282
𝕜 : Type ?u.289285
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, minDegree G = degree G v
obtain ⟨t, ht : _ = _⟩ := min_of_nonempty (univ_nonempty.image fun v => G.degree v)
case intro.intro.intro
ι : Sort ?u.289282
𝕜 : Type ?u.289285
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✝ : v ∈ univ
ht : Finset.min (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ ∃ v, minDegree G = degree G v
case intro
ι : Sort ?u.289282
𝕜 : Type ?u.289285
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.min (image (fun v => degree G v) univ) = ↑t
⊢ ∃ v, minDegree G = degree G v
obtain ⟨v, _, rfl⟩ := mem_image.mp (mem_of_min ht)
no goals
case intro.intro.intro
ι : Sort ?u.289282
𝕜 : Type ?u.289285
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✝ : v ∈ univ
ht : Finset.min (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ ∃ v, minDegree G = degree G v
refine' ⟨v, by simp [minDegree, ht]⟩
no goals
ι : Sort ?u.289282
𝕜 : Type ?u.289285
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✝ : v ∈ univ
ht : Finset.min (image (fun v => degree G v) univ) = ↑(degree G v)
⊢ minDegree G = degree G v
simp [minDegree, ht]