-- Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
theorem even_card_odd_degree_vertices [Fintype V] [DecidableRel G.Adj] :
    Even #{v | Odd (G.degree v)}

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#(filter (fun x => ¬↑(G.degree x) = 0) univ)) = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Tactic:
rw [← ZMod.eq_zero_iff_even]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#(filter (fun x => ¬↑(G.degree x) = 0) univ)) = 0
⊢ ↑(#(filter (fun v => Odd (G.degree v)) univ)) = 0

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#(filter (fun x => ¬↑(G.degree x) = 0) univ)) = 0
⊢ ↑(#(filter (fun v => Odd (G.degree v)) univ)) = 0

Tactic:
convert h

Result:
case h.e'_2.h.e'_3.h.e'_2.h.e'_2.h.a
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#(filter (fun x => ¬↑(G.degree x) = 0) univ)) = 0
x✝ : V
⊢ Odd (G.degree x✝) ↔ ¬↑(G.degree x✝) = 0

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v : V, G.degree v) = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Tactic:
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
v : V
⊢ True

Tactic:
trivial

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : (fun n => ↑n) (∑ v : V, G.degree v) = (fun n => ↑n) (2 * #G.edgeFinset)
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Tactic:
simp only [ZMod.natCast_self, zero_mul, Nat.cast_mul] at h

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v : V, G.degree v) = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Tactic:
rw [@sum_congr _ _ _ _ (fun v => (G.degree v : ZMod 2)) (fun _v => (1 : ZMod 2)) _ rfl] at h

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ _v ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, 1 = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
⊢ ∀ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 1

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
v : V
⊢ v ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ → ↑(G.degree v) = 1

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

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
v : V
⊢ ¬↑(G.degree v) = 0 → ↑(G.degree v) = 1

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ _v ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, 1 = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Tactic:
simp only [filter_congr, mul_one, nsmul_eq_mul, sum_const, Ne] at h

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#(filter (fun x => ¬↑(G.degree x) = 0) univ)) = 0
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Proof state:
case h.e'_2.h.e'_3.h.e'_2.h.e'_2.h.a
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#(filter (fun x => ¬↑(G.degree x) = 0) univ)) = 0
x✝ : V
⊢ Odd (G.degree x✝) ↔ ¬↑(G.degree x✝) = 0

Tactic:
exact ZMod.ne_zero_iff_odd.symm

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
v : V
⊢ ¬↑(G.degree v) = 0 → ↑(G.degree v) = 1

Tactic:
rw [ZMod.eq_zero_iff_even, ZMod.eq_one_iff_odd, ← Nat.not_even_iff_odd, imp_self]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
v : V
⊢ True

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Tactic:
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : (fun n => ↑n) (∑ v : V, G.degree v) = (fun n => ↑n) (2 * #G.edgeFinset)
⊢ Even #(filter (fun v => Odd (G.degree v)) univ)

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
⊢ ∀ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 1

Tactic:
intro v

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ, ↑(G.degree x) = 0
v : V
⊢ v ∈ filter (fun x => ↑(G.degree x) ≠ 0) univ → ↑(G.degree v) = 1