FormalConjectures.OEIS.«110835»

/-
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

Smallest $m > 0$ such that there are no primes between $nm$ and $n(m+1)$ inclusive.

Sierpinski's conjecture (1958) is precisely that a(n) >= n for all n.

References:

A110835

namespace OeisA110835open Nat Set

The primary defining sequence a. $a(n)$ is the smallest $m > 0$ such that there are no primes between $n \cdot m$ and $n \cdot (m+1)$ inclusive.

noncomputable def a (n : ℕ) : ℕ :=
  let IsPrimeFreeInterval (m : ℕ) : Prop :=
    ∀ p : ℕ, p.Prime → ¬ (n * m ≤ p ∧ p ≤ n * (m + 1))
  let s : Set ℕ := {m : ℕ | m > 0 ∧ IsPrimeFreeInterval m}
  sInf s

Term theorems verifying the first few values of the sequence against the official OEIS b-file


@[category test, AMS 11]
theorem a_1 : a 1 = 8 := by⊢ a 1 = 8
  dsimp [a]⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
  have hleast : IsLeast {m : ℕ | m > 0 ∧ ∀ p : ℕ, p.Prime → ¬ (1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8 := by⊢ a 1 = 8hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
    constructorleft⊢ 8 ∈ {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))}right⊢ 8 ∈ lowerBounds {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
    ·left⊢ 8 ∈ {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 simp only [mem_ofPred_eq, one_mul]left⊢ 8 > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(8 ≤ p ∧ p ≤ 8 + 1)hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      refine ⟨by⊢ 8 > 0hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8, ?_⟩
      intro p hp ⟨hge, hle⟩leftp:ℕhp:Nat.Prime phge:8 ≤ phle:p ≤ 8 + 1⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      interval_cases pleft.«8»p:ℕhp:Nat.Prime 8hge:8 ≤ 8hle:8 ≤ 8 + 1⊢ Falseleft.«9»p:ℕhp:Nat.Prime 9hge:8 ≤ 9hle:9 ≤ 8 + 1⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 <;>left.«8»p:ℕhp:Nat.Prime 8hge:8 ≤ 8hle:8 ≤ 8 + 1⊢ Falseleft.«9»p:ℕhp:Nat.Prime 9hge:8 ≤ 9hle:9 ≤ 8 + 1⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 revert hpleft.«9»p:ℕhge:8 ≤ 9hle:9 ≤ 8 + 1⊢ Nat.Prime 9 → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 <;>left.«8»p:ℕhge:8 ≤ 8hle:8 ≤ 8 + 1⊢ Nat.Prime 8 → Falseleft.«9»p:ℕhge:8 ≤ 9hle:9 ≤ 8 + 1⊢ Nat.Prime 9 → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
    ·right⊢ 8 ∈ lowerBounds {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 rintro m ⟨hmpos, hfree⟩rightm:ℕhmpos:m > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))⊢ 8 ≤ mhleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      by_contra! hltrightm:ℕhmpos:m > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))hlt:m < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      simp only [one_mul] at hfreerightm:ℕhmpos:m > 0hlt:m < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(m ≤ p ∧ p ≤ m + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      interval_cases mright.«1»m:ℕhmpos:1 > 0hlt:1 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(1 ≤ p ∧ p ≤ 1 + 1)⊢ Falseright.«2»m:ℕhmpos:2 > 0hlt:2 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 ≤ p ∧ p ≤ 2 + 1)⊢ Falseright.«3»m:ℕhmpos:3 > 0hlt:3 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 ≤ p ∧ p ≤ 3 + 1)⊢ Falseright.«4»m:ℕhmpos:4 > 0hlt:4 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(4 ≤ p ∧ p ≤ 4 + 1)⊢ Falseright.«5»m:ℕhmpos:5 > 0hlt:5 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(5 ≤ p ∧ p ≤ 5 + 1)⊢ Falseright.«6»m:ℕhmpos:6 > 0hlt:6 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(6 ≤ p ∧ p ≤ 6 + 1)⊢ Falseright.«7»m:ℕhmpos:7 > 0hlt:7 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(7 ≤ p ∧ p ≤ 7 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«1»m:ℕhmpos:1 > 0hlt:1 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(1 ≤ p ∧ p ≤ 1 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 2 (bym:ℕhmpos:1 > 0hlt:1 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(1 ≤ p ∧ p ≤ 1 + 1)⊢ Nat.Prime 2hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«1»m:ℕhmpos:1 > 0hlt:1 < 8⊢ ¬(1 ≤ 2 ∧ 2 ≤ 1 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«2»m:ℕhmpos:2 > 0hlt:2 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 ≤ p ∧ p ≤ 2 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 2 (bym:ℕhmpos:2 > 0hlt:2 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 ≤ p ∧ p ≤ 2 + 1)⊢ Nat.Prime 2hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«2»m:ℕhmpos:2 > 0hlt:2 < 8⊢ ¬(2 ≤ 2 ∧ 2 ≤ 2 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«3»m:ℕhmpos:3 > 0hlt:3 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 ≤ p ∧ p ≤ 3 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 3 (bym:ℕhmpos:3 > 0hlt:3 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 ≤ p ∧ p ≤ 3 + 1)⊢ Nat.Prime 3hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«3»m:ℕhmpos:3 > 0hlt:3 < 8⊢ ¬(3 ≤ 3 ∧ 3 ≤ 3 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«4»m:ℕhmpos:4 > 0hlt:4 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(4 ≤ p ∧ p ≤ 4 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 5 (bym:ℕhmpos:4 > 0hlt:4 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(4 ≤ p ∧ p ≤ 4 + 1)⊢ Nat.Prime 5hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«4»m:ℕhmpos:4 > 0hlt:4 < 8⊢ ¬(4 ≤ 5 ∧ 5 ≤ 4 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«5»m:ℕhmpos:5 > 0hlt:5 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(5 ≤ p ∧ p ≤ 5 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 5 (bym:ℕhmpos:5 > 0hlt:5 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(5 ≤ p ∧ p ≤ 5 + 1)⊢ Nat.Prime 5hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«5»m:ℕhmpos:5 > 0hlt:5 < 8⊢ ¬(5 ≤ 5 ∧ 5 ≤ 5 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«6»m:ℕhmpos:6 > 0hlt:6 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(6 ≤ p ∧ p ≤ 6 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 7 (bym:ℕhmpos:6 > 0hlt:6 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(6 ≤ p ∧ p ≤ 6 + 1)⊢ Nat.Prime 7hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«6»m:ℕhmpos:6 > 0hlt:6 < 8⊢ ¬(6 ≤ 7 ∧ 7 ≤ 6 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
      ·right.«7»m:ℕhmpos:7 > 0hlt:7 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(7 ≤ p ∧ p ≤ 7 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 specialize hfree 7 (bym:ℕhmpos:7 > 0hlt:7 < 8hfree:∀ (p : ℕ), Nat.Prime p → ¬(7 ≤ p ∧ p ≤ 7 + 1)⊢ Nat.Prime 7hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8); revert hfreeright.«7»m:ℕhmpos:7 > 0hlt:7 < 8⊢ ¬(7 ≤ 7 ∧ 7 ≤ 7 + 1) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8; decidehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(1 * m ≤ p ∧ p ≤ 1 * (m + 1))} = 8
  exact hleast.csInf_eqAll goals completed! 🐙



@[category test, AMS 11]
theorem a_2 : a 2 = 4 := by⊢ a 2 = 4
  dsimp [a]⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
  have hleast : IsLeast {m : ℕ | m > 0 ∧ ∀ p : ℕ, p.Prime → ¬ (2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4 := by⊢ a 2 = 4hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
    constructorleft⊢ 4 ∈ {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))}right⊢ 4 ∈ lowerBounds {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
    ·left⊢ 4 ∈ {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 simp only [mem_ofPred_eq]left⊢ 4 > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * 4 ≤ p ∧ p ≤ 2 * (4 + 1))hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      refine ⟨by⊢ 4 > 0hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4, ?_⟩
      intro p hp ⟨hge, hle⟩leftp:ℕhp:Nat.Prime phge:2 * 4 ≤ phle:p ≤ 2 * (4 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      interval_cases pleft.«8»p:ℕhp:Nat.Prime 8hge:2 * 4 ≤ 8hle:8 ≤ 2 * (4 + 1)⊢ Falseleft.«9»p:ℕhp:Nat.Prime 9hge:2 * 4 ≤ 9hle:9 ≤ 2 * (4 + 1)⊢ Falseleft.«10»p:ℕhp:Nat.Prime 10hge:2 * 4 ≤ 10hle:10 ≤ 2 * (4 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 <;>left.«8»p:ℕhp:Nat.Prime 8hge:2 * 4 ≤ 8hle:8 ≤ 2 * (4 + 1)⊢ Falseleft.«9»p:ℕhp:Nat.Prime 9hge:2 * 4 ≤ 9hle:9 ≤ 2 * (4 + 1)⊢ Falseleft.«10»p:ℕhp:Nat.Prime 10hge:2 * 4 ≤ 10hle:10 ≤ 2 * (4 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 revert hpleft.«10»p:ℕhge:2 * 4 ≤ 10hle:10 ≤ 2 * (4 + 1)⊢ Nat.Prime 10 → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 <;>left.«8»p:ℕhge:2 * 4 ≤ 8hle:8 ≤ 2 * (4 + 1)⊢ Nat.Prime 8 → Falseleft.«9»p:ℕhge:2 * 4 ≤ 9hle:9 ≤ 2 * (4 + 1)⊢ Nat.Prime 9 → Falseleft.«10»p:ℕhge:2 * 4 ≤ 10hle:10 ≤ 2 * (4 + 1)⊢ Nat.Prime 10 → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
    ·right⊢ 4 ∈ lowerBounds {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 rintro m ⟨hmpos, hfree⟩rightm:ℕhmpos:m > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))⊢ 4 ≤ mhleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      by_contra! hltrightm:ℕhmpos:m > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))hlt:m < 4⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      interval_cases mright.«1»m:ℕhmpos:1 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 1 ≤ p ∧ p ≤ 2 * (1 + 1))hlt:1 < 4⊢ Falseright.«2»m:ℕhmpos:2 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 2 ≤ p ∧ p ≤ 2 * (2 + 1))hlt:2 < 4⊢ Falseright.«3»m:ℕhmpos:3 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 3 ≤ p ∧ p ≤ 2 * (3 + 1))hlt:3 < 4⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      ·right.«1»m:ℕhmpos:1 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 1 ≤ p ∧ p ≤ 2 * (1 + 1))hlt:1 < 4⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 specialize hfree 2 (bym:ℕhmpos:1 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 1 ≤ p ∧ p ≤ 2 * (1 + 1))hlt:1 < 4⊢ Nat.Prime 2hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4); revert hfreeright.«1»m:ℕhmpos:1 > 0hlt:1 < 4⊢ ¬(2 * 1 ≤ 2 ∧ 2 ≤ 2 * (1 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      ·right.«2»m:ℕhmpos:2 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 2 ≤ p ∧ p ≤ 2 * (2 + 1))hlt:2 < 4⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 specialize hfree 5 (bym:ℕhmpos:2 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 2 ≤ p ∧ p ≤ 2 * (2 + 1))hlt:2 < 4⊢ Nat.Prime 5hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4); revert hfreeright.«2»m:ℕhmpos:2 > 0hlt:2 < 4⊢ ¬(2 * 2 ≤ 5 ∧ 5 ≤ 2 * (2 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
      ·right.«3»m:ℕhmpos:3 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 3 ≤ p ∧ p ≤ 2 * (3 + 1))hlt:3 < 4⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 specialize hfree 7 (bym:ℕhmpos:3 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(2 * 3 ≤ p ∧ p ≤ 2 * (3 + 1))hlt:3 < 4⊢ Nat.Prime 7hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4); revert hfreeright.«3»m:ℕhmpos:3 > 0hlt:3 < 4⊢ ¬(2 * 3 ≤ 7 ∧ 7 ≤ 2 * (3 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4; decidehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} 4⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(2 * m ≤ p ∧ p ≤ 2 * (m + 1))} = 4
  exact hleast.csInf_eqAll goals completed! 🐙



@[category test, AMS 11]
theorem a_3 : a 3 = 8 := by⊢ a 3 = 8
  dsimp [a]⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
  have hleast : IsLeast {m : ℕ | m > 0 ∧ ∀ p : ℕ, p.Prime → ¬ (3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8 := by⊢ a 3 = 8hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
    constructorleft⊢ 8 ∈ {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))}right⊢ 8 ∈ lowerBounds {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
    ·left⊢ 8 ∈ {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 simp only [mem_ofPred_eq]left⊢ 8 > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * 8 ≤ p ∧ p ≤ 3 * (8 + 1))hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      refine ⟨by⊢ 8 > 0hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8, ?_⟩
      intro p hp ⟨hge, hle⟩leftp:ℕhp:Nat.Prime phge:3 * 8 ≤ phle:p ≤ 3 * (8 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      interval_cases pleft.«24»p:ℕhp:Nat.Prime 24hge:3 * 8 ≤ 24hle:24 ≤ 3 * (8 + 1)⊢ Falseleft.«25»p:ℕhp:Nat.Prime 25hge:3 * 8 ≤ 25hle:25 ≤ 3 * (8 + 1)⊢ Falseleft.«26»p:ℕhp:Nat.Prime 26hge:3 * 8 ≤ 26hle:26 ≤ 3 * (8 + 1)⊢ Falseleft.«27»p:ℕhp:Nat.Prime 27hge:3 * 8 ≤ 27hle:27 ≤ 3 * (8 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 <;>left.«24»p:ℕhp:Nat.Prime 24hge:3 * 8 ≤ 24hle:24 ≤ 3 * (8 + 1)⊢ Falseleft.«25»p:ℕhp:Nat.Prime 25hge:3 * 8 ≤ 25hle:25 ≤ 3 * (8 + 1)⊢ Falseleft.«26»p:ℕhp:Nat.Prime 26hge:3 * 8 ≤ 26hle:26 ≤ 3 * (8 + 1)⊢ Falseleft.«27»p:ℕhp:Nat.Prime 27hge:3 * 8 ≤ 27hle:27 ≤ 3 * (8 + 1)⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 revert hpleft.«27»p:ℕhge:3 * 8 ≤ 27hle:27 ≤ 3 * (8 + 1)⊢ Nat.Prime 27 → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 <;>left.«24»p:ℕhge:3 * 8 ≤ 24hle:24 ≤ 3 * (8 + 1)⊢ Nat.Prime 24 → Falseleft.«25»p:ℕhge:3 * 8 ≤ 25hle:25 ≤ 3 * (8 + 1)⊢ Nat.Prime 25 → Falseleft.«26»p:ℕhge:3 * 8 ≤ 26hle:26 ≤ 3 * (8 + 1)⊢ Nat.Prime 26 → Falseleft.«27»p:ℕhge:3 * 8 ≤ 27hle:27 ≤ 3 * (8 + 1)⊢ Nat.Prime 27 → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
    ·right⊢ 8 ∈ lowerBounds {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))}hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 rintro m ⟨hmpos, hfree⟩rightm:ℕhmpos:m > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))⊢ 8 ≤ mhleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      by_contra! hltrightm:ℕhmpos:m > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))hlt:m < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      interval_cases mright.«1»m:ℕhmpos:1 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 1 ≤ p ∧ p ≤ 3 * (1 + 1))hlt:1 < 8⊢ Falseright.«2»m:ℕhmpos:2 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 2 ≤ p ∧ p ≤ 3 * (2 + 1))hlt:2 < 8⊢ Falseright.«3»m:ℕhmpos:3 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 3 ≤ p ∧ p ≤ 3 * (3 + 1))hlt:3 < 8⊢ Falseright.«4»m:ℕhmpos:4 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 4 ≤ p ∧ p ≤ 3 * (4 + 1))hlt:4 < 8⊢ Falseright.«5»m:ℕhmpos:5 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 5 ≤ p ∧ p ≤ 3 * (5 + 1))hlt:5 < 8⊢ Falseright.«6»m:ℕhmpos:6 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 6 ≤ p ∧ p ≤ 3 * (6 + 1))hlt:6 < 8⊢ Falseright.«7»m:ℕhmpos:7 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 7 ≤ p ∧ p ≤ 3 * (7 + 1))hlt:7 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«1»m:ℕhmpos:1 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 1 ≤ p ∧ p ≤ 3 * (1 + 1))hlt:1 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 3 (bym:ℕhmpos:1 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 1 ≤ p ∧ p ≤ 3 * (1 + 1))hlt:1 < 8⊢ Nat.Prime 3hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«1»m:ℕhmpos:1 > 0hlt:1 < 8⊢ ¬(3 * 1 ≤ 3 ∧ 3 ≤ 3 * (1 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«2»m:ℕhmpos:2 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 2 ≤ p ∧ p ≤ 3 * (2 + 1))hlt:2 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 7 (bym:ℕhmpos:2 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 2 ≤ p ∧ p ≤ 3 * (2 + 1))hlt:2 < 8⊢ Nat.Prime 7hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«2»m:ℕhmpos:2 > 0hlt:2 < 8⊢ ¬(3 * 2 ≤ 7 ∧ 7 ≤ 3 * (2 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«3»m:ℕhmpos:3 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 3 ≤ p ∧ p ≤ 3 * (3 + 1))hlt:3 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 11 (bym:ℕhmpos:3 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 3 ≤ p ∧ p ≤ 3 * (3 + 1))hlt:3 < 8⊢ Nat.Prime 11hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«3»m:ℕhmpos:3 > 0hlt:3 < 8⊢ ¬(3 * 3 ≤ 11 ∧ 11 ≤ 3 * (3 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«4»m:ℕhmpos:4 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 4 ≤ p ∧ p ≤ 3 * (4 + 1))hlt:4 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 13 (bym:ℕhmpos:4 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 4 ≤ p ∧ p ≤ 3 * (4 + 1))hlt:4 < 8⊢ Nat.Prime 13hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«4»m:ℕhmpos:4 > 0hlt:4 < 8⊢ ¬(3 * 4 ≤ 13 ∧ 13 ≤ 3 * (4 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«5»m:ℕhmpos:5 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 5 ≤ p ∧ p ≤ 3 * (5 + 1))hlt:5 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 17 (bym:ℕhmpos:5 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 5 ≤ p ∧ p ≤ 3 * (5 + 1))hlt:5 < 8⊢ Nat.Prime 17hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«5»m:ℕhmpos:5 > 0hlt:5 < 8⊢ ¬(3 * 5 ≤ 17 ∧ 17 ≤ 3 * (5 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«6»m:ℕhmpos:6 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 6 ≤ p ∧ p ≤ 3 * (6 + 1))hlt:6 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 19 (bym:ℕhmpos:6 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 6 ≤ p ∧ p ≤ 3 * (6 + 1))hlt:6 < 8⊢ Nat.Prime 19hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«6»m:ℕhmpos:6 > 0hlt:6 < 8⊢ ¬(3 * 6 ≤ 19 ∧ 19 ≤ 3 * (6 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
      ·right.«7»m:ℕhmpos:7 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 7 ≤ p ∧ p ≤ 3 * (7 + 1))hlt:7 < 8⊢ Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 specialize hfree 23 (bym:ℕhmpos:7 > 0hfree:∀ (p : ℕ), Nat.Prime p → ¬(3 * 7 ≤ p ∧ p ≤ 3 * (7 + 1))hlt:7 < 8⊢ Nat.Prime 23hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8 decideAll goals completed! 🐙hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8); revert hfreeright.«7»m:ℕhmpos:7 > 0hlt:7 < 8⊢ ¬(3 * 7 ≤ 23 ∧ 23 ≤ 3 * (7 + 1)) → Falsehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8; decidehleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8hleast:IsLeast {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} 8⊢ sInf {m | m > 0 ∧ ∀ (p : ℕ), Nat.Prime p → ¬(3 * m ≤ p ∧ p ≤ 3 * (m + 1))} = 8
  exact hleast.csInf_eqAll goals completed! 🐙

Sierpinski's conjecture (1958) is precisely that $a(n) >= n$ for all $n$.

@[category research open, AMS 11]
theorem conjecture : ∀ n > 0, a n ≥ n := by⊢ ∀ n > 0, OeisA110835.a n ≥ n
  sorryAll goals completed! 🐙

end OeisA110835