Entropy A eq entropy Z

theorem entropy_A_eq_entropy_Z (T β : ℝ) (hβT : T * β = 1) (hi : H.ZIntegrable d β)    : EntropyS H d T = EntropySβ H d β := by  have hTnz : T ≠ 0 := left_ne_zero_of_mul_eq_one hβT  have hβnz : β ≠ 0 := right_ne_zero_of_mul_eq_one hβT  have hβT' := eq_one_div_of_mul_eq_one_right hβT  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  · rw [PartitionZT, hβT']  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, hβT']  field_simp  ring_nf  --Show the differentiability side-goals  · rw [← one_div, ← hβT']    have h₁ := hi.2    have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt (OrderTop.le_top 1)    fun_prop (disch := assumption)  · fun_prop (disch := assumption)  · fun_prop  · simp_rw [PartitionZT]    rw [hβT'] at hi    have := hi.2    have := (DifferentiableAt_Z_if_ZIntegrable hi).differentiableAt (OrderTop.le_top 1)    fun_prop (disch := assumption)