interval_cases k
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 : ℕ
hregular : G.IsRegularOfDegree k
n : ℕ := Fintype.card V
eq₁ : n = k ^ 2 - k + 1
hk : k ≤ 2
⊢ False
case «0»
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 0
eq₁ : n = 0 ^ 2 - 0 + 1
hk : 0 ≤ 2
⊢ False

case «1»
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 1
eq₁ : n = 1 ^ 2 - 1 + 1
hk : 1 ≤ 2
⊢ 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
eq₁ : n = 2 ^ 2 - 2 + 1
hk : 2 ≤ 2
⊢ False