Entropy A eq entropy Z

theorem entropy_A_eq_entropy_Z (T : ℝ) (hT : T ≠ 0)    (hZne : H.partitionZ d (1 / T) ≠ 0)    (hZint : ((1 / T : ℝ) : ℂ) ∈ interior (H.ZComplexConvergenceDomain d)) :    entropyS H d T = entropySβ H d (1 / T) := by  have hZdiff : DifferentiableAt ℝ (H.partitionZ d) (1 / T) :=    (H.contDiffAt_partitionZ_of_mem_interior_convergenceDomain d hZint).differentiableAt      (by simp)  dsimp [entropyS, entropySβ, internalU, partitionZT]  unfold helmholtzA  erw [deriv_mul]  rw [deriv_neg'', neg_mul, one_mul, neg_add_rev, neg_neg, mul_neg, add_comm]  congr 1  simp_rw [partitionZT]  have hdc := deriv_comp (h := fun T ↦ T⁻¹) (h₂ := fun β => Real.log (H.partitionZ d β)) T ?_ ?_  unfold Function.comp at hdc  simp only [hdc, one_div, deriv_inv', mul_neg, neg_inj]  field_simp  ring_nf  --Show the differentiability side-goals  · rw [← one_div]    fun_prop (disch := assumption)  · fun_prop (disch := assumption)  · fun_prop  · simp_rw [partitionZT]    fun_prop (disch := assumption)