convert_to _ = Fintype.card V - 1
case h.e'_3
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 : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ (univ.erase v).card = 2
case h.e'_3
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 : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ 2 = Fintype.card V - 1

case h.e'_3.convert_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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : ∀ (v : V), (G.neighborFinset v).card = 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
x : V
hx_left : ¬v = x
hx_right : ¬G.Adj v x
this : (G.neighborFinset v).card = 2
⊢ (univ.erase v).card = Fintype.card V - 1