eSHP.nth_prime_vals

lemma nth_prime_vals : nth_prime 0 = 2 ∧ nth_prime 1 = 3 ∧ nth_prime 2 = 5 ∧    nth_prime 3 = 7 ∧ nth_prime 4 = 11 ∧ nth_prime 5 = 13 ∧ nth_prime 6 = 17 ∧    nth_prime 7 = 19 ∧ nth_prime 8 = 23 := by  norm_num [nth_prime, Nat.nth_zero]  refine ⟨?_, ?_, ?_, ?_, ?_⟩  · exact le_antisymm (Nat.sInf_le Nat.prime_two)      (le_csInf ⟨2, prime_two⟩ fun p hp ↦ Prime.two_le hp)  · rw [eq_comm, nth_eq_sInf]    refine le_antisymm ?_ ?_    · refine le_csInf ?_ ?_ <;> norm_num      · exact ⟨_, prime_nth_prime 5, fun k hk ↦ nth_strictMono infinite_setOf_prime hk⟩      · intro b hb hb'        contrapose! hb'        use count Nat.Prime b        interval_cases b <;> simp +arith +decide at hb ⊢    · exact Nat.sInf_le ⟨by norm_num, fun k hk ↦ by interval_cases k <;> norm_num [*]⟩  · have h_nth_prime_6 : nth_prime 6 = 17 := by      have : count Nat.Prime 17 = 6 := by decide      rw [← this, nth_prime, nth_count]      norm_num    exact h_nth_prime_6  · have h_prime_7 : nth_prime 7 = 19 := by      have : nth_prime 7 = nth_prime (count Nat.Prime 19) := by congr      exact this.trans (nth_count <| by norm_num)    exact h_prime_7  · have h_prime_8 : nth_prime 8 = 23 := by      have : count Nat.Prime 23 = 8 := by decide      rw [← this, nth_prime, nth_count]      norm_num    exact h_prime_8