have v := Classical.arbitrary V
case «2»
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 2
hk : 2 ≤ 2
eq₁ : n = 3
⊢ False
case «2»
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
⊢ False