niceKernel_eq_inv

lemma niceKernel_eq_inv {r x : ℝ} (hr : 0 < r ∧ r < π) (hx : 0 ≤ x ∧ x ≤ r) :    niceKernel r x = r⁻¹ := by  rw [niceKernel, ite_eq_iff', normSq_eq_norm_sq]  refine ⟨fun _ ↦ rfl, fun hexp ↦ min_eq_left ?_⟩  have : 0 < x := by    contrapose! hexp    simp [ge_antisymm hx.1 hexp]  apply le_add_of_nonneg_of_le zero_le_one  suffices 1 - r ^ 2 / 2 ≤ Real.cos x by    have : Real.cos x < 1 := by      rw [← Real.cos_zero]      apply Real.cos_lt_cos_of_nonneg_of_le_pi <;> linarith    rw [norm_sub_rev, norm_exp_I_mul_ofReal_sub_one, norm_mul, RCLike.norm_ofNat, Real.norm_eq_abs,      Real.abs_sin_half, mul_pow, Real.sq_sqrt, le_div_iff₀', mul_inv_le_iff₀] <;> linarith  grw [Real.one_sub_sq_div_two_le_cos]  apply Real.cos_le_cos_of_nonneg_of_le_pi <;> linarith