case intro
ι : Sort ?u.291752
𝕜 : Type ?u.291755
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
k : ℕ
h : ∀ (v : V), k ≤ degree G v
v : V
hv : minDegree G = degree G v
⊢ k ≤ minDegree G
ι : Sort ?u.291752
𝕜 : Type ?u.291755
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
k : ℕ
h : ∀ (v : V), k ≤ degree G v
⊢ k ≤ minDegree G
rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩
case intro
ι : Sort ?u.291752
𝕜 : Type ?u.291755
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
k : ℕ
h : ∀ (v : V), k ≤ degree G v
v : V
hv : minDegree G = degree G v
⊢ k ≤ degree G v
case intro
ι : Sort ?u.291752
𝕜 : Type ?u.291755
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
k : ℕ
h : ∀ (v : V), k ≤ degree G v
v : V
hv : minDegree G = degree G v
⊢ k ≤ minDegree G
rw [hv]
no goals
case intro
ι : Sort ?u.291752
𝕜 : Type ?u.291755
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
k : ℕ
h : ∀ (v : V), k ≤ degree G v
v : V
hv : minDegree G = degree G v
⊢ k ≤ degree G v
apply h