Sandwiched Trace Functional self

theorem sandwichedTraceFunctional_self (hα : 0 < α) (ρ : MState d) :    Q̃_ α(ρ‖ρ) = 1 := by  by_cases h : α = 1;  · subst h; simp [ sandwichedTraceFunctional ] ;  · unfold sandwichedTraceFunctional;    have := ρ.pos;    have h_simp : (ρ.M.conj (ρ.M ^ ((1 - α) / (2 * α))).mat) = ρ.M ^ (1 + 2 * ((1 - α) / (2 * α))) := by      rw [ ← HermitianMat.conj_rpow ];      · rw [ HermitianMat.rpow_one ];      · exact le_of_lt this;      · exact div_ne_zero ( sub_ne_zero_of_ne ( Ne.symm h ) ) ( mul_ne_zero two_ne_zero hα.ne' );      · cases lt_or_gt_of_ne h <;> nlinarith [ mul_div_cancel₀ ( 1 - α ) ( by positivity : ( 2 * α ) ≠ 0 ) ];    have h_simp : (ρ.M ^ (1 + 2 * ((1 - α) / (2 * α)))) ^ α = ρ.M ^ ((1 + 2 * ((1 - α) / (2 * α))) * α) := by      rw [ ← HermitianMat.rpow_mul ];      exact le_of_lt this;    field_simp at *;    simp_all only [add_sub_cancel, one_div, HermitianMat.rpow_one, MState.tr]