[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
⊢ filter (fun d => d.fst = v) univ = image (dartOfNeighborSet G v) univ
[PROOFSTEP]
ext d
[GOAL]
case a
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ d ∈ filter (fun d => d.fst = v) univ ↔ d ∈ image (dartOfNeighborSet G v) univ
[PROOFSTEP]
simp only [mem_image, true_and_iff, mem_filter, SetCoe.exists, mem_univ, exists_prop_of_true]
[GOAL]
case a
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ d.fst = v ↔ ∃ x h, dartOfNeighborSet G v { val := x, property := h } = d
[PROOFSTEP]
constructor
[GOAL]
case a.mp
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ d.fst = v → ∃ x h, dartOfNeighborSet G v { val := x, property := h } = d
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mp
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ ∃ x h, dartOfNeighborSet G d.fst { val := x, property := h } = d
[PROOFSTEP]
exact ⟨_, d.is_adj, by ext <;> rfl⟩
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ dartOfNeighborSet G d.fst { val := d.snd, property := (_ : Adj G d.fst d.snd) } = d
[PROOFSTEP]
ext
[GOAL]
case h.h₁
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ (dartOfNeighborSet G d.fst { val := d.snd, property := (_ : Adj G d.fst d.snd) }).toProd.fst = d.fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
⊢ (dartOfNeighborSet G d.fst { val := d.snd, property := (_ : Adj G d.fst d.snd) }).toProd.snd = d.snd
[PROOFSTEP]
rfl
[GOAL]
case a.mpr
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
d : Dart G
⊢ (∃ x h, dartOfNeighborSet G v { val := x, property := h } = d) → d.fst = v
[PROOFSTEP]
rintro ⟨e, he, rfl⟩
[GOAL]
case a.mpr.intro.intro
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v e : V
he : e ∈ neighborSet G v
⊢ (dartOfNeighborSet G v { val := e, property := he }).toProd.fst = v
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
v : V
⊢ card (filter (fun d => d.fst = v) univ) = degree G v
[PROOFSTEP]
simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
  card_image_of_injective univ (G.dartOfNeighborSet_injective v)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
[PROOFSTEP]
haveI := Classical.decEq V
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ Fintype.card (Dart G) = ∑ v : V, degree G v
[PROOFSTEP]
simp only [← card_univ, ← dart_fst_fiber_card_eq_degree]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ card univ = ∑ x : V, card (filter (fun d => d.fst = x) univ)
[PROOFSTEP]
exact card_eq_sum_card_fiberwise (by simp)
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
this : DecidableEq V
⊢ ∀ (x : Dart G), x ∈ univ → x.fst ∈ univ
[PROOFSTEP]
simp
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d d' : Dart G
⊢ d' ∈ filter (fun d' => edge d' = edge d) univ ↔ d' ∈ {d, symm d}
[PROOFSTEP]
simpa using dart_edge_eq_iff d' d
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = e) univ) = 2
[PROOFSTEP]
refine' Sym2.ind (fun v w h => _) e h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
[PROOFSTEP]
let d : G.Dart := ⟨(v, w), h⟩
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ card (filter (fun d => Dart.edge d = Quotient.mk (Sym2.Rel.setoid V) (v, w)) univ) = 2
[PROOFSTEP]
convert congr_arg card d.edge_fiber
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ 2 = card {d, Dart.symm d}
[PROOFSTEP]
rw [card_insert_of_not_mem, card_singleton]
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d ∈ {Dart.symm d}
[PROOFSTEP]
rw [mem_singleton]
[GOAL]
case h.e'_3
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h✝ : e ∈ edgeSet G
v w : V
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ edgeSet G
d : Dart G := { toProd := (v, w), is_adj := h }
⊢ ¬d = Dart.symm d
[PROOFSTEP]
exact d.symm_ne.symm
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ Fintype.card (Dart G) = 2 * card (edgeFinset G)
[PROOFSTEP]
rw [← card_univ]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ card univ = 2 * card (edgeFinset G)
[PROOFSTEP]
rw [@card_eq_sum_card_fiberwise _ _ _ Dart.edge _ G.edgeFinset fun d _h => by rw [mem_edgeFinset]; apply Dart.edge_mem]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
_h : d ∈ univ
⊢ Dart.edge d ∈ edgeFinset G
[PROOFSTEP]
rw [mem_edgeFinset]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
d : Dart G
_h : d ∈ univ
⊢ Dart.edge d ∈ edgeSet G
[PROOFSTEP]
apply Dart.edge_mem
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ ∑ a in edgeFinset G, card (filter (fun x => Dart.edge x = a) univ) = 2 * card (edgeFinset G)
[PROOFSTEP]
rw [← mul_comm, sum_const_nat]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
⊢ ∀ (x : Sym2 V), x ∈ edgeFinset G → card (filter (fun x_1 => Dart.edge x_1 = x) univ) = 2
[PROOFSTEP]
intro e h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeFinset G
⊢ card (filter (fun x => Dart.edge x = e) univ) = 2
[PROOFSTEP]
apply G.dart_edge_fiber_card e
[GOAL]
V : Type u
G : SimpleGraph V
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype (Sym2 V)
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ edgeFinset G
⊢ e ∈ edgeSet G
[PROOFSTEP]
rwa [← mem_edgeFinset]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
classical
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
simp only [ZMod.nat_cast_self, zero_mul, Nat.cast_mul] at h 
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h 
rw [@sum_congr _ _ _ _ (fun v => (G.degree v : ZMod 2)) (fun _v => (1 : ZMod 2)) _ rfl] at h 
· simp only [filter_congr, mul_one, nsmul_eq_mul, sum_const, Ne.def] at h 
  rw [← ZMod.eq_zero_iff_even]
  convert h
  exact ZMod.ne_zero_iff_odd.symm
