FormalConjectures.Wikipedia.Oppermann

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

Oppermann's Conjecture

References:

Wikipedia

Luan Alberto Ferreira, Real exponential sums over primes and prime gaps

open Finset Filternamespace Oppermann

For every integer $x \ge 2$ there exists a prime between $x(x-1)$ and $x^2$.

@[category research open, AMS 11]
theorem oppermann_conjecture.parts.i (x : ℕ) (hx : 2 ≤ x) :
    ∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime := byx:ℕhx:2 ≤ x⊢ ∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p
  sorryAll goals completed! 🐙

For every integer $x \ge 2$ there exists a prime between $x^2$ and $x(x+1)$.

@[category research open, AMS 11]
theorem oppermann_conjecture.parts.ii (x : ℕ) (hx : 2 ≤ x) :
    ∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime := byx:ℕhx:2 ≤ x⊢ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p
  sorryAll goals completed! 🐙

Oppermann's Conjecture: For every integer $x \ge 2$, the following hold:

There exists a prime between $x(x-1)$ and $x^2$.

There exists a prime between $x^2$ and $x(x+1)$.

@[category research open, AMS 11]
theorem oppermann_conjecture (x : ℕ) (hx : 2 ≤ x) :
    (∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime) ∧
    (∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime) := byx:ℕhx:2 ≤ x⊢ (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p
  sorryAll goals completed! 🐙

Oppermann's conjecture implies Brocard's conjecture.


@[category textbook, AMS 11]
theorem oppermann_implies_brocard (n : ℕ) (hn : 1 ≤ n) (P : type_of% oppermann_conjecture) :
    letI prev := n.nth Nat.Prime
    letI next := (n+1).nth Nat.Prime
    4 ≤ ((Ioo (prev ^ 2) (next ^ 2)).filter Nat.Prime).card := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))
  set prev := n.nth Nat.Prime with hprev_defn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime n⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))
  set next := (n+1).nth Nat.Prime with hnext_defn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hprev_prime : prev.Prime := Nat.prime_nth_prime nn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prev⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hnext_prime : next.Prime := Nat.prime_nth_prime (n+1)n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hprev_ge : 3 ≤ prev := Nat.nth_prime_one_eq_three ▸
    (Nat.nth_le_nth Nat.infinite_setOfPred_prime).mpr hnn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prev⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hlt : prev < next :=
    Nat.nth_strictMono Nat.infinite_setOfPred_prime (Nat.lt_succ_self n)n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hgap : prev + 2 ≤ next := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
    rcases hprev_prime.odd_of_ne_two (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < next⊢ prev ≠ 2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) omegaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))) with ⟨k, hk⟩
    rcases hnext_prime.odd_of_ne_two (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nextk:ℕhk:prev = 2 * k + 1⊢ next ≠ 2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) omegaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))) with ⟨m, hm⟩
    omegan:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  obtain ⟨_, p1, hp1mem, hp1p⟩ := P prev (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ next⊢ 2 ≤ prevn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) omegaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  obtain ⟨⟨p2, hp2mem, hp2p⟩, p3, hp3mem, hp3p⟩ := P (prev+1) (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1⊢ 2 ≤ prev + 1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) omegaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  obtain ⟨p4, hp4mem, hp4p⟩ := (P (prev+2) (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3⊢ 2 ≤ prev + 2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3p4:ℕhp4mem:p4 ∈ Ioo ((prev + 2) * (prev + 2 - 1)) ((prev + 2) ^ 2)hp4p:Nat.Prime p4⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) omegaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3p4:ℕhp4mem:p4 ∈ Ioo ((prev + 2) * (prev + 2 - 1)) ((prev + 2) ^ 2)hp4p:Nat.Prime p4⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))))).1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1mem:p1 ∈ Ioo (prev ^ 2) (prev * (prev + 1))hp1p:Nat.Prime p1p2:ℕhp2mem:p2 ∈ Ioo ((prev + 1) * (prev + 1 - 1)) ((prev + 1) ^ 2)hp2p:Nat.Prime p2p3:ℕhp3mem:p3 ∈ Ioo ((prev + 1) ^ 2) ((prev + 1) * (prev + 1 + 1))hp3p:Nat.Prime p3p4:ℕhp4mem:p4 ∈ Ioo ((prev + 2) * (prev + 2 - 1)) ((prev + 2) ^ 2)hp4p:Nat.Prime p4⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  simp only [Finset.mem_Ioo, show prev + 1 - 1 = prev from rfl,
    show prev + 2 - 1 = prev + 1 from rfl, show prev + 1 + 1 = prev + 2 from rfl]
    at hp1mem hp2mem hp3mem hp4memn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hsq : (prev + 2)^2 ≤ next^2 := Nat.pow_le_pow_left hgap 2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hsq1 : (prev + 1)^2 ≤ next^2 := Nat.pow_le_pow_left (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2⊢ prev + 1 ≤ nextn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) omegaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))) 2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hb0 : prev * (prev + 1) < (prev + 1)^2 := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) nlinarithn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have hb1 : (prev + 1) * (prev + 2) < (prev + 2)^2 := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) nlinarithn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have h12 : p1 < p2 := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) linarith [hp1mem.2, hp2mem.1]n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have h23 : p2 < p3 := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) linarith [hp2mem.2, hp3mem.1]n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  have h34 : p3 < p4 := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 4 ≤ #(filter Nat.Prime (Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))) linarith [hp3mem.2, hp4mem.1]n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ 4 ≤ #(filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)))
  refine ((show ({p1, p2, p3, p4} : Finset ℕ).card = 4 from ?_) ▸
    Finset.card_le_card (s := {p1, p2, p3, p4}) ?_)refine_1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ #{p1, p2, p3, p4} = 4refine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ {p1, p2, p3, p4} ⊆ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))
  ·refine_1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ #{p1, p2, p3, p4} = 4 simp [Finset.card_insert_of_notMem, h12.ne, (h12.trans h23).ne,
      (h12.trans (h23.trans h34)).ne, h23.ne, (h23.trans h34).ne, h34.ne]All goals completed! 🐙
  ·refine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4⊢ {p1, p2, p3, p4} ⊆ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)) intro x hxrefine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4x:ℕhx:x ∈ {p1, p2, p3, p4}⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))
    simp only [Finset.mem_insert, Finset.mem_singleton] at hxrefine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3h34:p3 < p4x:ℕhx:x = p1 ∨ x = p2 ∨ x = p3 ∨ x = p4⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))
    rcases hx with rfl | rfl | rfl | rflrefine_2.inln:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h23:p2 < p3h34:p3 < p4x:ℕhp1p:Nat.Prime xhp1mem:prev ^ 2 < x ∧ x < prev * (prev + 1)h12:x < p2⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))refine_2.inr.inln:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h34:p3 < p4x:ℕhp2p:Nat.Prime xhp2mem:(prev + 1) * prev < x ∧ x < (prev + 1) ^ 2h12:p1 < xh23:x < p3⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))refine_2.inr.inr.inln:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2x:ℕhp3p:Nat.Prime xhp3mem:(prev + 1) ^ 2 < x ∧ x < (prev + 1) * (prev + 2)h23:p2 < xh34:x < p4⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))refine_2.inr.inr.inrn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3x:ℕhp4p:Nat.Prime xhp4mem:(prev + 2) * (prev + 1) < x ∧ x < (prev + 2) ^ 2h34:p3 < x⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2)) <;>refine_2.inln:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h23:p2 < p3h34:p3 < p4x:ℕhp1p:Nat.Prime xhp1mem:prev ^ 2 < x ∧ x < prev * (prev + 1)h12:x < p2⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))refine_2.inr.inln:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h34:p3 < p4x:ℕhp2p:Nat.Prime xhp2mem:(prev + 1) * prev < x ∧ x < (prev + 1) ^ 2h12:p1 < xh23:x < p3⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))refine_2.inr.inr.inln:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2x:ℕhp3p:Nat.Prime xhp3mem:(prev + 1) ^ 2 < x ∧ x < (prev + 1) * (prev + 2)h23:p2 < xh34:x < p4⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))refine_2.inr.inr.inrn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3x:ℕhp4p:Nat.Prime xhp4mem:(prev + 2) * (prev + 1) < x ∧ x < (prev + 2) ^ 2h34:p3 < x⊢ x ∈ filter Nat.Prime (Ioo (prev ^ 2) (next ^ 2))
      refine Finset.mem_filter.mpr ⟨Finset.mem_Ioo.mpr ⟨?_, ?_⟩, byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3x:ℕhp4p:Nat.Prime xhp4mem:(prev + 2) * (prev + 1) < x ∧ x < (prev + 2) ^ 2h34:p3 < x⊢ Nat.Prime x assumptionAll goals completed! 🐙⟩ <;>refine_2.inl.refine_1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h23:p2 < p3h34:p3 < p4x:ℕhp1p:Nat.Prime xhp1mem:prev ^ 2 < x ∧ x < prev * (prev + 1)h12:x < p2⊢ prev ^ 2 < xrefine_2.inl.refine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h23:p2 < p3h34:p3 < p4x:ℕhp1p:Nat.Prime xhp1mem:prev ^ 2 < x ∧ x < prev * (prev + 1)h12:x < p2⊢ x < next ^ 2refine_2.inr.inl.refine_1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h34:p3 < p4x:ℕhp2p:Nat.Prime xhp2mem:(prev + 1) * prev < x ∧ x < (prev + 1) ^ 2h12:p1 < xh23:x < p3⊢ prev ^ 2 < xrefine_2.inr.inl.refine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p3:ℕhp3p:Nat.Prime p3p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h34:p3 < p4x:ℕhp2p:Nat.Prime xhp2mem:(prev + 1) * prev < x ∧ x < (prev + 1) ^ 2h12:p1 < xh23:x < p3⊢ x < next ^ 2refine_2.inr.inr.inl.refine_1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2x:ℕhp3p:Nat.Prime xhp3mem:(prev + 1) ^ 2 < x ∧ x < (prev + 1) * (prev + 2)h23:p2 < xh34:x < p4⊢ prev ^ 2 < xrefine_2.inr.inr.inl.refine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p4:ℕhp4p:Nat.Prime p4hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp4mem:(prev + 2) * (prev + 1) < p4 ∧ p4 < (prev + 2) ^ 2hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2x:ℕhp3p:Nat.Prime xhp3mem:(prev + 1) ^ 2 < x ∧ x < (prev + 1) * (prev + 2)h23:p2 < xh34:x < p4⊢ x < next ^ 2refine_2.inr.inr.inr.refine_1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3x:ℕhp4p:Nat.Prime xhp4mem:(prev + 2) * (prev + 1) < x ∧ x < (prev + 2) ^ 2h34:p3 < x⊢ prev ^ 2 < xrefine_2.inr.inr.inr.refine_2n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pprev:ℕ := Nat.nth Nat.Prime nhprev_def:prev = Nat.nth Nat.Prime nnext:ℕ := Nat.nth Nat.Prime (n + 1)hnext_def:next = Nat.nth Nat.Prime (n + 1)hprev_prime:Nat.Prime prevhnext_prime:Nat.Prime nexthprev_ge:3 ≤ prevhlt:prev < nexthgap:prev + 2 ≤ nextleft✝:∃ p ∈ Ioo (prev * (prev - 1)) (prev ^ 2), Nat.Prime pp1:ℕhp1p:Nat.Prime p1p2:ℕhp2p:Nat.Prime p2p3:ℕhp3p:Nat.Prime p3hp1mem:prev ^ 2 < p1 ∧ p1 < prev * (prev + 1)hp2mem:(prev + 1) * prev < p2 ∧ p2 < (prev + 1) ^ 2hp3mem:(prev + 1) ^ 2 < p3 ∧ p3 < (prev + 1) * (prev + 2)hsq:(prev + 2) ^ 2 ≤ next ^ 2hsq1:(prev + 1) ^ 2 ≤ next ^ 2hb0:prev * (prev + 1) < (prev + 1) ^ 2hb1:(prev + 1) * (prev + 2) < (prev + 2) ^ 2h12:p1 < p2h23:p2 < p3x:ℕhp4p:Nat.Prime xhp4mem:(prev + 2) * (prev + 1) < x ∧ x < (prev + 2) ^ 2h34:p3 < x⊢ x < next ^ 2
      linarith [hp1mem.1, hp1mem.2, hp2mem.1, hp2mem.2, hp3mem.1, hp3mem.2,
        hp4mem.1, hp4mem.2, hb0, hb1, hsq, hsq1]All goals completed! 🐙

