Β eq deriv S U

theorem β_eq_deriv_S_U {β : ℝ}    (hZne : H.partitionZ d β ≠ 0)    (hZint : (β : ℂ) ∈ interior (H.ZComplexConvergenceDomain d))    (hU' : deriv (H.internalU d) β ≠ 0) :    β = (deriv (H.entropySβ d) β) / deriv (H.internalU d) β := by  have hZ : ContDiffAt ℝ ⊤ (H.partitionZ d) β :=    H.contDiffAt_partitionZ_of_mem_interior_convergenceDomain d hZint  unfold entropySβ internalU   --Show the differentiability side-goals  have hlogDiff : DifferentiableAt ℝ (fun β => Real.log (H.partitionZ d β)) β :=    (hZ.differentiableAt (by simp)).log hZne  have hlogDerivDiff : DifferentiableAt ℝ (deriv fun β => Real.log (H.partitionZ d β)) β := by    have := ((hZ.log hZne).fderiv_right (m := ⊤) (OrderTop.le_top _)).differentiableAt (by simp)    unfold deriv    fun_prop  have hderiv : deriv (deriv fun β => Real.log (H.partitionZ d β)) β ≠ 0 := by    intro hzero    apply hU'    change deriv (-fun β => deriv (fun β' => Real.log (H.partitionZ d β')) β) β = 0    simp [deriv.neg, hzero]   --Main goal  simp only [mul_neg]  erw [deriv.neg', deriv_add, deriv.neg']  dsimp  erw [deriv_mul]  simp only [deriv_id'', one_mul, neg_add_rev, add_neg_cancel_comm_assoc, neg_div_neg_eq]  exact (mul_div_cancel_right₀ β hderiv).symm  --Discharge those side-goals  · exact differentiableAt_id  · exact hlogDerivDiff  · fun_prop (disch := assumption)  · fun_prop (disch := assumption)