V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : (fun n => ↑n) (∑ v : V, degree G v) = (fun n => ↑n) (2 * card (edgeFinset G))
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v : V, degree G v) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : (fun n => ↑n) (∑ v : V, degree G v) = (fun n => ↑n) (2 * card (edgeFinset G))
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
simp only [ZMod.nat_cast_self, MulZeroClass.zero_mul, Nat.cast_mul] at h
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v : V, degree G v) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ _v in filter (fun x => ↑(degree G x) ≠ 0) univ, 1 = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
⊢ ∀ (x : V), x ∈ filter (fun x => ↑(degree G x) ≠ 0) univ → ↑(degree G x) = 1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
rw [@sum_congr _ _ _ _ (fun v => (G.degree v : ZMod 2)) (fun _v => (1 : ZMod 2)) _ rfl] at h
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ _v in filter (fun x => ↑(degree G x) ≠ 0) univ, 1 = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
simp only [filter_congr, mul_one, nsmul_eq_mul, sum_const, Ne.def] at h
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
⊢ ↑(card (filter (fun v => Odd (degree G v)) univ)) = 0
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
rw [← ZMod.eq_zero_iff_even]
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✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
x✝ : V
⊢ Odd (degree G x✝) ↔ ¬↑(degree G x✝) = 0
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
⊢ ↑(card (filter (fun v => Odd (degree G v)) univ)) = 0
convert h
no goals
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✝ : ∑ x : V, ↑(degree G x) = 0
h : ↑(card (filter (fun x => ¬↑(degree G x) = 0) univ)) = 0
x✝ : V
⊢ Odd (degree G x✝) ↔ ¬↑(degree G x✝) = 0
exact ZMod.ne_zero_iff_odd.symm
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ v ∈ filter (fun x => ↑(degree G x) ≠ 0) univ → ↑(degree G v) = 1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
⊢ ∀ (x : V), x ∈ filter (fun x => ↑(degree G x) ≠ 0) univ → ↑(degree G x) = 1
intro v
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ ¬↑(degree G v) = 0 → ↑(degree G v) = 1
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ v ∈ filter (fun x => ↑(degree G x) ≠ 0) univ → ↑(degree G v) = 1
simp only [true_and_iff, mem_filter, mem_univ, Ne.def]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ True
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ ¬↑(degree G v) = 0 → ↑(degree G v) = 1
rw [ZMod.eq_zero_iff_even, ZMod.eq_one_iff_odd, Nat.odd_iff_not_even, imp_self]
no goals
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h✝ : ∑ x : V, ↑(degree G x) = 0
h : ∑ x in filter (fun x => ↑(degree G x) ≠ 0) univ, ↑(degree G x) = 0
v : V
⊢ True
trivial