Theorem: chapter44.friendship_theorem (FormalBook/Chapter_44.lean)

State before:
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
⊢ ∃ v, ∀ (w : V), v ≠ w → G.Adj v w
Tactic:
by_contra no_politician
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have lemma₁ :  ∃ k : ℕ, G.IsRegularOfDegree k := by
  sorry
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have ⟨k, hregular⟩ := lemma₁
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
let n := Fintype.card V
State after:
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
⊢ False

State before:
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
⊢ False
Tactic:
have eq₁ : n = k^2 - k  + 1 := by
  have : k + (n - 1) = k * k := by
    sorry
  rw [pow_two, this.symm]
  simp only [add_tsub_cancel_left]
  exact Nat.eq_add_of_sub_eq Fintype.card_pos rfl
State after:
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
⊢ False

State before:
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
this : 2 < k
⊢ False
Tactic:
let A := G.adjMatrix R
State after:
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
this : 2 < k
A : Matrix V V R := adjMatrix R G
⊢ False

State before:
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
this : 2 < k
A : Matrix V V R := adjMatrix R G
⊢ False
Tactic:
have : (A ^ 2) = (k - 1) • (1 : Matrix V V R) + of (fun _ _ => 1) := by sorry
State after:
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
this✝ : 2 < k
A : Matrix V V R := adjMatrix R G
this : A ^ 2 = (k - 1) • 1 + of fun x x => 1
⊢ False

State before:
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
this✝ : 2 < k
A : Matrix V V R := adjMatrix R G
this : A ^ 2 = (k - 1) • 1 + of fun x x => 1
⊢ False
Tactic:
sorry
State after:
no goals

State before:
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
⊢ ∃ k, G.IsRegularOfDegree k
Tactic:
sorry
State after:
no goals

State before:
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
⊢ n = k ^ 2 - k + 1
Tactic:
have : k + (n - 1) = k * k := by
  sorry
State after:
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
this : k + (n - 1) = k * k
⊢ n = k ^ 2 - k + 1

State before:
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
this : k + (n - 1) = k * k
⊢ n = k ^ 2 - k + 1
Tactic:
rw [pow_two, this.symm]
State after:
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
this : k + (n - 1) = k * k
⊢ n = k + (n - 1) - k + 1

State before:
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
this : k + (n - 1) = k * k
⊢ n = k + (n - 1) - k + 1
Tactic:
simp only [add_tsub_cancel_left]
State after:
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
this : k + (n - 1) = k * k
⊢ n = n - 1 + 1

State before:
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
this : k + (n - 1) = k * k
⊢ n = n - 1 + 1
Tactic:
exact Nat.eq_add_of_sub_eq Fintype.card_pos rfl
State after:
no goals

State before:
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
⊢ k + (n - 1) = k * k
Tactic:
sorry
State after:
no goals

State before:
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
⊢ 2 < k
Tactic:
by_contra hk
State after:
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 : ¬2 < k
⊢ False

State before:
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 : ¬2 < k
⊢ False
Tactic:
rw [not_lt] at hk
State after:
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

State before:
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
Tactic:
interval_cases k
State after:
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

State before:
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
Tactic:
simp at eq₁
State after:
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 = 3
hk : 2 ≤ 2
⊢ False

State before:
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 = 3
hk : 2 ≤ 2
⊢ False
Tactic:
have v := Classical.arbitrary V
State after:
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 = 3
hk : 2 ≤ 2
v : V
⊢ False

State before:
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 = 3
hk : 2 ≤ 2
v : V
⊢ False
Tactic:
simp at no_politician
State after:
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
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
⊢ False

State before:
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
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
⊢ False
Tactic:
have ⟨x, hx⟩ := no_politician v
State after:
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
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
⊢ False

State before:
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
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
⊢ False
Tactic:
have := hx.left
State after:
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
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
⊢ False

State before:
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
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
⊢ False
Tactic:
have : 1 < Fintype.card V := by
  refine' Fintype.one_lt_card_iff.mpr _
  use v
  use x
State after:
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
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
this : 1 < Fintype.card V
⊢ False

State before:
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
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
this : 1 < Fintype.card V
⊢ False
Tactic:
rw [(show Fintype.card V = n by rfl), eq₁] at this
State after:
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
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
this : 1 < 3
⊢ False

State before:
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
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
this : 1 < 3
⊢ False
Tactic:
tauto
State after:
no goals

State before:
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
⊢ 1 < Fintype.card V
Tactic:
refine' Fintype.one_lt_card_iff.mpr _
State after:
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

State before:
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
Tactic:
use v
State after:
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

State before:
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
Tactic:
use x
State after:
no goals

