-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem exists_ne_odd_degree_of_exists_odd_degree [Fintype V] [DecidableRel G.Adj] (v : V)
    (h : Odd (G.degree v)) : ∃ w : V, w ≠ v ∧ Odd (G.degree w)

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
have hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)} := by
  rw [hg]
  apply Nat.succ_pos

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
hg' : 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
⊢ 0 < 2 * k + 1

Tactic:
apply Nat.succ_pos

Result:
no goals

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
hg' : 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
rcases card_pos.mp hg' with ⟨w, hw⟩

Result:
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
hg' : 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
w : V
hw : w ∈ filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩

Result:
case intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
haveI := Classical.decEq V

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
hg' : 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
w : V
hw : w ∈ filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
simp only [true_and, mem_filter, mem_univ, Ne] at hw

Result:
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
hg' : 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
w : V
hw : ¬w = v ∧ Odd (G.degree w)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
⊢ 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)

Tactic:
rw [hg]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
⊢ 0 < 2 * k + 1

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
k : ℕ
hg : #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ) = 2 * k + 1
hg' : 0 < #(filter (fun w => w ≠ v ∧ Odd (G.degree w)) univ)
w : V
hw : ¬w = v ∧ Odd (G.degree w)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
exact ⟨w, hw⟩

Result:
no goals