Oppermann's conjecture implies Legendre's conjecture.


@[category textbook, AMS 11]
theorem oppermann_implies_legendre (n : ℕ) (hn : 1 ≤ n) (P : type_of% oppermann_conjecture) :
    ∃ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2), p.Prime := byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ ∃ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p
  obtain ⟨⟨p, ph⟩, _⟩ := P (n + 1) (byn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p⊢ 2 ≤ n + 1n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pright✝:∃ p ∈ Ioo ((n + 1) ^ 2) ((n + 1) * (n + 1 + 1)), Nat.Prime pp:ℕph:p ∈ Ioo ((n + 1) * (n + 1 - 1)) ((n + 1) ^ 2) ∧ Nat.Prime p⊢ ∃ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p simpaAll goals completed! 🐙n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pright✝:∃ p ∈ Ioo ((n + 1) ^ 2) ((n + 1) * (n + 1 + 1)), Nat.Prime pp:ℕph:p ∈ Ioo ((n + 1) * (n + 1 - 1)) ((n + 1) ^ 2) ∧ Nat.Prime p⊢ ∃ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p)n:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pright✝:∃ p ∈ Ioo ((n + 1) ^ 2) ((n + 1) * (n + 1 + 1)), Nat.Prime pp:ℕph:p ∈ Ioo ((n + 1) * (n + 1 - 1)) ((n + 1) ^ 2) ∧ Nat.Prime p⊢ ∃ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p
  use phn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pright✝:∃ p ∈ Ioo ((n + 1) ^ 2) ((n + 1) * (n + 1 + 1)), Nat.Prime pp:ℕph:p ∈ Ioo ((n + 1) * (n + 1 - 1)) ((n + 1) ^ 2) ∧ Nat.Prime p⊢ p ∈ Ioo (n ^ 2) ((n + 1) ^ 2) ∧ Nat.Prime p
  refine ⟨Finset.Ioo_subset_Ioo_left ?_ ph.1, ph.2⟩hn:ℕhn:1 ≤ nP:∀ (x : ℕ), 2 ≤ x → (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime pright✝:∃ p ∈ Ioo ((n + 1) ^ 2) ((n + 1) * (n + 1 + 1)), Nat.Prime pp:ℕph:p ∈ Ioo ((n + 1) * (n + 1 - 1)) ((n + 1) ^ 2) ∧ Nat.Prime p⊢ n ^ 2 ≤ (n + 1) * (n + 1 - 1)
  push_cast [sq, add_one_mul,le_self_add]All goals completed! 🐙

Ferreira proved that Oppermann's conjecture is true for sufficiently large x.

@[category research solved, AMS 11]
theorem oppermann_conjecture.ferreira_large_x : ∀ᶠ x in atTop,
    (∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime) ∧
    (∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime) := by⊢ ∀ᶠ (x : ℕ) in atTop, (∃ p ∈ Ioo (x * (x - 1)) (x ^ 2), Nat.Prime p) ∧ ∃ p ∈ Ioo (x ^ 2) (x * (x + 1)), Nat.Prime p
  sorryAll goals completed! 🐙

end Oppermann