V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
haveI := Classical.decEq V
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
have hg' : (filter (fun w : V => w ≠ v ∧ Odd (G.degree w)) univ).card > 0 := by
  rw [hg]
  apply Nat.succ_pos
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
w : V
hw : w ∈ filter (fun w => w ≠ v ∧ Odd (degree G w)) univ
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
rcases card_pos.mp hg' with ⟨w, hw⟩
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
w : V
hw : ¬w = v ∧ Odd (degree G w)
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
w : V
hw : w ∈ filter (fun w => w ≠ v ∧ Odd (degree G w)) univ
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
simp only [true_and_iff, mem_filter, mem_univ, Ne.def] at hw
no goals
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
hg' : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
w : V
hw : ¬w = v ∧ Odd (degree G w)
⊢ ∃ w, w ≠ v ∧ Odd (degree G w)
exact ⟨w, hw⟩
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ 2 * k + 1 > 0
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) > 0
rw [hg]
no goals
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
this : DecidableEq V
k : ℕ
hg : card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ) = 2 * k + 1
⊢ 2 * k + 1 > 0
apply Nat.succ_pos