FormalConjectures.OEIS.«117531»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Number of primes in $n$-th row of triangle $k^2 - k + p_n$

$a(n)$ is the number of primes in the $n$-th row of the triangle $T(n, k) = k^2 - k + p_n$ for $1 \le k \le n$, where $p_n$ is the $n$-th prime ($p_1=2, p_2=3, \dots$).

References:

A117531

namespace OeisA117531

Number of primes in the $n$-th row of $T(n, k) = k^2 - k + p_n$ for $1 \le k \le n$.

noncomputable def a (n : ℕ) : ℕ :=
  let pn : ℕ := Nat.nth Nat.Prime (n - 1)
  Finset.card ((Finset.Icc 1 n).filter fun k => (k ^ 2 - k + pn).Prime)

Value of the sequence a at 0.

@[category test, AMS 11]
theorem a_0 : a 0 = 0 := by⊢ a 0 = 0 rflAll goals completed! 🐙

Value of the sequence a at 1.


@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1
  unfold a⊢ (let pn := Nat.nth Nat.Prime (1 - 1);
  {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  1
  have h_zero : Nat.nth Nat.Prime (1 - 1) = 2 := Nat.nth_prime_zero_eq_twoh_zero:Nat.nth Nat.Prime (1 - 1) = 2⊢ (let pn := Nat.nth Nat.Prime (1 - 1);
  {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  1
  dsimp onlyh_zero:Nat.nth Nat.Prime (1 - 1) = 2⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + Nat.nth Nat.Prime (1 - 1))}.card = 1
  rw [h_zeroh_zero:Nat.nth Nat.Prime (1 - 1) = 2⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + 2)}.card = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + 2)}.card = 1]h_zero:Nat.nth Nat.Prime (1 - 1) = 2⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + 2)}.card = 1
  have h1 : Finset.Icc 1 1 = {1} := by⊢ a 1 = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + 2)}.card = 1 decideh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + 2)}.card = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ {k ∈ Finset.Icc 1 1 | Nat.Prime (k ^ 2 - k + 2)}.card = 1
  rw [h1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1]h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
  have : (Finset.filter (fun k : ℕ => (k ^ 2 - k + 2).Prime) {1}) = {1} := by⊢ a 1 = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
    ext xh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕ⊢ x ∈ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} ↔ x ∈ {1}h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
    simp only [Finset.mem_filter, Finset.mem_singleton]h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕ⊢ x = 1 ∧ Nat.Prime (x ^ 2 - x + 2) ↔ x = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
    constructormph_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕ⊢ x = 1 ∧ Nat.Prime (x ^ 2 - x + 2) → x = 1mprh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕ⊢ x = 1 → x = 1 ∧ Nat.Prime (x ^ 2 - x + 2)h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
    ·mph_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕ⊢ x = 1 ∧ Nat.Prime (x ^ 2 - x + 2) → x = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1 intro hmph_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕh:x = 1 ∧ Nat.Prime (x ^ 2 - x + 2)⊢ x = 1h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1; exact h.1All goals completed! 🐙h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
    ·mprh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}x:ℕ⊢ x = 1 → x = 1 ∧ Nat.Prime (x ^ 2 - x + 2)h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1 rintro rflmprh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ 1 = 1 ∧ Nat.Prime (1 ^ 2 - 1 + 2)h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1; exact ⟨rfl, byh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}⊢ Nat.Prime (1 ^ 2 - 1 + 2)h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1 norm_numAll goals completed! 🐙h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1⟩h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)}.card = 1
  rw [this,h_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ {1}.card = 1All goals completed! 🐙 Finset.card_singletonh_zero:Nat.nth Nat.Prime (1 - 1) = 2h1:Finset.Icc 1 1 = {1}this:{k ∈ {1} | Nat.Prime (k ^ 2 - k + 2)} = {1}⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

Value of the sequence a at 2.


@[category test, AMS 11]
theorem a_2 : a 2 = 2 := by⊢ a 2 = 2
  unfold a⊢ (let pn := Nat.nth Nat.Prime (2 - 1);
  {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  2
  have h_one : Nat.nth Nat.Prime (2 - 1) = 3 := Nat.nth_prime_one_eq_threeh_one:Nat.nth Nat.Prime (2 - 1) = 3⊢ (let pn := Nat.nth Nat.Prime (2 - 1);
  {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  2
  dsimp onlyh_one:Nat.nth Nat.Prime (2 - 1) = 3⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + Nat.nth Nat.Prime (2 - 1))}.card = 2
  rw [h_oneh_one:Nat.nth Nat.Prime (2 - 1) = 3⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + 3)}.card = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + 3)}.card = 2]h_one:Nat.nth Nat.Prime (2 - 1) = 3⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + 3)}.card = 2
  have h2 : Finset.Icc 1 2 = {1, 2} := by⊢ a 2 = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + 3)}.card = 2 decideh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + 3)}.card = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ {k ∈ Finset.Icc 1 2 | Nat.Prime (k ^ 2 - k + 3)}.card = 2
  rw [h2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2]h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
  have : (Finset.filter (fun k : ℕ => (k ^ 2 - k + 3).Prime) {1, 2}) = {1, 2} := by⊢ a 2 = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
    ext xh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕ⊢ x ∈ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} ↔ x ∈ {1, 2}h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
    simp only [Finset.mem_filter, Finset.mem_insert, Finset.mem_singleton]h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕ⊢ (x = 1 ∨ x = 2) ∧ Nat.Prime (x ^ 2 - x + 3) ↔ x = 1 ∨ x = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
    constructormph_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕ⊢ (x = 1 ∨ x = 2) ∧ Nat.Prime (x ^ 2 - x + 3) → x = 1 ∨ x = 2mprh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕ⊢ x = 1 ∨ x = 2 → (x = 1 ∨ x = 2) ∧ Nat.Prime (x ^ 2 - x + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
    ·mph_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕ⊢ (x = 1 ∨ x = 2) ∧ Nat.Prime (x ^ 2 - x + 3) → x = 1 ∨ x = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2 intro hmph_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕh:(x = 1 ∨ x = 2) ∧ Nat.Prime (x ^ 2 - x + 3)⊢ x = 1 ∨ x = 2h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2; exact h.1All goals completed! 🐙h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
    ·mprh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}x:ℕ⊢ x = 1 ∨ x = 2 → (x = 1 ∨ x = 2) ∧ Nat.Prime (x ^ 2 - x + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2 rintro (rfl | rfl)mpr.inlh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ (1 = 1 ∨ 1 = 2) ∧ Nat.Prime (1 ^ 2 - 1 + 3)mpr.inrh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ (2 = 1 ∨ 2 = 2) ∧ Nat.Prime (2 ^ 2 - 2 + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
      ·mpr.inlh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ (1 = 1 ∨ 1 = 2) ∧ Nat.Prime (1 ^ 2 - 1 + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2 refine ⟨Or.inl rfl, byh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ Nat.Prime (1 ^ 2 - 1 + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2 norm_numAll goals completed! 🐙h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2⟩
      ·mpr.inrh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ (2 = 1 ∨ 2 = 2) ∧ Nat.Prime (2 ^ 2 - 2 + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2 refine ⟨Or.inr rfl, byh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}⊢ Nat.Prime (2 ^ 2 - 2 + 3)h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2 norm_numAll goals completed! 🐙h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2⟩h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)}.card = 2
  rw [this,h_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ {1, 2}.card = 2All goals completed! 🐙 Finset.card_pair (byh_one:Nat.nth Nat.Prime (2 - 1) = 3h2:Finset.Icc 1 2 = {1, 2}this:{k ∈ {1, 2} | Nat.Prime (k ^ 2 - k + 3)} = {1, 2}⊢ 1 ≠ 2All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙

Value of the sequence a at 3.


@[category test, AMS 11]
theorem a_3 : a 3 = 3 := by⊢ a 3 = 3
  unfold a⊢ (let pn := Nat.nth Nat.Prime (3 - 1);
  {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  3
  have h_two : Nat.nth Nat.Prime (3 - 1) = 5 := Nat.nth_prime_two_eq_fiveh_two:Nat.nth Nat.Prime (3 - 1) = 5⊢ (let pn := Nat.nth Nat.Prime (3 - 1);
  {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  3
  dsimp onlyh_two:Nat.nth Nat.Prime (3 - 1) = 5⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + Nat.nth Nat.Prime (3 - 1))}.card = 3
  rw [h_twoh_two:Nat.nth Nat.Prime (3 - 1) = 5⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + 5)}.card = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + 5)}.card = 3]h_two:Nat.nth Nat.Prime (3 - 1) = 5⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + 5)}.card = 3
  have h3 : Finset.Icc 1 3 = {1, 2, 3} := by⊢ a 3 = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + 5)}.card = 3 decideh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + 5)}.card = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ {k ∈ Finset.Icc 1 3 | Nat.Prime (k ^ 2 - k + 5)}.card = 3
  rw [h3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3]h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
  have : (Finset.filter (fun k : ℕ => (k ^ 2 - k + 5).Prime) {1, 2, 3}) = {1, 2, 3} := by⊢ a 3 = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
    ext xh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕ⊢ x ∈ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} ↔ x ∈ {1, 2, 3}h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
    simp only [Finset.mem_filter, Finset.mem_insert, Finset.mem_singleton]h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕ⊢ (x = 1 ∨ x = 2 ∨ x = 3) ∧ Nat.Prime (x ^ 2 - x + 5) ↔ x = 1 ∨ x = 2 ∨ x = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
    constructormph_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕ⊢ (x = 1 ∨ x = 2 ∨ x = 3) ∧ Nat.Prime (x ^ 2 - x + 5) → x = 1 ∨ x = 2 ∨ x = 3mprh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕ⊢ x = 1 ∨ x = 2 ∨ x = 3 → (x = 1 ∨ x = 2 ∨ x = 3) ∧ Nat.Prime (x ^ 2 - x + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
    ·mph_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕ⊢ (x = 1 ∨ x = 2 ∨ x = 3) ∧ Nat.Prime (x ^ 2 - x + 5) → x = 1 ∨ x = 2 ∨ x = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 intro hmph_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕh:(x = 1 ∨ x = 2 ∨ x = 3) ∧ Nat.Prime (x ^ 2 - x + 5)⊢ x = 1 ∨ x = 2 ∨ x = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3; exact h.1All goals completed! 🐙h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
    ·mprh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}x:ℕ⊢ x = 1 ∨ x = 2 ∨ x = 3 → (x = 1 ∨ x = 2 ∨ x = 3) ∧ Nat.Prime (x ^ 2 - x + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 rintro (rfl | rfl | rfl)mpr.inlh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ (1 = 1 ∨ 1 = 2 ∨ 1 = 3) ∧ Nat.Prime (1 ^ 2 - 1 + 5)mpr.inr.inlh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ (2 = 1 ∨ 2 = 2 ∨ 2 = 3) ∧ Nat.Prime (2 ^ 2 - 2 + 5)mpr.inr.inrh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ (3 = 1 ∨ 3 = 2 ∨ 3 = 3) ∧ Nat.Prime (3 ^ 2 - 3 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
      ·mpr.inlh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ (1 = 1 ∨ 1 = 2 ∨ 1 = 3) ∧ Nat.Prime (1 ^ 2 - 1 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 refine ⟨Or.inl rfl, byh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ Nat.Prime (1 ^ 2 - 1 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 norm_numAll goals completed! 🐙h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3⟩
      ·mpr.inr.inlh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ (2 = 1 ∨ 2 = 2 ∨ 2 = 3) ∧ Nat.Prime (2 ^ 2 - 2 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 refine ⟨Or.inr (Or.inl rfl), byh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ Nat.Prime (2 ^ 2 - 2 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 norm_numAll goals completed! 🐙h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3⟩
      ·mpr.inr.inrh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ (3 = 1 ∨ 3 = 2 ∨ 3 = 3) ∧ Nat.Prime (3 ^ 2 - 3 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 refine ⟨Or.inr (Or.inr rfl), byh_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}⊢ Nat.Prime (3 ^ 2 - 3 + 5)h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3 norm_numAll goals completed! 🐙h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3⟩h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)}.card = 3
  rw [thish_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {1, 2, 3}.card = 3h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {1, 2, 3}.card = 3]h_two:Nat.nth Nat.Prime (3 - 1) = 5h3:Finset.Icc 1 3 = {1, 2, 3}this:{k ∈ {1, 2, 3} | Nat.Prime (k ^ 2 - k + 5)} = {1, 2, 3}⊢ {1, 2, 3}.card = 3
  decideAll goals completed! 🐙

Value of the sequence a at 4.


@[category test, AMS 11]
theorem a_4 : a 4 = 3 := by⊢ a 4 = 3
  unfold a⊢ (let pn := Nat.nth Nat.Prime (4 - 1);
  {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  3
  have h_three : Nat.nth Nat.Prime (4 - 1) = 7 := Nat.nth_prime_three_eq_sevenh_three:Nat.nth Nat.Prime (4 - 1) = 7⊢ (let pn := Nat.nth Nat.Prime (4 - 1);
  {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + pn)}.card) =
  3
  dsimp onlyh_three:Nat.nth Nat.Prime (4 - 1) = 7⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + Nat.nth Nat.Prime (4 - 1))}.card = 3
  rw [h_threeh_three:Nat.nth Nat.Prime (4 - 1) = 7⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + 7)}.card = 3h_three:Nat.nth Nat.Prime (4 - 1) = 7⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + 7)}.card = 3]h_three:Nat.nth Nat.Prime (4 - 1) = 7⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + 7)}.card = 3
  have h4 : Finset.Icc 1 4 = {1, 2, 3, 4} := by⊢ a 4 = 3h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + 7)}.card = 3 decideh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + 7)}.card = 3h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ {k ∈ Finset.Icc 1 4 | Nat.Prime (k ^ 2 - k + 7)}.card = 3
  rw [h4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3]h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
  have : (Finset.filter (fun k : ℕ => (k ^ 2 - k + 7).Prime) {1, 2, 3, 4}) = {1, 3, 4} := by⊢ a 4 = 3h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
    ext xh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}x:ℕ⊢ x ∈ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} ↔ x ∈ {1, 3, 4}h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
    simp only [Finset.mem_filter, Finset.mem_insert, Finset.mem_singleton]h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}x:ℕ⊢ (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4) ∧ Nat.Prime (x ^ 2 - x + 7) ↔ x = 1 ∨ x = 3 ∨ x = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
    constructormph_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}x:ℕ⊢ (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4) ∧ Nat.Prime (x ^ 2 - x + 7) → x = 1 ∨ x = 3 ∨ x = 4mprh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}x:ℕ⊢ x = 1 ∨ x = 3 ∨ x = 4 → (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4) ∧ Nat.Prime (x ^ 2 - x + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
    ·mph_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}x:ℕ⊢ (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4) ∧ Nat.Prime (x ^ 2 - x + 7) → x = 1 ∨ x = 3 ∨ x = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 rintro ⟨(rfl | rfl | rfl | rfl), hp⟩mp.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (1 ^ 2 - 1 + 7)⊢ 1 = 1 ∨ 1 = 3 ∨ 1 = 4mp.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (2 ^ 2 - 2 + 7)⊢ 2 = 1 ∨ 2 = 3 ∨ 2 = 4mp.inr.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (3 ^ 2 - 3 + 7)⊢ 3 = 1 ∨ 3 = 3 ∨ 3 = 4mp.inr.inr.inrh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (4 ^ 2 - 4 + 7)⊢ 4 = 1 ∨ 4 = 3 ∨ 4 = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
      ·mp.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (1 ^ 2 - 1 + 7)⊢ 1 = 1 ∨ 1 = 3 ∨ 1 = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 exact Or.inl rflAll goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
      ·mp.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (2 ^ 2 - 2 + 7)⊢ 2 = 1 ∨ 2 = 3 ∨ 2 = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 exfalsomp.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (2 ^ 2 - 2 + 7)⊢ Falseh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3; revert hpmp.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ Nat.Prime (2 ^ 2 - 2 + 7) → Falseh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3; norm_numAll goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
      ·mp.inr.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (3 ^ 2 - 3 + 7)⊢ 3 = 1 ∨ 3 = 3 ∨ 3 = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 exact Or.inr (Or.inl rfl)All goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
      ·mp.inr.inr.inrh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}hp:Nat.Prime (4 ^ 2 - 4 + 7)⊢ 4 = 1 ∨ 4 = 3 ∨ 4 = 4h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 exact Or.inr (Or.inr rfl)All goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
    ·mprh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}x:ℕ⊢ x = 1 ∨ x = 3 ∨ x = 4 → (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4) ∧ Nat.Prime (x ^ 2 - x + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 rintro (rfl | rfl | rfl)mpr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ (1 = 1 ∨ 1 = 2 ∨ 1 = 3 ∨ 1 = 4) ∧ Nat.Prime (1 ^ 2 - 1 + 7)mpr.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ (3 = 1 ∨ 3 = 2 ∨ 3 = 3 ∨ 3 = 4) ∧ Nat.Prime (3 ^ 2 - 3 + 7)mpr.inr.inrh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ (4 = 1 ∨ 4 = 2 ∨ 4 = 3 ∨ 4 = 4) ∧ Nat.Prime (4 ^ 2 - 4 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
      ·mpr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ (1 = 1 ∨ 1 = 2 ∨ 1 = 3 ∨ 1 = 4) ∧ Nat.Prime (1 ^ 2 - 1 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 refine ⟨Or.inl rfl, byh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ Nat.Prime (1 ^ 2 - 1 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 norm_numAll goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3⟩
      ·mpr.inr.inlh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ (3 = 1 ∨ 3 = 2 ∨ 3 = 3 ∨ 3 = 4) ∧ Nat.Prime (3 ^ 2 - 3 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 refine ⟨Or.inr (Or.inr (Or.inl rfl)), byh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ Nat.Prime (3 ^ 2 - 3 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 norm_numAll goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3⟩
      ·mpr.inr.inrh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ (4 = 1 ∨ 4 = 2 ∨ 4 = 3 ∨ 4 = 4) ∧ Nat.Prime (4 ^ 2 - 4 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 refine ⟨Or.inr (Or.inr (Or.inr rfl)), byh_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}⊢ Nat.Prime (4 ^ 2 - 4 + 7)h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3 norm_numAll goals completed! 🐙h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3⟩h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)}.card = 3
  rw [thish_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {1, 3, 4}.card = 3h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {1, 3, 4}.card = 3]h_three:Nat.nth Nat.Prime (4 - 1) = 7h4:Finset.Icc 1 4 = {1, 2, 3, 4}this:{k ∈ {1, 2, 3, 4} | Nat.Prime (k ^ 2 - k + 7)} = {1, 3, 4}⊢ {1, 3, 4}.card = 3
  decideAll goals completed! 🐙

Conjecture: $a(n) < n$ for $n > 13$.

@[category research open, AMS 11]
theorem conjecture (n : ℕ) (h : n > 13) : a n < n := byn:ℕh:n > 13⊢ a n < n
  sorryAll goals completed! 🐙

end OeisA117531