internlm/Lean-Github huggingface dataset:
Theorem: chapter02.centralBinom_le_of_no_bertrand_prime
Proof state before:
case h₂.refine'_1.intro
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ f p ≤ p
Tactic:
refine' (pow_le_pow_right (Finset.mem_filter.1 h1).2.one_lt.le _).trans (pow_one p).le
Proof state after:
case h₂.refine'_1.intro
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ n.centralBinom.factorization p ≤ 1
Theorem: chapter02.centralBinom_le_of_no_bertrand_prime
Proof state before:
case h₂.refine'_1.intro
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ n.centralBinom.factorization p ≤ 1
Tactic:
exact Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
by_contra no_prime
Proof state after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ False
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ False
Tactic:
have H1 : n * (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := bertrand_main_inequality n_big
Proof state after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ False
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ False
Tactic:
have H2 : 4 ^ n < n * n.centralBinom :=
  Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_big)
Proof state after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False
Tactic:
have H3 : n.centralBinom ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ (2 * n / 3) :=
  centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_big) no_prime
Proof state after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False
Tactic:
rw [mul_assoc] at H1
Proof state after:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False
Tactic:
exact not_le.2 H2 ((mul_le_mul_left' H3 n).trans H1)
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ 4 ≤ 512
Tactic:
norm_num1
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul_eventually
Proof state before:
n : ℕ
n_big : 512 ≤ n
no_prime : ¬∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ 2 < 512
Tactic:
norm_num1
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul_succ
Proof state before:
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
by_cases h : p ≤ 2 * n
Proof state after:
case pos
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case neg
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Theorem: chapter02.exists_prime_lt_and_le_two_mul_succ
Proof state before:
case pos
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact ⟨p, prime_p, hn, h⟩
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul_succ
Proof state before:
case neg
n q p : ℕ
prime_p : p.Prime
covering : p ≤ 2 * q
H : n < q → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
hn : n < p
h : ¬p ≤ 2 * n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact H (lt_of_mul_lt_mul_left' (lt_of_lt_of_le (not_le.1 h) covering))
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
n : ℕ
hn0 : n ≠ 0
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
cases' lt_or_le 511 n with h h
Proof state after:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
swap
Proof state after:
case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n

case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inr
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
replace h : n < 521 := h.trans_lt (by norm_num1)
Proof state after:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inr
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
revert h
Proof state after:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
open Lean Elab Tactic in
run_tac do
  for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
    let i : Term := quote i
    evalTactic <| ←
      `(tactic| refine' exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) _)
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ 511 < 521
Tactic:
norm_num1
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 521 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
run_tac do
  for i in [317, 163, 83, 43, 23, 13, 7, 5, 3, 2] do
    let i : Term := quote i
    evalTactic <| ←
      `(tactic| refine' exists_prime_lt_and_le_two_mul_succ $i (by norm_num1) (by norm_num1) _)
Proof state after:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inr
n : ℕ
hn0 : n ≠ 0
⊢ n < 2 → ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact fun h2 => ⟨2, prime_two, h2, Nat.mul_le_mul_left 2 (Nat.pos_of_ne_zero hn0)⟩
Proof state after:
no goals
Theorem: chapter02.exists_prime_lt_and_le_two_mul
Proof state before:
case inl
n : ℕ
hn0 : n ≠ 0
h : 511 < n
⊢ ∃ p, p.Prime ∧ n < p ∧ p ≤ 2 * n
Tactic:
exact exists_prime_lt_and_le_two_mul_eventually n h
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
⊢ ∃ v, ∀ (w : V), v ≠ w → G.Adj v w
Tactic:
by_contra no_politician
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
⊢ False
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
⊢ False
Tactic:
have lemma₁ :  ∃ k : ℕ, G.IsRegularOfDegree k := by
  sorry
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
⊢ False
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
⊢ False
Tactic:
have ⟨k, hregular⟩ := lemma₁
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
lemma₁ : ∃ k, G.IsRegularOfDegree k
k : ℕ
hregular : G.IsRegularOfDegree k
⊢ False
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
no_politician : ¬∃ v, ∀ (w : V), v ≠ w → G.Adj v w
⊢ ∃ k, G.IsRegularOfDegree k
Tactic:
sorry
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
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
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
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
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
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]
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
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
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
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]
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
Proof 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
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:
simp 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
eq₁ : n = 3
hk : 2 ≤ 2
⊢ 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
eq₁ : n = 3
hk : 2 ≤ 2
⊢ 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
eq₁ : n = 3
hk : 2 ≤ 2
v : V
⊢ False