Inner eq inner conj of ker le

lemma inner_eq_inner_conj_of_ker_le (ρ σ : MState d)    (H : HermitianMat d ℂ) (hker : σ.M.ker ≤ ρ.M.ker) (γ : ℝ) (hγ : γ ≠ 0) :    ⟪ρ.M, H⟫_ℝ = ⟪ρ.M.conj (σ.M ^ γ).mat, H.conj (σ.M ^ (-γ)).mat⟫_ℝ := by  -- Since $\sigma^\gamma \sigma^{-\gamma}$ acts as the identity on the support of $\rho$, we can simplify the expression.  have h_support : (σ.M ^ γ).mat * (σ.M ^ (-γ)).mat = σ.M.supportProj.mat ∧ (σ.M ^ (-γ)).mat * (σ.M ^ γ).mat = σ.M.supportProj.mat := by    exact ⟨ rpow_mul_neg_rpow_eq_supportProj σ.nonneg γ hγ, by simpa using rpow_mul_neg_rpow_eq_supportProj σ.nonneg ( -γ ) ( neg_ne_zero.mpr hγ ) ⟩;  simp only [HermitianMat.inner_def, HermitianMat.conj_apply_mat];  have h_support : σ.M.supportProj.mat * ρ.M.mat = ρ.M.mat ∧ ρ.M.mat * σ.M.supportProj.mat = ρ.M.mat := by    exact ⟨ supportProj_mul_of_ker_le hker, mul_supportProj_of_ker_le hker ⟩;  have h_trace_cyclic : Matrix.trace ((σ.M ^ γ).mat * ρ.M.mat * (σ.M ^ γ).mat * (σ.M ^ (-γ)).mat * H.mat * (σ.M ^ (-γ)).mat) = Matrix.trace ((σ.M ^ (-γ)).mat * (σ.M ^ γ).mat * ρ.M.mat * (σ.M ^ γ).mat * (σ.M ^ (-γ)).mat * H.mat) := by    rw [ ← Matrix.trace_mul_comm ] ; simp [ Matrix.mul_assoc ] ;  simp_all [ mul_assoc, Matrix.trace_mul_comm ( ( σ.M ^ γ ).mat ) ];  simp_all [ ← mul_assoc ]