Matrix Map Is Positive herm Dual

theorem MatrixMap.IsPositive.hermDual (h : MatrixMap.IsPositive f.map) : f.hermDual.map.IsPositive := by  unfold IsPositive at h ⊢  intro x hx  set xH : HermitianMat dOut ℂ := ⟨x, hx.left⟩ with hxH  have hx' : x = xH := rfl; clear_value xH; subst x; clear hxH  change Matrix.PosSemidef (f.hermDual xH).mat  rw [← HermitianMat.zero_le_iff] at hx ⊢  classical  rw [HermitianMat.nonneg_iff_inner_nonneg]  intro y hy  rw [HermitianMat.zero_le_iff] at hy  specialize h hy  change Matrix.PosSemidef (f y).mat at h  rw [← HermitianMat.zero_le_iff] at h  rw [HPMap.inner_hermDual, HPMap.hermDual_hermDual]  apply HermitianMat.inner_ge_zero hx h