-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem odd_card_odd_degree_vertices_ne [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (v : V)
    (h : Odd (G.degree v)) : Odd #{w | w ≠ v ∧ Odd (G.degree w)}

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

Tactic:
rw [← filter_filter, filter_ne', card_erase_of_mem]

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

case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ filter (fun w => Odd (G.degree w)) univ

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

Tactic:
rw [add_assoc, one_add_one_eq_two, ← Nat.mul_succ, ← two_mul]

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

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

Tactic:
exact zero_lt_two

Result:
no goals

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

Tactic:
simp only [hc, filter_congr]

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

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

Tactic:
rw [and_comm]

Result:
no goals

Proof state:
case intro.e_a
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v
⊢ k = (k - 1).succ

Tactic:
omega

Result:
no goals

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

Tactic:
ext w

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

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hh : (filter (fun v => Odd (G.degree v)) univ).Nonempty
⊢ 0 < k

Tactic:
rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh

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

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

Tactic:
refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩

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

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

Tactic:
congr

Result:
case intro.e_a
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v
⊢ k = (k - 1).succ

Proof state:
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (G.degree w)) = fun w => Odd (G.degree w) ∧ w ≠ v
⊢ v ∈ filter (fun w => Odd (G.degree w)) univ

Tactic:
simpa only [true_and, mem_filter, mem_univ]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ (filter (fun v => Odd (G.degree v)) univ).Nonempty

Tactic:
use v

Result:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ v ∈ filter (fun v => Odd (G.degree v)) univ

Proof state:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ Odd (G.degree v)

Tactic:
exact h

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ v ∈ filter (fun v => Odd (G.degree v)) univ

Tactic:
simp only [true_and, mem_filter, mem_univ]

Result:
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #(filter (fun v => Odd (G.degree v)) univ) = k + k
⊢ Odd (G.degree v)