Ker kron le of le

lemma ker_kron_le_of_le {d₁ d₂ : Type*} [Fintype d₁] [Fintype d₂] [DecidableEq d₁] [DecidableEq d₂]    (A C : Matrix d₁ d₁ ℂ) (B D : Matrix d₂ d₂ ℂ)    (hA : LinearMap.ker A.toEuclideanLin ≤ LinearMap.ker C.toEuclideanLin)    (hB : LinearMap.ker B.toEuclideanLin ≤ LinearMap.ker D.toEuclideanLin) :    LinearMap.ker (A.kronecker B).toEuclideanLin ≤ LinearMap.ker (C.kronecker D).toEuclideanLin := by  intro x hx  simp only [Matrix.kronecker, LinearMap.mem_ker, Matrix.toLpLin_apply,    WithLp.toLp_eq_zero] at hx ⊢  -- By definition of Kronecker product, we know that $(A \otimes B)x = 0$ if and only if for all $i$ and $j$, $\sum_{k,l} A_{ik} B_{jl} x_{kl} = 0$.  have h_kronecker : ∀ i j, ∑ k, A i k • ∑ l, B j l • x (k, l) = 0 := by    intro i j    replace hx := congr_fun hx ( i, j )    simp only [Matrix.mulVec, dotProduct, Matrix.kroneckerMap_apply,      Pi.zero_apply, smul_eq_mul, Finset.mul_sum] at hx ⊢    rw [ ← Finset.sum_product' ]    simpa only [mul_assoc, Finset.univ_product_univ] using hx  -- Apply the hypothesis `hA` to each term in the sum.  have h_apply_hA : ∀ i j, ∑ k, C i k • ∑ l, B j l • x (k, l) = 0 := by    intro i j    specialize hA ( show (WithLp.toLp 2 ( fun k => ∑ l, B j l • x ( k, l ) )) ∈ LinearMap.ker ( Matrix.toEuclideanLin A ) from ?_ )    · simp_all only [smul_eq_mul, LinearMap.mem_ker]      ext i_1 : 1      simp_all only [PiLp.zero_apply]      apply h_kronecker    · exact congr(WithLp.ofLp $hA i)  ext ⟨ i, j ⟩  simp only [smul_eq_mul, Matrix.mulVec, dotProduct, Matrix.kroneckerMap_apply,    Pi.zero_apply] at h_kronecker h_apply_hA ⊢  have h_apply_hB : ∑ l, D j l • ∑ k, C i k • x (k, l) = 0 := by    specialize hB    simp_all only [funext_iff, Pi.zero_apply, Prod.forall, smul_eq_mul]    have := hB ( show  (WithLp.toLp 2 ( fun l => ∑ k, C i k * x ( k, l ) )) ∈ LinearMap.ker ( Matrix.toEuclideanLin B ) from ?_ )    · simp_all only [LinearMap.mem_ker] ;      exact congr(WithLp.ofLp $this j)    · ext j      specialize h_apply_hA i j      simp [ Matrix.mulVec, dotProduct, Finset.mul_sum ] at h_apply_hA ⊢      simp_rw [mul_left_comm]      rw [Finset.sum_comm]      exact h_apply_hA  rw [← h_apply_hB]  simp only [smul_eq_mul, Finset.mul_sum]  rw [ Finset.sum_sigma' ];  refine' Finset.sum_bij ( fun x _ => ⟨ x.2, x.1 ⟩ ) _ _ _ _  · simp  · simp  · simp  · simp only [Finset.mem_univ, mul_assoc, Prod.mk.eta, mul_left_comm, imp_self, implies_true]