Deriv Within mean Energy Beta eq neg variance

lemma derivWithin_meanEnergy_Beta_eq_neg_variance    [MeasurableSingletonClass ι][𝓒.IsFinite] (T : Temperature) (hT_pos : 0 < T.val) :    derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) (T.β : ℝ) = - 𝓒.energyVariance T := by  let β₀ := (T.β : ℝ)  have hβ₀_pos : 0 < β₀ := beta_pos T hT_pos  have h_eq_on : Set.EqOn 𝓒.meanEnergyBeta 𝓒.meanEnergyBetaReal (Set.Ioi 0) := by    intro b hb; exact meanEnergy_Beta_eq_finite 𝓒 b hb  rw [derivWithin_congr h_eq_on (h_eq_on hβ₀_pos)]  have h_diff : DifferentiableAt ℝ 𝓒.meanEnergyBetaReal β₀ :=    (differentiable_meanEnergyBetaReal 𝓒) β₀  rw [h_diff.derivWithin (uniqueDiffOn_Ioi 0 β₀ hβ₀_pos)]  rw [deriv_meanEnergyBetaReal 𝓒 β₀]  have h_U_eq : 𝓒.meanEnergyBetaReal β₀ = 𝓒.meanEnergy T := by    rw [← meanEnergy_Beta_eq_finite 𝓒 β₀ hβ₀_pos]    simp [meanEnergyBeta]    simp_all only [NNReal.coe_pos, toNNReal_coe, ofβ_β, β₀]  have h_prob_eq (i : ι) : 𝓒.probabilityBetaReal β₀ i = 𝓒.probability T i := by    unfold probabilityBetaReal CanonicalEnsemble.probability    congr 1    · unfold mathematicalPartitionFunctionBetaReal      rw [mathematicalPartitionFunction_of_fintype]  rw [h_U_eq]  simp_rw [h_prob_eq]  rw [energyVariance_of_fintype 𝓒 T]  ring