· intro v
  simp only [true_and_iff, mem_filter, mem_univ, Ne.def]
  rw [ZMod.eq_zero_iff_even, ZMod.eq_one_iff_odd, Nat.odd_iff_not_even, imp_self]
  trivial
[GOAL]
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (card (filter (fun v => Odd (degree G v)) univ))
[PROOFSTEP]
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
[GOAL]
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))
[PROOFSTEP]
simp only [ZMod.nat_cast_self, zero_mul, Nat.cast_mul] at h 
[GOAL]
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))
[PROOFSTEP]
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h 
[GOAL]
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))
[PROOFSTEP]
rw [@sum_congr _ _ _ _ (fun v => (G.degree v : ZMod 2)) (fun _v => (1 : ZMod 2)) _ rfl] at h 
[GOAL]
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))
[PROOFSTEP]
simp only [filter_congr, mul_one, nsmul_eq_mul, sum_const, Ne.def] at h 
[GOAL]
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))
[PROOFSTEP]
rw [← ZMod.eq_zero_iff_even]
[GOAL]
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
[PROOFSTEP]
convert h
[GOAL]
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
[PROOFSTEP]
exact ZMod.ne_zero_iff_odd.symm
[GOAL]
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
[PROOFSTEP]
intro v
[GOAL]
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
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ, Ne.def]
[GOAL]
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
[PROOFSTEP]
rw [ZMod.eq_zero_iff_even, ZMod.eq_one_iff_odd, Nat.odd_iff_not_even, imp_self]
[GOAL]
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
[PROOFSTEP]
trivial
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
have hk : 0 < k :=
  by
  have hh : (filter (fun v : V => Odd (G.degree v)) univ).Nonempty :=
    by
    use v
    simp only [true_and_iff, mem_filter, mem_univ]
    exact h
  rwa [← card_pos, hg, ← two_mul, zero_lt_mul_left] at hh 
  exact zero_lt_two
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ 0 < k
[PROOFSTEP]
have hh : (filter (fun v : V => Odd (G.degree v)) univ).Nonempty :=
  by
  use v
  simp only [true_and_iff, mem_filter, mem_univ]
  exact h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ Finset.Nonempty (filter (fun v => Odd (degree G v)) univ)
[PROOFSTEP]
use v
[GOAL]
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ v ∈ filter (fun v => Odd (degree G v)) univ
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ]
[GOAL]
case h
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
⊢ Odd (degree G v)
[PROOFSTEP]
exact h
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hh : Finset.Nonempty (filter (fun v => Odd (degree G v)) univ)
⊢ 0 < k
[PROOFSTEP]
rwa [← card_pos, hg, ← two_mul, zero_lt_mul_left] at hh 
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hh : 0 < 2 * k
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v :=
  by
  ext w
  rw [and_comm]
[GOAL]
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
⊢ (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
[PROOFSTEP]
ext w
[GOAL]
case h.a
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
w : V
⊢ w ≠ v ∧ Odd (degree G w) ↔ Odd (degree G w) ∧ w ≠ v
[PROOFSTEP]
rw [and_comm]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ Odd (card (filter (fun w => w ≠ v ∧ Odd (degree G w)) univ))
[PROOFSTEP]
simp only [hc, filter_congr]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ Odd (card (filter (fun w => Odd (degree G w) ∧ w ≠ v) univ))
[PROOFSTEP]
rw [← filter_filter, filter_ne', card_erase_of_mem]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ Odd (card (filter (fun w => Odd (degree G w)) univ) - 1)
[PROOFSTEP]
refine' ⟨k - 1, tsub_eq_of_eq_add <| hg.trans _⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ k + k = 2 * (k - 1) + 1 + 1
[PROOFSTEP]
rw [add_assoc, one_add_one_eq_two, ← Nat.mul_succ, ← two_mul]
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ 2 * k = 2 * Nat.succ (k - 1)
[PROOFSTEP]
congr
[GOAL]
case intro.e_a
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ k = Nat.succ (k - 1)
[PROOFSTEP]
exact (tsub_add_cancel_of_le <| Nat.succ_le_iff.2 hk).symm
[GOAL]
case intro
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (degree G v)
k : ℕ
hg : card (filter (fun v => Odd (degree G v)) univ) = k + k
hk : 0 < k
hc : (fun w => w ≠ v ∧ Odd (degree G w)) = fun w => Odd (degree G w) ∧ w ≠ v
⊢ v ∈ filter (fun w => Odd (degree G w)) univ
[PROOFSTEP]
simpa only [true_and_iff, mem_filter, mem_univ]
[GOAL]
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)
[PROOFSTEP]
haveI := Classical.decEq V
[GOAL]
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)
[PROOFSTEP]
rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩
[GOAL]
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)
[PROOFSTEP]
have hg' : (filter (fun w : V => w ≠ v ∧ Odd (G.degree w)) univ).card > 0 :=
  by
  rw [hg]
  apply Nat.succ_pos
[GOAL]
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
[PROOFSTEP]
rw [hg]
[GOAL]
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
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
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)
[PROOFSTEP]
rcases card_pos.mp hg' with ⟨w, hw⟩
[GOAL]
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)
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ, Ne.def] at hw 
[GOAL]
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)
[PROOFSTEP]
exact ⟨w, hw⟩
