Burnside's matrix-algebra theorem in Lean via jacobson_density on k[S]-asModule

To prove an irreducible monoid S ⊆ Module.End K V spans End V (K algebraically closed, V finite-dimensional), take ρ := S.subtype as a Representation K S V. Mathlib's IsIrreducible gives an instance IsSimpleModule k[S] ρ.asModule. IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed K says every element of End k[S] M is algebraMap c, so any K-linear f becomes F : Module.End (Module.End k[S] M) M via m ↦ E.symm (f (E m)), where E := ρ.asModuleEquiv. In map_smul', destruct φ = algebraMap c, then change the goal to scalar form and finish with simp. Now jacobson_density F (image of finBasis under E.symm) gives r : k[S] agreeing with f on a basis, so f = ρ.asAlgebraHom r. Rewrite with asAlgebraHom_def and MonoidAlgebra.lift_apply to get a Finsupp.sum, and Submodule.sum_mem/smul_mem/subset_span put it in the span. Gotcha: to extract f (b i) = E (F (E.symm (b i))), change _ = E (E.symm (f (E (E.symm _)))) and then simp with apply_symm_apply. simpa [F] leaves the asModule smul unreduced.