eSHP.first_gap_4

lemma first_gap_4 : first_gap 4 = 7 := by  rw [show first_gap 4 = nth_prime (Nat.find (show ∃ n, nth_prime_gap n = 4 from by    use 3; simp [nth_prime_gap])) from by unfold first_gap; grind]  rw [show Nat.find (show ∃ n, nth_prime_gap n = 4 from by use 3; simp [nth_prime_gap]) = 3 by    simp only [find_eq_iff, nth_prime_gap, reduceAdd, nth_prime_four_eq_eleven,      nth_prime_three_eq_seven, reduceSub, true_and]    intro n hn    interval_cases n <;> norm_num [nth_prime_vals]]  exact nth_prime_three_eq_seven