Ker le of ker kron le right

lemma ker_le_of_ker_kron_le_right (ρ₁ σ₁ : MState d₁) (ρ₂ σ₂ : MState d₂)  (h : (σ₁ ⊗ᴹ σ₂).M.ker ≤ (ρ₁ ⊗ᴹ ρ₂).M.ker) :    σ₂.M.ker ≤ ρ₂.M.ker := by  intro v hv;  have h_z : ∃ u : EuclideanSpace ℂ d₁, u ≠ 0 ∧ u ∉ σ₁.M.ker ∧ u ∉ ρ₁.M.ker := by    have h_z : σ₁.M.ker ≠ ⊤ ∧ ρ₁.M.ker ≠ ⊤ := by      have h_ker_ne_top : ∀ (ρ : MState d₁), ρ.M.ker ≠ ⊤ := by        intro ρ hρ_top        have h_contra : ρ.M = 0 := by          ext i j          simp_all [ Submodule.eq_top_iff' ] ;          convert congr(WithLp.ofLp $(hρ_top ( EuclideanSpace.single j 1 ) ) i) using 1          simp          erw [ Matrix.toLpLin_apply ]          aesop        exact ρ.pos.ne' h_contra;      exact ⟨ h_ker_ne_top σ₁, h_ker_ne_top ρ₁ ⟩;    have h_z : ∃ u : EuclideanSpace ℂ d₁, u ∉ σ₁.M.ker ∧ u ∉ ρ₁.M.ker := by      have h_z : ∀ (U V : Submodule ℂ (EuclideanSpace ℂ d₁)), U ≠ ⊤ → V ≠ ⊤ → ∃ u : EuclideanSpace ℂ d₁, u ∉ U ∧ u ∉ V := by        intro U V hU hV        by_contra h_contra        push_neg at h_contra;        have h_union : ∃ u : EuclideanSpace ℂ d₁, u ∉ U ∧ u ∈ V := by          exact Exists.elim ( show ∃ u : EuclideanSpace ℂ d₁, u ∉ U from by simpa [ Submodule.eq_top_iff' ] using hU ) fun u hu => ⟨ u, hu, h_contra u hu ⟩;        obtain ⟨ u, hu₁, hu₂ ⟩ := h_union;        have h_union : ∀ v : EuclideanSpace ℂ d₁, v ∈ U → v + u ∈ V := by          intro v hv; specialize h_contra ( v + u ) ; simp_all [ Submodule.add_mem_iff_right ] ;        have h_union : ∀ v : EuclideanSpace ℂ d₁, v ∈ U → v ∈ V := by          exact fun v hv => by simpa using V.sub_mem ( h_union v hv ) hu₂;        exact hV ( eq_top_iff.mpr fun x hx => by by_cases hxU : x ∈ U <;> aesop );      exact h_z _ _ ( by tauto ) ( by tauto );    exact ⟨ h_z.choose, by intro h; simpa [ h ] using h_z.choose_spec.1, h_z.choose_spec.1, h_z.choose_spec.2 ⟩;  obtain ⟨ u, hu₁, hu₂, hu₃ ⟩ := h_z;  -- Consider the vector $z = u \otimes v$.  set z : EuclideanSpace ℂ (d₁ × d₂) := .toLp 2 ( fun p => u p.1 * v p.2 );  have hz : z ∈ (σ₁ ⊗ᴹ σ₂).M.ker := by    -- By definition of $z$, we have $(σ₁ ⊗ σ₂).mat.mulVec z = σ₁.mat.mulVec u ⊗ σ₂.mat.mulVec v$.    have hz_mul : (σ₁ ⊗ᴹ σ₂).M.mat.mulVec z = fun p => (σ₁.M.mat.mulVec u) p.1 * (σ₂.M.mat.mulVec v) p.2 := by      ext p; simp [z, Matrix.mulVec]      simp [ dotProduct, Finset.mul_sum, Finset.sum_mul, mul_assoc, mul_comm, mul_left_comm ];      rw [ ← Finset.sum_product' ];      refine' Finset.sum_bij ( fun x _ => ( x.2, x.1 ) ) _ _ _ _ <;> simp;      exact fun a b => Or.inl <| Or.inl <| rfl;    simp_all [ funext_iff, Matrix.mulVec ];    ext ⟨ a, b ⟩    specialize hz_mul a b    simp_all [ dotProduct]    convert hz_mul using 1;    simp_all only [zero_eq_mul]    exact Or.inr ( by simpa [ Matrix.mulVec, dotProduct ] using congr(WithLp.ofLp $hv b) );  have hz' : z ∈ (ρ₁ ⊗ᴹ ρ₂).M.ker := by    exact h hz;  have hz'' : ∀ i j, (ρ₁.M.val.mulVec u) i * (ρ₂.M.val.mulVec v) j = 0 := by    intro i j;    have hz'' : (ρ₁.M.val.kronecker ρ₂.M.val).mulVec (fun p => u p.1 * v p.2) (i, j) = (ρ₁.M.val.mulVec u) i * (ρ₂.M.val.mulVec v) j := by      simp [ Matrix.mulVec, dotProduct, Finset.mul_sum, mul_assoc, mul_comm, mul_left_comm ];      simp [ mul_assoc, Finset.mul_sum, Finset.sum_mul ];      rw [ ← Finset.sum_product' ];      refine' Finset.sum_bij ( fun x _ => ( x.2, x.1 ) ) _ _ _ _      · simp      · simp      · simp      · intro _ _        simp only [MState.m, HermitianMat.mat_apply]        ring_nf    exact hz''.symm.trans ( by simpa using congr(WithLp.ofLp $hz' ( i, j )) );  contrapose! hz'';  obtain ⟨ i, hi ⟩ := Function.ne_iff.mp ( show ρ₁.M.val.mulVec u ≠ 0 from fun h => hu₃ <| congr(WithLp.toLp 2 $h))  obtain ⟨ j, hj ⟩ := Function.ne_iff.mp ( show ρ₂.M.val.mulVec v ≠ 0 from fun h => hz'' <| congr(WithLp.toLp 2 $h))  use i, j  aesop;