State before:
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
this : 1 < Fintype.card V
⊢ Fintype.card V = n
Tactic:
rfl
State after:
no goals

State before:
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
Tactic:
norm_num at eq₁
State after:
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

State before:
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
Tactic:
have v := Classical.arbitrary V
State after:
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

State before:
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
Tactic:
simp only [ne_eq, not_exists, not_forall, exists_prop] at no_politician
State after:
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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
⊢ False

State before:
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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 2
hk : 2 ≤ 2
eq₁ : n = 3
v : V
no_politician : ∀ (x : V), ∃ x_1, ¬x = x_1 ∧ ¬G.Adj x x_1
⊢ False
Tactic:
have ⟨x, ⟨hx_left, hx_right⟩⟩ := no_politician v
State after:
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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 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
⊢ False

State before:
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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 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
⊢ False
Tactic:
refine' hx_right _
State after:
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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 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
⊢ G.Adj v x

State before:
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
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
n : ℕ := Fintype.card V
hregular : G.IsRegularOfDegree 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
⊢ G.Adj v x
Tactic:
simp only [IsRegularOfDegree, degree] at hregular
State after:
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
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
⊢ G.Adj v x

State before:
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
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
⊢ G.Adj v x
Tactic:
rw [← mem_neighborFinset]
State after:
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
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
⊢ x ∈ G.neighborFinset v

State before:
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
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
⊢ x ∈ G.neighborFinset v
Tactic:
have := hregular v
State after:
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
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
⊢ x ∈ G.neighborFinset v

State before:
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
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
this : G.neighborFinset v = univ.erase v
⊢ x ∈ G.neighborFinset v
Tactic:
rw [this]
State after:
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
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
this : G.neighborFinset v = univ.erase v
⊢ x ∈ univ.erase v

State before:
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
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
this : G.neighborFinset v = univ.erase v
⊢ x ∈ univ.erase v
Tactic:
simp only [Finset.mem_erase, Finset.mem_univ]
State after:
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
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
this : G.neighborFinset v = univ.erase v
⊢ x ≠ v ∧ True

State before:
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
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
this : G.neighborFinset v = univ.erase v
⊢ x ≠ v ∧ True
Tactic:
tauto
State after:
no goals

State before:
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
⊢ G.neighborFinset v = univ.erase v
Tactic:
apply eq_of_subset_of_card_le
State after:
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 : ∀ (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
⊢ G.neighborFinset v ⊆ univ.erase v

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 : ∀ (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 ≤ (G.neighborFinset v).card

State before:
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 : ∀ (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 ≤ (G.neighborFinset v).card
Tactic:
convert_to 2 ≤ _
State after:
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₂.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
⊢ 2 ≤ (G.neighborFinset v).card

State before:
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 : ∀ (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
⊢ G.neighborFinset v ⊆ univ.erase v
Tactic:
rw [Finset.subset_iff]
State after:
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 : ∀ (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
⊢ ∀ ⦃x : V⦄, x ∈ G.neighborFinset v → x ∈ univ.erase v

State before:
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 : ∀ (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
⊢ ∀ ⦃x : V⦄, x ∈ G.neighborFinset v → x ∈ univ.erase v
Tactic:
intro x
State after:
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 : ∀ (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
x : V
⊢ x ∈ G.neighborFinset v → x ∈ univ.erase v

State before:
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 : ∀ (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
x : V
⊢ x ∈ G.neighborFinset v → x ∈ univ.erase v
Tactic:
rw [mem_neighborFinset, Finset.mem_erase]
State after:
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 : ∀ (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
x : V
⊢ G.Adj v x → x ≠ v ∧ x ∈ univ

State before:
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 : ∀ (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
x : V
⊢ G.Adj v x → x ≠ v ∧ x ∈ univ
Tactic:
exact fun h => ⟨(G.ne_of_adj h).symm, Finset.mem_univ _⟩
State after:
no goals

State before:
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
Tactic:
convert_to _ = Fintype.card V - 1
State after:
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

State before:
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
Tactic:
rw [(show Fintype.card V = n by rfl), eq₁]
State after:
no goals

State before:
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
⊢ Fintype.card V = n
Tactic:
rfl
State after:
no goals

State before:
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
Tactic:
exact Finset.card_erase_of_mem (Finset.mem_univ _)
State after:
no goals

State before:
case h₂.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
⊢ 2 ≤ (G.neighborFinset v).card
Tactic:
rw [hregular]
State after:
no goals

State before:
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
this : 2 < k
A : Matrix V V R := adjMatrix R G
⊢ A ^ 2 = (k - 1) • 1 + of fun x x => 1
Tactic:
sorry
State after:
no goals