internlm/Lean-Github huggingface dataset:
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof 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 _
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof 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
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof 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₁
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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 _
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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]
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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]
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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]
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof state after:
no goals
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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 ≤ _
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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]
Proof 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
Theorem: chapter44.friendship_theorem
Proof 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
Proof 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