Conj Transpose isometry mul isometry le one

theorem conjTranspose_isometry_mul_isometry_le_one {m n k : Type*}    [Fintype m] [Fintype n] [Fintype k] [DecidableEq m] [DecidableEq n] [DecidableEq k]    (A : Matrix k m ℂ) (B : Matrix k n ℂ)    (hA : A.conjTranspose * A = 1) (hB : B.conjTranspose * B = 1) :    (A.conjTranspose * B).conjTranspose * (A.conjTranspose * B) ≤ 1 := by  have h_le : (Bᴴ * A) * (Bᴴ * A)ᴴ ≤ 1 := by    have h_le : (Bᴴ * A) * (Bᴴ * A)ᴴ ≤ (Bᴴ * B) := by      have h_le : (A * Aᴴ) ≤ 1 := by        apply isometry_mul_conjTranspose_le_one A hA;      -- Apply the fact that if $X \leq Y$, then $CXC^* \leq CYC^*$ for any matrix $C$.      have h_conj : ∀ (C : Matrix n k ℂ) (X Y : Matrix k k ℂ), X ≤ Y → C * X * Cᴴ ≤ C * Y * Cᴴ :=        fun C X Y a => Matrix.PosSemidef.mul_mul_conjTranspose_mono C a      simpa [ Matrix.mul_assoc ] using h_conj Bᴴ ( A * Aᴴ ) 1 h_le;    aesop;  simpa [ Matrix.mul_assoc ] using h_le