W mat sq le one

theorem W_mat_sq_le_one [Nonempty dA] [Nonempty dB] [Nonempty dC]    (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ)    (hρ : ρAB.mat.PosDef) (hσ : σBC.mat.PosDef) :    (W_mat ρAB σBC)ᴴ * (W_mat ρAB σBC) ≤ 1 := by  rw [W_mat_eq_three_factors]  have h_T₂ := T₂_sq_le_one (dA := dA) σBC hσ  have h_step1 : (PERM_mat dA dB dC)ᴴ * ((T₂_mat dA dB dC σBC)ᴴ * (T₂_mat dA dB dC σBC)) *      PERM_mat dA dB dC ≤ 1 := by    calc _ ≤ (PERM_mat dA dB dC)ᴴ * 1 * PERM_mat dA dB dC :=          Matrix.PosSemidef.conjTranspose_mul_mul_mono _ h_T₂        _ = 1 := by rw [Matrix.mul_one, PERM_isometry]  calc _ = (T₁_mat dA dB dC ρAB)ᴴ * ((PERM_mat dA dB dC)ᴴ *          ((T₂_mat dA dB dC σBC)ᴴ * (T₂_mat dA dB dC σBC)) *          PERM_mat dA dB dC) * (T₁_mat dA dB dC ρAB) := by        simp [Matrix.conjTranspose_mul, Matrix.mul_assoc]      _ ≤ (T₁_mat dA dB dC ρAB)ᴴ * 1 * (T₁_mat dA dB dC ρAB) :=        Matrix.PosSemidef.conjTranspose_mul_mul_mono _ h_step1      _ = 1 := by rw [Matrix.mul_one, T₁_isometry _ hρ]