The free light condensed R-module R[ℕ∪∞] is internally projective

theorem LightCondensed.internallyProjective_free_natUnionInfty (R : Type) [CommRing R] : CategoryTheory.InternallyProjective ((free R).obj LightProfinite.NatUnionInfty.toCondensed)