eSHP.first_gap_6

lemma first_gap_6 : first_gap 6 = 23 := by  unfold first_gap  split_ifs with h  · have h_find : Nat.find h ≤ 8 := by      refine Nat.find_min' h ?_      unfold nth_prime_gap      have h_nth_prime_9 : nth_prime 9 = 29 := by        have : count Nat.Prime 29 = 9 := by decide        simp only [nth_prime]        rw [← this, nth_count]        norm_num      exact h_nth_prime_9.symm ▸ by        have := nth_prime_vals; aesop    interval_cases _ : Nat.find h <;>      simp_all only [find_eq_iff]    all_goals simp_all [nth_prime_gap, nth_prime_vals]  · contrapose! h    use 8    norm_num [nth_prime_gap, nth_prime_vals]    have h_prime_10 : nth_prime 9 = 29 := by      have : nth_prime 9 = nth_prime (count Nat.Prime 29) := by congr      exact this.trans (nth_count <| by norm_num)    exact h_prime_10.symm ▸ rfl