Sandwiched Trace Functional conj unitary hermitian

theorem sandwichedTraceFunctional_conj_unitary_hermitian    (U : Matrix.unitaryGroup d ℂ) (A B : HermitianMat d ℂ) :    let γ := (1 - α) / (2 * α)    ((A.conj U.val).conj ((B.conj U.val) ^ γ).mat ^ α).trace =      ((A.conj (B ^ γ).mat) ^ α).trace := by  have h_rpow_conj : ∀ (A : HermitianMat d ℂ) (U : Matrix.unitaryGroup d ℂ) (r : ℝ), (HermitianMat.conj U.val A) ^ r = HermitianMat.conj U.val (A ^ r) := by    -- Apply the theorem `HermitianMat.rpow_conj_unitary` to conclude the proof.    apply HermitianMat.rpow_conj_unitary;  have h_conj_conj : ∀ (A B : HermitianMat d ℂ) (U : Matrix.unitaryGroup d ℂ), (HermitianMat.conj U.val A).conj ((HermitianMat.conj U.val B).mat) = HermitianMat.conj U.val (A.conj B.mat) := by    intros A B U    simp [HermitianMat.conj];    have h_unitary : ∀ (U : Matrix.unitaryGroup d ℂ), U.val * U.val.conjTranspose = 1 := by      exact fun U => U.2.2;    simp [ ← mul_assoc ];    have := h_unitary U; simp_all [ Matrix.mul_assoc, mul_eq_one_comm.mp this ] ;  simp_all [ HermitianMat.conj_apply_mat ]