eSHP.exists_prime_gap_record_le

lemma exists_prime_gap_record_le (n : ℕ) :    ∃ m, nth_prime m ≤ nth_prime n ∧ nth_prime_gap n ≤ nth_prime_gap m ∧      prime_gap_record (nth_prime m) (nth_prime_gap m) := by  let g := nth_prime_gap n  let S := {k | k ≤ n ∧ g ≤ nth_prime_gap k}  obtain ⟨m, hm_mem, hm_min⟩ : ∃ m ∈ S, ∀ k ∈ S, m ≤ k :=    ⟨Nat.find <| show S.Nonempty from ⟨n, le_rfl, le_rfl⟩,      Nat.find_spec <| show S.Nonempty from ⟨n, le_rfl, le_rfl⟩,      fun k hk ↦ Nat.find_min' _ hk⟩  refine ⟨m, ?_, hm_mem.2, m, rfl, rfl, fun k hk ↦ ?_⟩  · exact monotone_nat_of_le_succ (fun n ↦ nth_monotone infinite_setOf_prime n.le_succ) hm_mem.1  · contrapose! hk    exact monotone_nat_of_le_succ (fun n ↦ nth_monotone infinite_setOf_prime n.le_succ)      (le_of_not_gt fun h ↦ not_lt_of_ge        (hm_min _ ⟨by linarith [hm_mem.1], by linarith [hm_mem.2]⟩) h)