Pos Def trace Right

lemma PosDef_traceRight [Nonempty dB] (A : HermitianMat (dA × dB) ℂ) (hA : A.mat.PosDef) :    A.traceRight.mat.PosDef := by  have h_trace_right_pos_def : ∀ (x : EuclideanSpace ℂ dA), x ≠ 0 → 0 < ∑ k : dB, (star x) ⬝ᵥ (Matrix.mulVec (A.val.submatrix (fun i => (i, k)) (fun i => (i, k))) x) := by    intro x hx_ne_zero    have h_inner_pos : ∀ k : dB, 0 ≤ (star x) ⬝ᵥ (Matrix.mulVec (A.val.submatrix (fun i => (i, k)) (fun i => (i, k))) x) := by      have := (Matrix.posDef_iff_dotProduct_mulVec.mp hA).2;      intro k      specialize @this ( fun i => if h : i.2 = k then x i.1 else 0 )      simp_all only [ne_eq, dite_eq_ite, dotProduct, Pi.star_apply, RCLike.star_def, Matrix.mulVec,        HermitianMat.mat_apply, mul_ite, mul_zero, HermitianMat.val_eq_coe, Matrix.submatrix_apply]      convert this ( show ( fun i : dA × dB => if i.2 = k then x i.1 else 0 ) ≠ 0 from fun h => hx_ne_zero <| by ext i; simpa using congr_fun h ( i, k ) ) |> le_of_lt using 1;      rw [ ← Finset.sum_subset ( Finset.subset_univ ( Finset.image ( fun i : dA => ( i, k ) ) Finset.univ ) ) ]      · simp only [Finset.sum_ite, Finset.sum_const_zero, add_zero, Set.InjOn, Finset.coe_univ,          Set.mem_univ, Prod.mk.injEq, and_true, imp_self, implies_true, Finset.sum_image, ↓reduceIte];        refine' Finset.sum_congr rfl fun i hi => _;        refine' congr_arg _ ( Finset.sum_bij ( fun j _ => ( j, k ) ) _ _ _ _ ) <;> simp      · simp only [Finset.mem_univ, Finset.mem_image, true_and, not_exists, ne_eq, Finset.sum_ite,          Finset.sum_const_zero, add_zero, mul_eq_zero, map_eq_zero, ite_eq_right_iff, forall_const,          Prod.forall, Prod.mk.injEq, not_and, forall_eq];        exact fun a b hb => Or.inl fun h => False.elim <| hb <| h.symm;    obtain ⟨k, hk⟩ : ∃ k : dB, (star x) ⬝ᵥ (Matrix.mulVec (A.val.submatrix (fun i => (i, k)) (fun i => (i, k))) x) > 0 := by      have := @(Matrix.posDef_iff_dotProduct_mulVec.mp hA).2 ( fun i => x i.1 * ( if i.2 = Classical.arbitrary dB then 1 else 0 ) )      simp_all only [ne_eq, dotProduct, Pi.star_apply, RCLike.star_def, Matrix.mulVec,        HermitianMat.val_eq_coe, Matrix.submatrix_apply, HermitianMat.mat_apply, mul_ite, mul_one, mul_zero]      contrapose! this      simp_all only [ne_eq, funext_iff, Pi.zero_apply, ite_eq_right_iff, Prod.forall, forall_eq,        not_forall, Finset.sum_ite, Finset.sum_const_zero, add_zero] ;      constructor      · rw [← Function.ne_iff]        change _ ≠ 0        simpa using hx_ne_zero      convert this ( Classical.arbitrary dB ) using 1;      rw [ ← Finset.sum_subset ( Finset.subset_univ ( Finset.univ.image fun i : dA => ( i, Classical.arbitrary dB ) ) ) ]      · simp only [Finset.coe_univ, Prod.mk.injEq, and_true, implies_true, Set.injOn_of_eq_iff_eq,          Finset.sum_image, ↓reduceIte, gt_iff_lt]        congr! 3;        refine' Finset.sum_bij ( fun y hy => y.1 ) _ _ _ _ <;> simp      · simp only [Finset.mem_univ, Finset.mem_image, true_and, not_exists, ne_eq, mul_eq_zero,          map_eq_zero, ite_eq_right_iff, forall_const, Prod.forall, Prod.mk.injEq, not_and, forall_eq]        exact fun a b hb => Or.inl fun h => False.elim <| hb <| h.symm ▸ rfl    exact lt_of_lt_of_le hk ( Finset.single_le_sum ( fun k _ => h_inner_pos k ) ( Finset.mem_univ k ) );  rw [Matrix.posDef_iff_dotProduct_mulVec]  refine' ⟨A.traceRight.2, fun x hx => _ ⟩;  · convert h_trace_right_pos_def (WithLp.toLp 2 x) (by simpa using hx) using 1;    unfold HermitianMat.traceRight    simp only [dotProduct, Pi.star_apply, RCLike.star_def, HermitianMat.mat_mk, HermitianMat.val_eq_coe]    simp only [Matrix.mulVec, dotProduct, mul_comm, Matrix.submatrix_apply, HermitianMat.mat_apply];    simp only [Matrix.traceRight, HermitianMat.mat_apply, Matrix.of_apply, mul_comm, Finset.mul_sum]    rw [Finset.sum_comm_cycle]