Ker le of ker kron le left

lemma ker_le_of_ker_kron_le_left (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂)  (h : (σ₁ ⊗ᴹ σ₂).M.ker ≤ (ρ₁ ⊗ᴹ ρ₂).M.ker) :    σ₁.M.ker ≤ ρ₁.M.ker := by  intro u hu  obtain ⟨v, hv⟩ : ∃ v : EuclideanSpace ℂ d₂, v ∉ (σ₂ :HermitianMat d₂ ℂ).ker ∧ v ∉ (ρ₂ :HermitianMat d₂ ℂ).ker := by    have h_union : (σ₂ : HermitianMat d₂ ℂ).ker ≠ ⊤ ∧ (ρ₂ : HermitianMat d₂ ℂ).ker ≠ ⊤ := by      constructor <;> intro h_top;      · have h_contra : σ₂.M = 0 := by          ext1          simp_all [ Submodule.eq_top_iff'];          ext i j          specialize h_top ( EuclideanSpace.single j 1 )          simp_all          replace h_top := congr(WithLp.ofLp $h_top i)          simp_all          convert h_top using 1;          erw [ Matrix.toLpLin_apply ]          simp_all only [MState.mat_M, EuclideanSpace.ofLp_single, Matrix.mulVec_single,            MulOpposite.op_one, Pi.smul_apply, Matrix.col_apply, one_smul]        exact σ₂.pos.ne' h_contra;      · have h_contra : ρ₂.M = 0 := by          ext i j; simp_all [ Submodule.eq_top_iff' ] ;          convert congr(WithLp.ofLp $(h_top (WithLp.toLp 2 ( Pi.single j 1 )) ) i) using 1          simp          simp [ HermitianMat.lin ];          rfl        exact ρ₂.pos.ne' h_contra;    have h_union : ∀ (U V : Submodule ℂ (EuclideanSpace ℂ d₂)), U ≠ ⊤ → V ≠ ⊤ → ∃ v : EuclideanSpace ℂ d₂, v ∉ U ∧ v ∉ V := by      intros U V hU hV;      by_contra h_contra;      have h_union : U ⊔ V = ⊤ := by        ext v        simp only [Submodule.mem_top, iff_true]        by_cases hvU : v ∈ U <;> by_cases hvV : v ∈ V <;> simp_all [ Submodule.mem_sup ];        · exact ⟨ v, hvU, 0, by simp, by simp ⟩;        · exact ⟨ v, hvU, 0, by simp, by simp ⟩;        · exact ⟨ 0, by simp, v, h_contra v hvU, by simp ⟩;      have h_union : ∃ v : EuclideanSpace ℂ d₂, v ∉ U ∧ v ∈ V := by        have h_union : ∃ v : EuclideanSpace ℂ d₂, v ∈ V ∧ v ∉ U := by          have h_not_subset : ¬V ≤ U := by            exact fun h => hU <| by rw [ eq_top_iff ] ; exact h_union ▸ sup_le ( by tauto ) h;          exact Set.not_subset.mp h_not_subset;        exact ⟨ h_union.choose, h_union.choose_spec.2, h_union.choose_spec.1 ⟩;      obtain ⟨ v, hv₁, hv₂ ⟩ := h_union;      obtain ⟨ w, hw₁, hw₂ ⟩ : ∃ w : EuclideanSpace ℂ d₂, w ∉ V ∧ w ∈ U := by        obtain ⟨ w, hw ⟩ := ( show ∃ w : EuclideanSpace ℂ d₂, w ∉ V from by simpa [ Submodule.eq_top_iff' ] using hV ) ; use w; simp_all [ Submodule.eq_top_iff' ] ;        exact Classical.not_not.1 fun hw' => hw <| h_contra _ hw';      have h_union : v + w ∉ U ∧ v + w ∉ V := by        exact ⟨ fun h => hv₁ <| by simpa using U.sub_mem h hw₂, fun h => hw₁ <| by simpa using V.sub_mem h hv₂ ⟩;      exact h_contra ⟨ v + w, h_union.1, h_union.2 ⟩;    exact h_union _ _ ( by tauto ) ( by tauto );  -- Consider $z = u \otimes v$.  set z : EuclideanSpace ℂ (d₁ × d₂) := WithLp.toLp 2 ( fun p => u p.1 * v p.2 );  have hz : z ∈ (σ₁ ⊗ᴹ σ₂ : HermitianMat (d₁ × d₂) ℂ).ker := by    ext ⟨i, j⟩    simp [z]    have h_kronecker : ∀ (A : Matrix d₁ d₁ ℂ) (B : Matrix d₂ d₂ ℂ) (u : d₁ → ℂ) (v : d₂ → ℂ), (A.kronecker B).mulVec (fun p => u p.1 * v p.2) = fun p => (A.mulVec u) p.1 * (B.mulVec v) p.2 := by      intro A B u v; ext ⟨ i, j ⟩ ; simp [ Matrix.mulVec, dotProduct, Finset.mul_sum, mul_comm, mul_left_comm ] ;      exact Fintype.sum_prod_type_right fun x => A i x.1 * (B j x.2 * (u x.1 * v x.2));    convert congr_fun ( h_kronecker σ₁.1.mat σ₂.1.mat u v ) ( i, j ) using 1 ; simp    exact Or.inl ( by simpa [ Matrix.mulVec ] using congr(WithLp.ofLp $hu i) );  have hz' : z ∈ (ρ₁ ⊗ᴹ ρ₂ : HermitianMat (d₁ × d₂) ℂ).ker := by    exact h hz;  have hz'' : ∀ a b, (ρ₁.M.val.mulVec u) a * (ρ₂.M.val.mulVec v) b = 0 := by    intro a b    have hz'' : (ρ₁.M.val.mulVec u) a * (ρ₂.M.val.mulVec v) b = ((ρ₁ ⊗ᴹ ρ₂ : HermitianMat (d₁ × d₂) ℂ).val.mulVec z) (a, b) := by      simp [ Matrix.mulVec, dotProduct];      simp [  Finset.sum_mul, mul_assoc, mul_comm];      simp [ z, Finset.mul_sum, mul_assoc, mul_left_comm ];      erw [ Finset.sum_product ] ; simp      exact rfl;    exact hz''.trans ( by simpa using congr(WithLp.ofLp $hz' ( a, b )) );  ext a; specialize hz'' a; simp_all [ Matrix.mulVec, dotProduct ] ;  contrapose! hv;  intro hv'; ext b; specialize hz'' b; simp_all  exact hz''.resolve_left ( by simpa [ Matrix.mulVec, dotProduct ] using hv )