Operator ineq SSA

theorem operator_ineq_SSA [Nonempty dA] [Nonempty dB] [Nonempty dC]    (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ)    (hρ : ρAB.mat.PosDef) (hσ : σBC.mat.PosDef) :    ρAB.traceRight⁻¹ ⊗ₖ σBC ≤      (ρAB⁻¹ ⊗ₖ σBC.traceLeft).reindex (Equiv.prodAssoc dA dB dC) := by  have h_inv_symm : ((ρAB.traceRight ⊗ₖ σBC⁻¹).reindex (Equiv.prodAssoc dA dB dC).symm)⁻¹ ≤ (ρAB ⊗ₖ σBC.traceLeft⁻¹)⁻¹ := by    apply HermitianMat.inv_antitone;    · apply HermitianMat.PosDef_kronecker ρAB (σBC.traceLeft)⁻¹ hρ (PosDef_traceLeft σBC hσ).inv;    · exact intermediate_ineq ρAB σBC hρ hσ;  have h_inv_symm : ((ρAB.traceRight ⊗ₖ σBC⁻¹).reindex (Equiv.prodAssoc dA dB dC).symm)⁻¹ = (ρAB.traceRight⁻¹ ⊗ₖ σBC).reindex (Equiv.prodAssoc dA dB dC).symm := by    have h_inv_symm : (ρAB.traceRight ⊗ₖ σBC⁻¹)⁻¹ = ρAB.traceRight⁻¹ ⊗ₖ (σBC⁻¹)⁻¹ := by      convert HermitianMat.inv_kronecker _ _ using 1;      · infer_instance;      · exact ⟨ ⟨ Classical.arbitrary dB, Classical.arbitrary dC ⟩ ⟩;      · have h_trace_right_pos_def : (ρAB.traceRight).mat.PosDef := by          exact PosDef_traceRight ρAB hρ        exact ⟨by exact PosDef_traceRight ρAB hρ |>.isUnit⟩      · have h_inv_symm : σBC⁻¹.NonSingular := by          have h_inv_symm : σBC.NonSingular := by            exact nonSingular_of_posDef hσ          exact nonSingular_iff_inv.mpr h_inv_symm;        exact h_inv_symm;    convert congr_arg ( fun x : HermitianMat _ _ => x.reindex ( Equiv.prodAssoc dA dB dC ).symm ) h_inv_symm using 1;    · apply HermitianMat.inv_reindex    · convert rfl;      apply HermitianMat.ext;      convert Matrix.nonsing_inv_nonsing_inv _ _;      exact isUnit_iff_ne_zero.mpr ( hσ.det_pos.ne' );  have h_inv_symm : (ρAB ⊗ₖ σBC.traceLeft⁻¹)⁻¹ = ρAB⁻¹ ⊗ₖ σBC.traceLeft := by    have h_inv_symm : (ρAB ⊗ₖ σBC.traceLeft⁻¹)⁻¹ = ρAB⁻¹ ⊗ₖ (σBC.traceLeft⁻¹)⁻¹ := by      convert HermitianMat.inv_kronecker ρAB ( σBC.traceLeft⁻¹ ) using 1;      · exact nonSingular_of_posDef hρ;      · have h_inv_symm : σBC.traceLeft.mat.PosDef := by          exact PosDef_traceLeft σBC hσ;        -- Since σBC.traceLeft is positive definite, its inverse is also positive definite, and hence non-singular.        have h_inv_pos_def : (σBC.traceLeft⁻¹).mat.PosDef := by          convert h_inv_symm.inv using 1;        exact nonSingular_of_posDef h_inv_pos_def;    convert h_inv_symm using 1;    have h_inv_symm : (σBC.traceLeft⁻¹)⁻¹ = σBC.traceLeft := by      have h_inv_symm : (σBC.traceLeft⁻¹).mat * σBC.traceLeft.mat = 1 := by        have h_inv_symm : (σBC.traceLeft⁻¹).mat * σBC.traceLeft.mat = 1 := by          have h_inv_symm : σBC.traceLeft.mat.PosDef := by            exact PosDef_traceLeft σBC hσ          convert Matrix.nonsing_inv_mul _ _;          exact isUnit_iff_ne_zero.mpr h_inv_symm.det_pos.ne';        exact h_inv_symm      have h_inv_symm : (σBC.traceLeft⁻¹ : HermitianMat dC ℂ).mat⁻¹ = σBC.traceLeft.mat := by        rw [ Matrix.inv_eq_right_inv h_inv_symm ];      exact Eq.symm (HermitianMat.ext (id (Eq.symm h_inv_symm)));    rw [h_inv_symm];  have h_inv_symm : (ρAB.traceRight⁻¹ ⊗ₖ σBC).reindex (Equiv.prodAssoc dA dB dC).symm ≤ ρAB⁻¹ ⊗ₖ σBC.traceLeft := by    aesop;  convert HermitianMat.reindex_le_reindex_iff ( Equiv.prodAssoc dA dB dC ) _ _ |>.2 h_inv_symm using 1