Support Proj mul of ker le

lemma supportProj_mul_of_ker_le {A B : HermitianMat d ℂ}    (hker : A.ker ≤ B.ker) :    A.supportProj.mat * B.mat = B.mat := by  contrapose! hker;  simp_all [ SetLike.le_def ];  -- Since $B$ is not in the kernel of $A$, there exists some $x \in \ker(A)$ such that $Bx \neq 0$.  obtain ⟨x, hx⟩ : ∃ x : EuclideanSpace ℂ d, A.mat.mulVec x = 0 ∧ B.mat.mulVec x ≠ 0 := by    contrapose! hker;    have h_support : ∀ x : EuclideanSpace ℂ d, B.mat.mulVec x = B.mat.mulVec (A.supportProj.mat.mulVec x) := by      intro x      have h_support : x.ofLp = A.supportProj.mat.mulVec x.ofLp + A.kerProj.mat.mulVec x.ofLp := by        have h_support : A.supportProj.mat + A.kerProj.mat = 1 := by          simp [ add_comm];          simp [ ← Matrix.ext_iff];          intro i j; exact (by          have h_support : A.kerProj + A.supportProj = 1 := by            exact HermitianMat.kerProj_add_supportProj A;          convert congr_arg ( fun f => f i j ) h_support using 1);        rw [ ← Matrix.add_mulVec, h_support, Matrix.one_mulVec ];      have h_support : B.mat.mulVec (A.kerProj.mat.mulVec x.ofLp) = 0 := by        convert hker _ _;        have h_support : A.mat * A.kerProj.mat = 0 := by          have h_support : A.mat * A.kerProj.mat = A.mat * (1 - A.supportProj.mat) := by            congr;            have h_support : A.kerProj + A.supportProj = 1 := by              exact HermitianMat.kerProj_add_supportProj A;            exact eq_sub_of_add_eq <| congr_arg Subtype.val h_support;          rw [ h_support, mul_sub, mul_one, sub_eq_zero ];          exact Eq.symm (HermitianMat.mul_supportProj_of_ker_le fun ⦃x⦄ a => a);        convert congr_arg ( fun m => m.mulVec x.ofLp ) h_support using 1;        · simp        · simp      convert congr_arg ( fun y => B.mat.mulVec y ) ‹x.ofLp = A.supportProj.mat.mulVec x.ofLp + A.kerProj.mat.mulVec x.ofLp› using 1 ; simp [ Matrix.mulVec_add, h_support ];    have h_support : B.mat = B.mat * A.supportProj.mat := by      ext i j;      convert congr_fun ( h_support ( EuclideanSpace.single j 1 ) ) i using 1;      · simp [ Matrix.mulVec, dotProduct ];      · simp [ Matrix.mulVec, dotProduct ];        rfl;    have h_support : B.mat = B.mat.conjTranspose := by      exact B.2.symm;    have h_support : (B.mat * A.supportProj.mat).conjTranspose = A.supportProj.mat * B.mat := by      simp [Matrix.conjTranspose_mul ];    lia;  refine ⟨x, ?_, ?_⟩  · simpa [HermitianMat.ker, HermitianMat.lin, funext_iff, Matrix.toLpLin] using hx.1  · rw [HermitianMat.mem_ker_iff_mulVec_zero]    exact hx.right