use v
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 2
eq₁ : n = 3
hk : 2 ≤ 2
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx : ¬v = x ∧ ¬G.Adj v x
this : ¬v = x
⊢ ∃ a b, a ≠ b
case h
V : Type u
R : Type v
inst✝² : Semiring R
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : Nonempty V
h : ∀ ⦃v w : V⦄, v ≠ w → Fintype.card ↑(G.commonNeighbors v w) = 1
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 2
eq₁ : n = 3
hk : 2 ≤ 2
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx : ¬v = x ∧ ¬G.Adj v x
this : ¬v = x
⊢ ∃ b, v ≠ b