Theorem: SimpleGraph.exists_even_degree (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean)

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : filter (fun x => Odd (degree G x)) univ ≠ univ
⊢ ∃ v, Even (degree G v)
Tactic:
rw [Ne.def, filter_eq_self] at this
State after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : ¬∀ x ∈ univ, Odd (degree G x)
⊢ ∃ v, Even (degree G v)

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
this : ¬∀ x ∈ univ, Odd (degree G x)
⊢ ∃ v, Even (degree G v)
Tactic:
simpa using this
State after:
no goals

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ filter (fun x => Odd (degree G x)) univ ≠ univ
Tactic:
rw [←card_lt_iff_ne_univ, (card_le_univ _).lt_iff_ne]
State after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ Finset.card (filter (fun x => Odd (degree G x)) univ) ≠ Fintype.card V

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
⊢ Finset.card (filter (fun x => Odd (degree G x)) univ) ≠ Fintype.card V
Tactic:
intro h
State after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
⊢ False

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
⊢ False
Tactic:
have h' := even_card_odd_degree_vertices G
State after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : Even (Finset.card (filter (fun v => Odd (degree G v)) univ))
⊢ False

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : Even (Finset.card (filter (fun v => Odd (degree G v)) univ))
⊢ False
Tactic:
rw [h, Nat.even_iff_not_odd] at h'
State after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : ¬Odd (Fintype.card V)
⊢ False

State before:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
hV : Odd (Fintype.card V)
h : Finset.card (filter (fun x => Odd (degree G x)) univ) = Fintype.card V
h' : ¬Odd (Fintype.card V)
⊢ False
Tactic:
exact h' hV
State after:
no goals